我尝试了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)
特别是第一个和第三个。好像有什么意想不到的事情发生了?我不太明白该工具在这里遇到的确切问题。