Combine Uninitialized Variables Analysis with Alias Analysis
Supervisor
Suitable for
Abstract
goto-instrument features an instrumentation to track cases of use-before-define, i.e., reading of uninitialized variables. At present, the analysis does not take into account aliasing information. As such, the following code will yield a spurious counterexample:int main() { int x; int *ptr;
ptr=&x; *ptr=42;
if(x < 42) return 1;
return 0; }