<div dir="ltr"><div dir="ltr"><div dir="ltr"><div dir="ltr">Hi!<div>I have a checker that stores the SymbolRef of a function call (return value). Later the checker makes assumption on this value. If the value was constrained by branch conditions these assumptions  should fail in some cases (if the condition is the opposite of the assumption). The problem is if the return value is assigned to a variable the original symbol value is lost (garbage collected).</div><div><br></div><div>An example code:</div><div><div><br></div><div>void test() {<br></div><div>  int ret = (function() != 0);<br></div><div>  if (ret == 0) { }</div><div>}</div></div><div><br></div><div>It looks like that the analyzer decides about the value of 'function() != 0' at the time of the 'ret = (function() != 0);' statement. Then the value of the function call is lost from the state. The checker needs to test if it is possible for the 'function()' to be zero or nonzero (by making assumption on the function's return value) but the value is not in the state so any assume will succeed. Is it possible to prevent the value of 'function' from garbage collection? Or is there some way in the checker to find the assumed value of the function call? (The state graph shows a state where the needed value is available but I found that no checker callback is called in that phase.)</div><div><br></div><div>Balázs</div><div><br></div></div></div></div></div>