3

我是 Frama-C 的新手用户，对指针断言有一些疑问。

考虑以下涉及的 C 片段：

  • 两个相关的数据结构Data和Handle，st Handle有一个指向Data的指针；
  • 数据中的“状态”字段，指示某些假设操作是否已完成
  • 三个函数：init()、start_operation() 和 wait()；
  • 使用上述方法的 main() 函数，并包含 6 个断言 (A1-A6)

现在，为什么 A5 和 A6 不能用 WP 验证程序断言（“frama-c -wp file.c”）由于 start_operation() 上的最后一个“ensures”子句，它们不应该成立吗？

我究竟做错了什么？

最好的，

爱德华多

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

1 回答 1

2

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

ACSL 结构的\old工作方式与您想象的不完全一样。

首先，\old(handle)在后置条件中与 相同handle，因为handle是参数。合同旨在从调用者的角度使用。即使函数wait被修改handle（这可能是不寻常的，但可能），它的合约仍然旨在将调用者作为参数传递的值与函数返回给调用者的状态相关联。

简而言之，在 ACSL 后置条件中，parameter总是意味着\old(parameter)（即使函数parameter像局部变量一样修改）。

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

从上下文来看，您似乎打算handle->data == \old(handle->data)改为，这意味着“新状态中旧值指向的字段等于.data旧状态中旧值指向的字段”。随着这种变化，所有你程序中的断言为我得到了证明（使用 Alt-Ergo 0.93）。handle.datahandle

于 2012-03-29T20:50:04.320 回答