使用 frama-c WP 插件证明可免费使用

Question

如何证明指针是 \freeable，因为它是前提条件？

#include <stdlib.h>

/*@ requires \freeable(i);
  @ frees i;
 */
void fint (int* i) {
    //@ assert(\freeable(i));
    free(i);
}

是否因此，WP 尚未完全支持分配？

$ frama-c -wp -wp-rte lll.c
[jessie3] Loading Why3 configuration...
[jessie3] Why3 environment loaded.
[jessie3] Loading Why3 theories...
[jessie3] Loading Why3 modules...
[kernel] Parsing FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i (no preprocessing)
[kernel] Parsing lll.c (with preprocessing)
[wp] Running WP plugin...
[wp] Collecting axiomatic usage
[rte] annotating function fint
lll.c:8:[wp] warning: Cast with incompatible pointers types (source: sint32*) (target: sint8*)
FRAMAC_SHARE/libc/stdlib.h:175:[wp] warning: Allocation, initialization and danglingness not yet im
plemented                                                                                         
              (freeable: \freeable(p))
FRAMAC_SHARE/libc/stdlib.h:177:[wp] warning: Allocation, initialization and danglingness not yet im
plemented                                                                                         
              (\allocable(\at(p,Pre)))
lll.c:7:[wp] warning: Allocation, initialization and danglingness not yet implemented
              (\freeable(i))
lll.c:3:[wp] warning: Allocation, initialization and danglingness not yet implemented
              (\freeable(\at(i,Pre)))
[wp] 2 goals scheduled
[wp] [Alt-Ergo] Goal typed_fint_call_free_deallocation_pre_freeable : Unknown (52ms) (Degenerated, 
4 warnings)                                                                                       
[wp] [Alt-Ergo] Goal typed_fint_assert : Unknown (53ms) (Degenerated, 2 warnings)
[wp] Proved goals:    0 / 2
     Alt-Ergo:        0  (unknown: 2)

如果不支持，WP为什么会生成typed_fint_call_free_deallocation_pre_freeable条件，如何丢弃？

P.S。我用的是 sodium frama-c。

Answer 1

Is it a consequence, that the allocation is not fully supported by WP yet?

没错。事实上，WP 试图通过这些消息警告您

FRAMAC_SHARE/libc/stdlib.h:175:[wp] warning: Allocation, initialization and danglingness not yet implemented                                                                                         
          (freeable: \freeable(p))

当 WP 遇到不知道如何翻译的结构时，它将其替换为 \false 以防注释位于某些死代码路径中（因此始终有效）。据我所知，此行为无法停用。

如果您为注释命名，您可以使用 -wp-prop="-name" 有选择地取消选择其中的一些注释。对于 free，如果您不想编辑 Frama-C 的标准 header，事情就比较棘手了。一种可能性是禁用所有需要检查（-wp-prop="-@requires"），并有选择地启用其他检查（-wp-prop="r1,r2,r3,...,rn" 如果您为所有这些检查提供了名称。

使用 frama-c WP 插件证明可免费使用

Prooving freeable with frama-c WP plugin

formal-verification

frama-c