ftsrg / gazer

An LLVM-based formal verification frontend for C programs.
24 stars 5 forks source link

Segmentation fault in a program with return in a nested loop #72

Open sallaigy opened 3 years ago

sallaigy commented 3 years ago

Translating the following program results in a segmentation fault:

int *a;
int b;
int c(int e, int *g) {
  for (;;)
    for (b = 1; e; b++)
      if (a[b]) {
        *g = b;
        return 1;
      }
}
int main() { int d, f = c(d, &f); }

This is caused by the value of variable being null in ModuleToAutomata.cpp:448