Skip to main content

Combine Uninitialized Variables Analysis with Alias Analysis

Supervisor

Suitable for

MSc in Computer Science

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; }