WP: Incorrect assigns global/static handling
View all of the following goals succeed for the following program:
#include <assert.h>
unsigned int number = 0;
/*@
assigns number;
ensures \valid(\result);
*/
unsigned int* a_num(void) {
++number;
return &number;
}
void test_a_num(void) {
unsigned int* a = a_num();
unsigned int copy = *a;
assert(copy == *a);
unsigned int* b = a_num();
assert(copy == *a);
}
int main(int argc, char** argv) {
test_a_num();
return 0;
}
compiled with frama-c-gui -wp -wp-rte -wp-smoke-tests test.c
Expected behaviour
The second assert function call fails when run, and therefore WP should not be able to prove its preconditions.
Actual behaviour
It claims that it has proven (incorrectly) that the assert function call will be successful. Of course the assert
calls may be replaced with /*@ assert */
statements instead, and it still claims that they pass.
Fix ideas
Check handling of static/global variables with assigns?
Edited by Loïc Correnson