Open taquangtrung opened 3 years ago
Conservative underlying analysis could be improved.
Do you suggest that both EXPECTEDFAIL_NOALIAS
and NOALIAS
are acceptable for b
and &b1
?
Hi again,
Sorry for bothering you a lot this morning. I think this test case also needs to be fixed for the non-terminating recursive call...
Thank you a lot again for fixing them! :-)
Done and thank you~ f8ac87128bd29fc281ea96cf13b3307fa0808385
For a quick update, when a base case is added to foo
, I think the two assertions MUSTALIAS
will become MAYALIAS
(when the call to foo
terminates immediately at the base case).
How do you think about it?
Yes, correct. However, for current SVF's flow-sensitive implementation, we did not distinguish MAY and MUST for now. For your usage purposes, I have changed it.
Thank you very much! :-)
Hi,
In this test case, I think the assertion
EXPECTEDFAIL_NOALIAS(b,&b1)
should beNOALIAS(b,&b1)
?It is very similar to the assertion
NOALIAS(c,&c1)
, which I think is correct.