The value of \ old in post-condition ACSL
I'm a new Frama-C user and have a few questions regarding assertions over pointers.
Consider snippet C below:
- two related data structures Data and Handle, st Handle has a pointer to Data;
- a 'state' field in Data indicating whether any hypothetical operation has completed
- three functions: init (), start_operation () and wait ();
- main () function using the above and containing 6 statements (A1-A6)
Now why can't A5 and A6 be validated with the WP verifier ("frama-c -wp file.c") Should they not be held because of the last clause "provides" on start_operation ()?
What am I doing wrong?
Best,
Eduardo
typedef enum
{
PENDING, NOT_PENDING
} DataState;
typedef struct
{
DataState state;
int value;
} Data;
typedef struct
{
Data* data;
int id;
} Handle;
/*@
@ ensures \valid(\result);
@ ensures \result->state == NOT_PENDING;
@*/
Data* init(void);
/*@
@ requires data->state == NOT_PENDING;
@ ensures data->state == PENDING;
@ ensures \result->data == data;
@*/
Handle* start_operation(Data* data, int to);
/*@
@ requires handle->data->state == PENDING;
@ ensures handle->data->state == NOT_PENDING;
@ ensures handle->data == \old(handle)->data;
@*/
void wait(Handle* handle);
int main(int argc, char** argv)
{
Data* data = init();
/*@ assert A1: data->state == NOT_PENDING; */
Handle* h = start_operation(data,0);
/*@ assert A2: data->state == PENDING; */
/*@ assert A3: h->data == data; */
wait(h);
/*@ assert A4: h->data->state == NOT_PENDING; */
/*@ assert A5: data->state == NOT_PENDING; */
/*@ assert A6: h->data == data; */
return 0;
}
source to share
You are testing some clever memory manipulation for a "novice".
The ACSL construct \old
doesn't work the way you think.
First, \old(handle)
in the post-condition it matches handle
, because it handle
is a parameter. The contract is intended to be used from the point of view of the subscribers. Even if the function is wait
changed handle
(which would be unusual, but possible), its contract still had to bind the values passed as an argument to the caller and the state returned by the function to the caller.
In short, in an ACSL post-condition, parameter
always means\old(parameter)
(even if the function changes parameter
as a local variable).
Second, the rule above is only for parameters. For globals and memory access, the post-condition is considered to be applicable to the post-state, as you would expect from its name. The construct \old(handle)->data
you wrote, which is equivalent handle->data
, means "the field .data
pointed to by the old descriptor value in the new state", so the postcondition handle->data == \old(handle)->data
is a tautology and probably not what you intended.
From the context it seems like you intended handle->data == \old(handle->data)
instead, which means that the field .data
that the old value handle
points to in the new state is equal to the field .data
that the old value handle
points to the old state. "With this change, all statements in your program will confirm for me (using Alt -Ergo 0.93).
source to share