<div dir="ltr"><div dir="ltr"><div dir="ltr"><div dir="ltr"><div dir="ltr"><div dir="ltr"><div dir="ltr"><div dir="ltr"><div dir="ltr"><div dir="ltr"><div>I hit a problem where it seems the analyzer is not tracking loop control as expected. In the following code, I see a[0] is detected to be a garbage value when symbolically executed. </div><div><br></div><div>clang -cc1 -analyze  -analyzer-checker=core  test.c </div><div>test.c:19:3: warning: Undefined or garbage value returned to caller<br>  return a[0];<br>  ^~~~~~~~~~~<br>1 warning generated.<br><br></div><div>Dumping the egraph, I see that the analyzer eagerly assumes the expression "x < (offs+users)" is false along one of the paths, which is what leads to the failure. </div><div><br></div><div>1) clang -cc1 -analyze  -analyzer-checker=core  -analyzer-config  eagerly-assume=true  -analyzer-dump-egraph=graph.dot  -trim-egraph   test.c</div><div>2) exploded-graph-rewriter.py --single-path --diff --diff graph.dot<br></div><div><br></div><div>Program points: 61. test.c: 14 : 18 : BinaryOperator S867 PostStmt x < (offs + users) Tag: ExprEngine : Eagerly Assume False 62. BlockEdge [B4] -> [B1] 63. BlockEntrance [B1] Store: (0x814b8a8) No changes! Expressions: #0 Call foo - S867 x < (offs + users) (conj_$5{unsigned int, LC1, S815, #1}) < ((conj_$5{unsigned int, LC1, S815, #1}) + (conj_$2{unsigned int, LC1, S796, #1})) + S867 x < (offs + users) 0 S32b Ranges: (conj_$5{unsigned int, LC1, S815, #1}) < ((conj_$5{unsigned int, LC1, S815, #1}) + (conj_$2{unsigned int, LC1, S796, #1})) { [0, 0] }<br></div><div><br></div><div>disabling eagerly-assume shows the same problem. </div><div>clang -cc1 -analyze  -analyzer-checker=core  -analyzer-config  eagerly-assume=false test.c<br></div><div><br></div><div>adding a "__builtin_assume(offs==0);" shows the same problem, and </div><div>adding a "__builtin_assume(offs=0);" avoids the problem but shows a new warning ...</div><div>test.c:14:20: warning: the argument to '__builtin_assume' has side effects that will be discarded<br>  __builtin_assume(offs=0);<br>                   ^~~~~~<br>warning: Trimmed ExplodedGraph is empty.<br>Warning: dumping graph requires assertions<br>1 warning generated.<br><br></div><div>So for the case of "__builtin_assume(offs=0);", one of two things may be occurring:</div><div>1) There really may be a side effect even though the warning says something different.</div><div>2) There really is no side effect, but the SA is picking up on the constraint. </div><div><br></div><div>These are contradictory, and I'm not sure which is correct :/</div><div><br></div><div>Does any one have knowledge of this particular issue and where to dig further into this? Or maybe I'm just missing something obvious :/ </div><div><br></div><div>Thanks - Vince </div><div><br></div><div>The reproducer … </div><div><br></div><div>unsigned getusers(void);<br>unsigned getoffs(void);<br>unsigned foo(void);</div><div>unsigned foo(void) {<br>  unsigned users;<br>  unsigned offs;<br>  unsigned x;<br>  unsigned a[1];</div><div>  users = getusers();<br>  offs = getoffs();<br>  for (x = offs; x < (offs+users); x++) {<br>    a[(x + offs)] = 0; <br>  }</div><div>  // SA warns 'warning: Undefined or garbage value returned to caller' <br>  return a[0];<br>}<br><br></div></div></div></div></div></div></div></div></div></div></div>