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

Provide expressive error message when user attempts to use is_fresh in assertion #8498

Open
hanno-becker opened this issue Nov 7, 2024 · 0 comments

Comments

@hanno-becker
Copy link

hanno-becker commented Nov 7, 2024

It seems that __CPROVER_is_fresh() is not supported in an assertion, but it is difficult to understand that from the error messages provided by CBMC.

Example:

// file: harness.c
void harness(void) {
    int x;
    __CPROVER_assert(__CPROVER_is_fresh(&x, sizeof(x)), "");
}

Commands:

	goto-cc harness.c --function harness -o a.out
	goto-instrument --dfcc harness a.out b.out
	cbmc b.out --smt2

Error message:

...
Removal of function pointers and virtual functions
Generic Property Instrumentation
Starting Bounded Model Checking
goto_symext::address_arithmetic does not handle address_of
make: *** [Makefile:59: doit2] Error 6

Ask: Improve the error message to explain to the user that one cannot use __CPROVER_is_fresh in an assertion (?)

@hanno-becker hanno-becker changed the title Provide expressive error message when user attempts to user is_fresh in assertion Provide expressive error message when user attempts to use is_fresh in assertion Nov 7, 2024
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

1 participant