Hi Dave,

>> 
>> I has looked into compiling those files with the patch some time ago;
>> looking at my notes, one issue was with this on-stack buffer:
>>    char extra[1024];
>> declared outside the loop.  Inside the loop, it gets modified in
>> various ways:
>>    extra[0] = '\0';
>> and
>>    if (fread(extra, 1, extsize, fpZip) == extsize) {
>> where the latter means "extra" becomes tainted.
>> 
>> However "extra" is barely used, and is effectively reset each time
>> through the loop - but the analyzer doesn't figure that out.  So the
>> loop analysis explodes, as it tries to keep track of the possibility
>> that "extra" is still tainted from previous iteration(s), despite the
>> fact that it's going to be clobbered before it ever gets used.
>> 
>> So one fix might be to extend the state-purging code so that it somehow
>> "sees" that "extra" gets clobbered before it gets used, and thus we can
>> purge the tainted state from it.
> 
> Thanks for your notes. I think we may be talking about the same thing? If you look at the updated proposal (I have changed it quite a lot since I first sent it out), you’ll see there is one relevant paper for state merging (although it is slightly different from state purging, I think the goal and general methodology is similar): https://dslab.epfl.ch/pubs/stateMerging.pdf 
> 
> I was trying to say if some similar situation happened for other types of checkers, I expected state explosion would also happen. I tried to construct a similar example (with the same kind of reset and nested conditionals + a loop) but for double-free, so far no success yet. I’ll pick it up afterwards, at latest by next Saturday, because I need to prepare for a coming midterm on Friday. I will also put this test case to the proposal because it seems like a very good starting point for the project.

As promised, below is a small example that causes state explosion without taint state machine involved.

void test()
{
  void *p;
  int a;
  scanf(“%d", &a);
  
  while (a > 0)
  {
     p = malloc (1024);
     if (a > 1)
       free(p);
     a--;
   }
   
   if (a >0)
     free(p);
}

This example not only causes state explosion, but also reports false positive of double-free.

By the way, do you have any feedback regarding my proposal (https://docs.google.com/document/d/1MRI1R5DaX8kM6DaqRQsEri5Mx2FvHmWv13qe1W0Bj0g <https://docs.google.com/document/d/1MRI1R5DaX8kM6DaqRQsEri5Mx2FvHmWv13qe1W0Bj0g/edit>)? I am happy to allocate more time polishing the proposal if you find anything off there. If you prefer me sending it via email again (for ease of reference in the future maybe?), I am happy to do so as well.

Best,
Shengyu