使用 Frama-C 复制单链表

Question

我正在尝试用 Frama-C 验证上述内容。从手册来看，Frama-C 似乎不太适合 malloc 和函数指针。我想知道我的验证条件中是否缺少某些内容，或者 Frama-C 不太适合处理列表？输出用于 Alt-Ergo 求解器。

#include <stdlib.h>

typedef struct _list { 
int key;
struct _list *next;
} list; //defined list

/*@
  inductive reachable{L} (list* root, list* node) {
     case root_reachable{L}: \forall list* root; reachable(root,root);
     case next_reachable{L}: \forall list* root, *node; \valid(root) && reachable(root->next,node) ==> reachable(root,node) ;
} */

/*@inductive samelist{L} (list* l1, list* l2) {
     case base_same{L}: \forall list* l1, *l2; l1 == \null && l2 == \null;
     case next_same{L}: \forall list* l1, *l2; \valid(l1) && \valid(l2) && \separated(l1, l2) 
      && l1->key == l2->key && samelist(l1->next,l2->next) ==> samelist(l1,l2) ;
} */

/*@ predicate finite{L}(list* root) = reachable(root,\null); */

/*@ 
axiomatic Length {
  logic integer length{L}(list* l);
  axiom length_nil{L}: length(\null) == 0;
  axiom length_cons{L}:
  \forall list* l, integer n; finite(l) && \valid(l) ==> length(l) == length(l->next) + 1;
} */

/*@
  terminates finite(h); 
  assigns \result \from h;
  ensures \separated(\result,h);
  ensures finite(\result);
  ensures samelist(\result,h);
*/

 list *copyListRec(list *h)
 {
    if(h == NULL)
    {
       return NULL;
    }
    else
    {
       list *c = (list *) malloc (sizeof *c);
       c->key = h->key;
       c->next = copyListRec(h->next);
       return c;
    }
  
}

这是 wp (Alt-Ergo) 的输出：

[kernel] Parsing framac-copyList.c (with preprocessing)
[kernel:annot:missing-spec] FRAMAC_SHARE/libc/stdlib.h:436: Warning: 
  Neither code nor explicit exits and terminates for function malloc,
   generating default clauses. See -generated-spec-* options for more info
[wp] Warning: Missing RTE guards
[wp] Warning: No definition for 'length' interpreted as reads nothing
[wp] framac-copyList.c:47: Warning: 
  Missing decreases clause on recursive function copyListRec, call must be unreachable
[wp] FRAMAC_SHARE/libc/stdlib.h:427: Warning: 
  Allocation, initialization and danglingness not yet implemented
  (allocation: \fresh{Old, Here}(\at(\result,wp:post),\at(size,wp:pre)))
[wp] framac-copyList.c:45: Warning: 
  Cast with incompatible pointers types (source: sint8*) (target: _list*)
[wp] 18 goals scheduled
[wp] [Failure] typed_copyListRec_ensures (Qed 5ms) (Alt-Ergo) (Stronger, 2 warnings)
[wp] [Failure] typed_copyListRec_terminates_part3 (Qed 0.73ms) (Alt-Ergo) (Stronger, 2 warnings)
[wp] [Failure] typed_copyListRec_terminates_part2 (Qed 1ms) (Alt-Ergo) (Stronger, 2 warnings)
[wp] [Failure] typed_copyListRec_ensures_2 (Qed 6ms) (Alt-Ergo) (Stronger, 2 warnings)
[wp] [Failure] typed_copyListRec_ensures_3 (Qed 8ms) (Alt-Ergo) (Stronger, 2 warnings)
[wp] [Failure] typed_copyListRec_assigns_normal_part3 (Qed 3ms) (Alt-Ergo) (Stronger, 2 warnings)
[wp] [Failure] typed_copyListRec_assigns_normal_part6 (Qed 4ms) (Alt-Ergo) (Stronger, 2 warnings)
[wp] [Failure] typed_copyListRec_assigns_normal_part5 (Qed 5ms) (Alt-Ergo) (Stronger, 2 warnings)
[wp] Proved goals:   10 / 18
  Qed:            10 (0.73ms-2ms-8ms)
  Failed:          8

Answer 1

使用 Frama-C 和 WP 处理链表非常困难。此外，当前 WP 不处理动态分配（这是 WP 手册中列出的已知限制）。

这里，失败是由于你的归纳定义

samelist

：第一种情况没有使用

samelist

，这导致Why3中输入错误。 WP 应该这么说，所以我建议在 Frama-C 的公共 GitLab 上创建一个问题。

此外，您对

length

的定义没有给出它所依赖的内存占用量，应该使用

reads

子句来完成。

如果您有兴趣查看 Frama-C 的链表退出验证，您可以查看这篇论文：https://link.springer.com/chapter/10.1007/978-3-319-77935-5_3 以及本文中引用的文章。