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?



typedef enum 
} 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; */

  /*@ assert A4: h->data->state == NOT_PENDING; */
  /*@ assert A5: data->state == NOT_PENDING; */
  /*@ assert A6: h->data == data; */

  return 0; 



source to share

1 answer

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).



All Articles