1*1f5207b7SJohn Levon #include <stdio.h> 2*1f5207b7SJohn Levon #include <string.h> 3*1f5207b7SJohn Levon #include "check_debug.h" 4*1f5207b7SJohn Levon 5*1f5207b7SJohn Levon int a, b, c, d; 6*1f5207b7SJohn Levon int e, f, g; main(void)7*1f5207b7SJohn Levonint main(void) 8*1f5207b7SJohn Levon { 9*1f5207b7SJohn Levon if (b > 1000000000) 10*1f5207b7SJohn Levon return 0; 11*1f5207b7SJohn Levon 12*1f5207b7SJohn Levon if (a >= b) 13*1f5207b7SJohn Levon return 1; 14*1f5207b7SJohn Levon if (a < 0 || b < 0) 15*1f5207b7SJohn Levon return 1; 16*1f5207b7SJohn Levon c = b - a; 17*1f5207b7SJohn Levon __smatch_implied(c); 18*1f5207b7SJohn Levon __smatch_compare(b, c); 19*1f5207b7SJohn Levon 20*1f5207b7SJohn Levon if (e < 0 || e > b) 21*1f5207b7SJohn Levon return; 22*1f5207b7SJohn Levon if (f <= 0 || f > b) 23*1f5207b7SJohn Levon return; 24*1f5207b7SJohn Levon g = e + f; 25*1f5207b7SJohn Levon 26*1f5207b7SJohn Levon __smatch_implied(g); 27*1f5207b7SJohn Levon __smatch_implied(e); 28*1f5207b7SJohn Levon __smatch_compare(g, e); 29*1f5207b7SJohn Levon __smatch_compare(e, g); 30*1f5207b7SJohn Levon __smatch_implied(g - e); 31*1f5207b7SJohn Levon __smatch_implied(g - f); 32*1f5207b7SJohn Levon 33*1f5207b7SJohn Levon return 0; 34*1f5207b7SJohn Levon } 35*1f5207b7SJohn Levon 36*1f5207b7SJohn Levon /* 37*1f5207b7SJohn Levon * check-name: Smatch compare #3 38*1f5207b7SJohn Levon * check-command: smatch -I.. sm_compare3.c 39*1f5207b7SJohn Levon * 40*1f5207b7SJohn Levon * check-output-start 41*1f5207b7SJohn Levon sm_compare3.c:17 main() implied: c = '1-1000000000' 42*1f5207b7SJohn Levon sm_compare3.c:18 main() b <= c 43*1f5207b7SJohn Levon sm_compare3.c:26 main() implied: g = '1-2000000000' 44*1f5207b7SJohn Levon sm_compare3.c:27 main() implied: e = '0-1000000000' 45*1f5207b7SJohn Levon sm_compare3.c:28 main() g > e 46*1f5207b7SJohn Levon sm_compare3.c:29 main() e < g 47*1f5207b7SJohn Levon sm_compare3.c:30 main() implied: g - e = '1-2000000000' 48*1f5207b7SJohn Levon sm_compare3.c:31 main() implied: g - f = '0-1999999999' 49*1f5207b7SJohn Levon * check-output-end 50*1f5207b7SJohn Levon */ 51