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.

Sign up for GitHub

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

Jump to bottom

#39 #41

Open

MCFuzzer opened this issue Feb 19, 2019 · 0 comments

Labels

confirmed memory model SeaHorn

Owner

MCFuzzer commented Feb 19, 2019

void foo()
{
  static int last_align = -1;
  int dummy = 0;
  int align = (int)&dummy & 15;
  if (last_align < 0)
    last_align = align;
  else if (align != last_align)
    {__VERIFIER_error();}
}

int main()
{
	foo();
	foo();
	return 0;
}

OS: Ubuntu 18.04
Version: 21a1c0
Commandline: sea bpf <file_name.h>
Expected result: TRUE
Tool result: FALSE

The text was updated successfully, but these errors were encountered:

MCFuzzer added SeaHorn memory model confirmed labels

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment