Frama-C news and ideas

To content | To menu | To search | Frama-C Home

Post-conditions and names of arguments

In an ACSL post-condition, any reference to the name of one of the function's arguments is assumed to refer to the initial value of the argument.

/* ensures arg == 1; */
void f(int arg)
{
  arg = 1;
}

For instance, in function f above, Frama-C's value analysis plug-in will typically say that the status of the post-condition is unknown, because arg is taken to mean \old(arg), the value passed to f and thus untouched by the assignment. The rationale is that arg has already ceased to live when the post-condition is evaluated: the program could not observe or otherwise depend on the value of arg after the call to f() anyway. On the other hand, it is convenient to be able to relate results and arguments of the function, and this can be done with the simple syntax “arg”. For a global variable G, one would have to write “\old(G)” to refer in f's post-condition to the value of G just before the call to f. The syntax “G” in a post-condition would refer to the value of G at the end of the function.


But do not worry, if you forget the above subtlety, you can always spend twenty minutes adding debug messages to the value analysis plug-in until you finally remember that said subtlety is what is actually implemented.

Comments

1. On Thursday, January 23 2014, 08:46 by Yannick Moy

Hi Pascal, why not deprecate this use, and instead recommend to use \old(arg) always in postconditions?

2. On Thursday, January 23 2014, 18:29 by Virgile

Frama-C sorts of recommend it, at it is how it is "pretty"-printed in the normalized code.

3. On Thursday, January 23 2014, 23:12 by pascal
@yannick I don't think this is a problem that needs solving. People write ACSL for functions that do not use their arguments as local variables all the time. On the other hand, I was caught once by an over-reduced testcase that the sender thought exhibited something strange, and it only took me twenty minutes to understand my mistake.