SVF-tools / Test-Suite

PTABen: Micro-benchmark Suite for Pointer Analysis
70 stars 38 forks source link

Possile incorrect assertion in `cs_tests/cs21.c`? #21

Open taquangtrung opened 3 years ago

taquangtrung commented 3 years ago

Hi,

For the test case cs_tests/cs21.c, I believe the assertion MUSTALIAS inside the function foo should be only MAYALIAS.

This is because the function foo is non-terminating in the if-then case (in the function call foo(z): z==x). Hence, the return statement can never be reached, therefore, we cannot say that y and &a are must-alias.

Could you advise if my understanding is correct?

// cs_tests/cs21.c

#include "aliascheck.h"
int a;
int *foo(int *x){
   int*z = x;
   int* y;
   if(x)
    y = foo(z);
   else
    y = x;

    MUSTALIAS(y,&a);             // this should be MayAlias, since `foo` is non-terminating in the if-then case.
    return y;
}

int main(){
 int*p;
 p = &a;
 foo(p);
}
yuleisui commented 3 years ago

Yes, correct. Would you mind submitting a pull request or you want me to change it?

Thanks,

taquangtrung commented 3 years ago

Hi, thanks for the quick reply. Could you please change it? I think that will be more convenient for you.

yuleisui commented 3 years ago

Done.