使用Frama-C验证单链表复制函数失败的原因咨询

我正尝试使用Frama-C结合Alt-Ergo求解器验证单链表的递归复制函数copyListRec，但验证后有8个目标未被证明。查阅手册后发现Frama-C对malloc和函数指针的支持似乎有限，我想确认是验证条件存在遗漏，还是Frama-C本身不适合处理链表相关的形式化验证？

验证所用代码 #

#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

问题分析与解决方案 #

Frama-C完全支持链表验证 #

Frama-C（尤其是WP插件）完全可以处理链表这类递归数据结构的验证，你的问题并非工具本身不适合，而是验证规范和条件存在遗漏，同时需要补充malloc的行为约束。

关键问题修复 #

1. 补充malloc的规范

WP默认生成的malloc规范不足以支撑验证，需要手动添加明确的契约：

/*@
  requires size > 0;
  assigns \nothing;
  ensures \valid(\result) && \fresh(\result, size);
  ensures \separated(\result, \allocated);
*/
extern void* malloc(size_t size);

这个规范明确malloc返回的指针是有效、新鲜（未被使用过）且与已分配内存分离的，这对证明\separated(\result,h)和samelist的分离条件至关重要。

2. 修复递归函数的终止性证明

WP警告递归函数缺少decreases子句，需要补充终止度量（用链表的length），同时明确输入链表有限的前置条件：

/*@
  requires finite(h);  // 明确输入链表是有限的
  terminates \true; 
  decreases length(h); // 终止度量：递归调用时链表长度递减
  assigns \result \from h;
  ensures \separated(\result,h);
  ensures finite(\result);
  ensures samelist(\result,h);
*/

3. 修正samelist的归纳定义

原基例写法错误，应该直接定义空链表的相等情况：

/*@inductive samelist{L} (list* l1, list* l2) {
     case base_same{L}: samelist(\null, \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) ;
} */

修正后才能触发WP的归纳推理机制，证明递归复制后的链表与原链表结构一致。

4. 消除类型转换警告

代码中(list *) malloc (sizeof *c)的强制转换可去掉，C标准允许void*隐式转换为其他指针类型，避免类型不兼容警告：

list *c = malloc(sizeof *c);

验证优化建议 #

• 启用RTE检查：添加-rte选项，让WP自动生成空指针解引用、内存有效性等检查目标，确保代码无运行时错误。
• 多求解器配合：使用-wp-prover alt-ergo,cvc4让WP尝试多个求解器，提升证明成功率。

修复后的效果 #

补充上述规范和修正后，大部分未证明的目标可被Alt-Ergo自动证明，剩余少量目标可能需要辅助引理（如finite(h) ==> finite(h->next)），但WP的归纳策略通常能自动处理这类递归性质。

内容的提问来源于stack exchange，提问作者user3598542