a soundness bug (perhaps due to mishandling of parameter passing?)

[zhendongsu]

$ tis-interpreter.sh test.c
[value] Analyzing a complete application starting at main
[value] Computing initial state
[value] Initial state computed

100

[value] done for function main
$ 
$ cat test.c
int printf (const char *, ...); 

int a = 100; 

void foo (int p)
{
  a = 0;
}

int main ()
{
  foo (a);
  printf ("%d\n", a); 
  return 0; 
}
$ 

[regehr]

It's crazy that we ran tis-interpreter on so many interesting codes and never ran into this!

[zhendongsu]

I've been doing some testing of the tis-interpreter itself lately. More to come. :)

[regehr]

Cool! It might be worth getting a more recent snapshot of the tool from Pascal if he has time to prepare one.

[pascal-cuoq]

Well found. This is one case where the sophistication of the analyzer leads to bugs that would not have happened in an interpreter written from scratch.

[zhendongsu]

@pascal-cuoq I'd certainly almost agree with you, Pascal, but "... would not have happened ..." would be a bit too strong --- anything could happen of course.

[pascal-cuoq]

Let me put it this way then: the fix only deletes code. The code would not have existed in the first place if tis-interpreter did not originate from a static analyzer.