文档中的 ACSL 列表示例生成错误的警告答案

【问题标题】：ACSL list example in the documentation generate a bad sounding warning文档中的 ACSL 列表示例生成错误的警告
【发布时间】：2020-06-08 17:05:50
【问题描述】：

我尝试了 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)

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

【问题讨论】：

标签： c frama-c acsl

【解决方案1】：

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

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

【讨论】：