Enforce assumptions made by WP memory model in Frama-C

Question

Is there a way to enforce the assumptions made by a WP memory model?

Consider the following two functions to be verified with Frama-C:

/*@ requires \valid(a) && \valid(b);
  @ ensures A: *a == 1;
  @ ensures B: *b == 2;
  @ assigns *a, *b;
  @*/
void assign_many(int *a, int *b)
{
  *a = 1;
  *b = 2;
}


int main() {
  int a = 42;
  assign_many(&a, &a);
  //@ assert a == 1;
  //@ assert a == 2;
  return 0;
}

The function assign_many cannot verify in the general case, since the two arguments could alias (as demonstrated in main). However, if you choose the Hoare+ref memory model, this function verifies since it assumes separation. But I can still verify main, even using the Typed memory model. With the command-line option -wp-warn-memory-model, a message warns you about what assumptions the memory model requires. Is it possible to enforce these assumptions, e.g., add them as preconditions to assign_many?

Virgile Virgile · Accepted Answer · 2019-03-12T13:49:02

I'm afraid this is not possible directly (i.e. without copy-pasting the generated specification into a new C file and reanalyzing the whole source: the text of the warning seems to take care of expressing that as a valid ACSL contract).

Digging a little bit in the API of the Wp plugin, it can be seen that the separation hypotheses are dealt with in the MemoryContext module of the plug-in, that uses its own custom datatype to represent them (as opposed to an ACSL predicate from the standard AST defined in the kernel).

It is possible to write some code that would take the clauses generated by a given model for a given function and generate a set of ACSL predicates that could then be added as requires clauses for this function (i.e. the programmatic equivalent of the copy-and-paste mentioned above), but this implies a certain knowledge of the Frama-C API.

Enforce assumptions made by WP memory model in Frama-C

1 Answers