ACSL后置条件中old的意义

Question

我是Frama的新手用户，对于指针上的断言有几个问题。

考虑下面的C片段，包括：

• 两个相关的数据结构数据和句柄，s.t。句柄具有指向数据的指针；
• 是数据中的一个“状态”字段，指示某些假设操作是否具有

函数: init()、start_operation()和wait()；

• 是使用上述方法的main()函数，包含6个断言(A1-A6)

。

现在，为什么A5和A6不能用WP验证器(“frama -wp file.c")断言，因为start_operation()上的最后一个”确保“子句不应该保留？

我做错了什么？

最好的

爱德华多

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; 
}

Answer 1

您正在为“新手”验证一些棘手的内存操作。

ACSL构造\old并不完全像您认为的那样工作。

首先，后置条件下的\old(handle)与handle相同，因为handle是一个参数.合同是从呼叫者的角度来使用的。即使函数wait修改了handle (这是不寻常的，但也是可能的)，它的约定仍然是将调用方作为参数传递的值和函数返回给调用方的状态关联起来。

简而言之，在ACSL的后置条件下，parameter 总是指 \old(parameter) (即使函数像局部变量一样修改parameter )。

第二，上面的规则只适用于参数。对于全局变量和内存访问，post条件被认为适用于post状态，正如您从其名称中所期望的那样。您编写的构造\old(handle)->data (相当于handle->data )意味着“句柄的旧值在新状态中指向的字段.data”，因此后条件handle->data == \old(handle)->data是一个重言式，可能不是您想要的那样。

从上下文来看，您似乎打算使用handle->data == \old(handle->data)，这意味着“handle在新状态中所指向的旧值所指向的字段.data等于旧的handle值在旧状态中所指向的字段.data”。