2

我尝试了ACSL 手册中的列表示例（第 37 页上的示例 2.23，在“功能合同”部分），但我隐藏了实现incr_list并更改了返回类型。完整来源如下。

struct list {
  int hd;
  struct list *next;
};

/*@ inductive reachable{L} (struct list *root,struct list *to) {
  @ case empty{L}: \forall  struct list *l; reachable(l,l) ;
  @ case non_empty{L}:\forall struct list *l1,*l2;
  @ \valid(l1) && reachable(l1->next,l2) ==> reachable(l1,l2) ;
  @ }
  */

// The requires clause forbids giving a circular list
/*@ requires reachable(p,\null);
  @ assigns \result \from { q->hd | struct list *q ; reachable(p,q) } ;
  @
*/
int incr_list(struct list *p);

int main() {
  struct list l = {.hd=0, .next=0};
  struct list l2 = {.hd=1, .next=&l};
  return incr_list(&l2);
}

我正在用切片机运行它frama-c test-1.c -slice-calls incr_list -then-last -print。输出看起来不错，但我担心运行此命令时生成的警告：

[inout] test-1.c:23: Warning: 
  failed to interpret inputs in assigns clause 'assigns \result
                                                  \from {q->hd |
                                                         struct list *q
                                                         ; reachable{Old}(p, q)};'
[eva:alarm] test-1.c:23: Warning: 
  function incr_list: precondition got status unknown.
[eva] test-1.c:23: Warning: 
  cannot interpret 'from'
  clause 'assigns \result \from {q->hd | struct list *q; reachable{Old}(p, q)};'
  (error in AST: non-lval term {q->hd | struct list *q; reachable{Old}(p, q)}; please report)

特别是第一个和第三个。好像有什么意想不到的事情发生了？我不太明白该工具在这里遇到的确切问题。

4

1 回答 1

1

Eva 警告的最后一行确实有点吓人，应该进一步调查，因为这\from部分是完全合法的（它基本上说返回的值incr_list取决于作为参数传递的列表中包含的所有元素）。另一方面，Eva 不知道如何解释集合理解（更不用说reachable归纳谓词也在其能力之外），并且cannot interpret 'from' clause警告的部分是完全正确的。

这反过来可能会对切片产生影响，因为这意味着返回的值incr_list与其参数之间的数据依赖关系没有准确表示。更一般地说，所有基于 Eva 的处理依赖关系（from、inout、slicing、impact...）的分析都需要\fromEva 可以解释的子句，或对应函数的存根定义（如果你有定义，Eva 就不需要规范）。

于 2020-06-09T07:54:25.460 回答