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

Non-terminating recursive call before assertions in cs_tests/recur10.c #29

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

Comments

@taquangtrung
Copy link

taquangtrung commented Nov 18, 2020

Hi,

For this test case, the first recursive call to f() inside the body of f will be non-terminating.

So, I wonder if it is OK to check alias information after this call?
Such assertions will never be reached anyway.

// cs_tests/recur10.c

#include "aliascheck.h"
int **p,*x, y, z;

void f() {
  p = &x;
  if (1) {
    *p = &y;
	MUSTALIAS(x,&y);
    f();
    *p = &z;
	/// p doesn't point to x at the above line: although p's
	/// value changed by stmt "p=&x", the value flow can not
	/// reach "*p=&z" since it will flow into f() before
	/// "*p=&z" and connected with the entry of f(). So the
	/// store "*p=&z" can not be completed as p's pts is empty.
	NOALIAS(x,&z);
	NOALIAS(x,&y);
    f();
  }
}

int main()
{
    f();
    return 0;
}
@yuleisui
Copy link
Collaborator

Yes, correct. I guess the reason might because the test case writer was not considering path sensitivity (branch conditions). I am changing the if condition to make it terminable.

@taquangtrung
Copy link
Author

Thank you for the update!

@taquangtrung
Copy link
Author

Hi,

Do you have any updates for this test case?

Is it possible to change the condition if (1) to something like if (z)? I saw that if (z) is also used by the other test case recur4.c

@yuleisui
Copy link
Collaborator

Added the base case: 60848d6

@taquangtrung
Copy link
Author

taquangtrung commented Jan 14, 2021

Thank you for the quick update! I also notice the same issue in recur0.c

void f() {
  if (1) {
    x = &y;
    MUSTALIAS(x, &y)
    f();
    x = &z;
    MUSTALIAS(x, &z)
    NOALIAS(x, &y)
    f();
  }
}

@yuleisui
Copy link
Collaborator

Done. dca7f8d

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