文档中的ACSL列表示例会产生听起来不好的警告

Question

我尝试了ACSL manual中的列表示例（第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)

特别是第一个和第三个。好像发生了意外情况？我不太了解该工具在这里出现了什么确切问题。

Answer 1

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

这可能会对切片产生影响，因为这意味着incr_list返回的值与其参数之间的数据依存关系无法准确表示。更一般而言，所有基于Eva的依赖项分析（从入库，切入，切片，影响等）都需要Eva可以解释的\from子句，或者对相应功能的定义进行存根（如果有定义，Eva会赢得不需要规格）。