Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

The EXPECTEDFAIL_NOALIAS in cs_tests/recur9.c should be NOALIAS? #28

Open
taquangtrung opened this issue Nov 18, 2020 · 7 comments
Open

Comments

@taquangtrung
Copy link

Hi,

In this test case, I think the assertion EXPECTEDFAIL_NOALIAS(b,&b1) should be NOALIAS(b,&b1)?

It is very similar to the assertion NOALIAS(c,&c1), which I think is correct.

// cs_tests/recur9.c

#include "aliascheck.h"
int z;
void foo(int **a);
void bar(int **q){
    int** a = malloc(10);
    foo(a);
}

void foo(int **a){
    *a = &z;
    bar(a);
}

int main(){
    int** a,*b,*c,b1,c1;
    b = &b1;
    a = &b;
    foo(a);
    MUSTALIAS(b,&z);
    EXPECTEDFAIL_NOALIAS(b,&b1);
    a = &c;
    foo(a);
    MUSTALIAS(c,&z);
    NOALIAS(c,&c1);
}
@yuleisui
Copy link
Collaborator

Conservative underlying analysis could be improved.

@taquangtrung
Copy link
Author

Do you suggest that both EXPECTEDFAIL_NOALIAS and NOALIAS are acceptable for b and &b1?

@taquangtrung
Copy link
Author

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! :-)

@yuleisui
Copy link
Collaborator

Done and thank you~
f8ac871

@taquangtrung
Copy link
Author

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?

@yuleisui
Copy link
Collaborator

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.

@taquangtrung
Copy link
Author

Thank you very much! :-)

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

2 participants