search

boogie-org / corral

solver for the reachability modulo theories problem
MIT License
58 stars 29 forks source link

AV: Deadcode detection not working for null test after deref #39

Open shaobo-he opened 7 years ago

shaobo-he commented 7 years ago

Consider the following program:

struct X {int* p;};

int foo(struct X* x)
{
  int a = x->p;
  if (!x)
    return -1;
  else
    return a;
}

AV does not detect deadcode of the if branch given the blocking condition x != NULL because we disable the assertion assert x != NULL into assume x != NULL when checking inconsistency. The reachability angelic assertion is proved at the beginning therefore the consistency will trivially hold.

To reproduce this issue, please try, avh null-test-before-deref-null.inst.bpl hinst.bpl /entryPointProc:foo /unknownProc:malloc /unknownProc:$alloc /killAfter:1000 /noAA /deadCodeDetection avn hinst.bpl /sdv /timeoutEE:200 /timeout:1000 /noEbasic /EE:ignoreAllAssumes+ /dontGeneralize /dumpResults:results.txt /EE:onlySlicAssumes+ /EE:ignoreAllAssumes- /killAfter:3600

zvonimir commented 4 years ago

I am guessing nobody will work on this any time soon, if ever. @shuvendu-lahiri and @akashlal : are you ok if I mark this as "won't fix" and close the issue?