FRAMA-C/WP验证swap函数时ensures目标未被证明问题咨询

问题背景 #

尝试验证WP手册中简化版swap函数，但其中一条ensures条款始终无法被证明，使用环境为Frama-C 24.0、Alt-Ergo 2.0.0，此前在大规模代码库测试时也遇到过类似Alt-Ergo报错，想确认是自身操作问题还是 prover的问题。

待验证代码 #

/*@ requires \valid(a) && \valid(b);
@ ensures A: *a == \old(*b) ;
@ ensures B: *b == \old(*a) ;
@ assigns *a,*b ;
@*/
void swap(int *a,int *b)
{
    int tmp = *a;
    *a = *b;
    *b = tmp;
}

执行命令与报错信息 #

执行命令：

frama-c -wp -wp-rte swap.c

报错输出：

[kernel] Parsing main_wp.c (with preprocessing)
[rte] annotating function swap
Collecting axiomatic usagewarning: [Warning] cannot load an editor: missing field 'options'

warning: [Warning] cannot load an editor: missing field 'options'

warning: [Warning] cannot load an editor: missing field 'options'

warning: [Warning] cannot load an editor: missing field 'options'

warning: [Warning] cannot load an editor: missing field 'options'

[wp] 8 goals scheduled
[wp] [Alt-Ergo 2.0.0] Goal typed_swap_ensures_A : Failed
[wp] [Cache] found:3
[wp] Proved goals:    7 / 8
  Qed:               5  (1ms-2ms-4ms)
  Alt-Ergo 2.0.0:    2  (12ms-15ms) (22) (cached: 3) (failed: 1)

分析与解决建议 #

1. 操作无问题：swap函数的逻辑和契约注释完全正确，ensures条款准确描述了交换后的结果，因此不是用户操作的问题。
2. Prover版本局限性：Alt-Ergo 2.0.0存在一些证明能力上的不足，这类简单目标无法证明属于版本偶发问题，在后续版本中已修复。
3. 可行解决方法：
   • 更换Prover：尝试用CVC4或Z3替代Alt-Ergo，执行命令如：

     frama-c -wp -wp-prover cvc4 -wp-rte swap.c
     

   • 升级Alt-Ergo：将Alt-Ergo升级至2.4.0及以上版本，新版本修复了大量证明相关的bug。
   • 添加中间断言：在代码中插入中间断言帮助WP分解证明目标，降低Prover的推理难度：

     /*@ requires \valid(a) && \valid(b);
     @ ensures A: *a == \old(*b) ;
     @ ensures B: *b == \old(*a) ;
     @ assigns *a,*b ;
     @*/
     void swap(int *a,int *b)
     {
         int tmp = *a;
         /*@ assert tmp == \old(*a); */
         *a = *b;
         /*@ assert *a == \old(*b); */
         *b = tmp;
         /*@ assert *b == \old(*a); */
     }
     

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