GitLab

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?