1

\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条件，我该如何丢弃它？

PS我使用钠frama-c。

4

1 回答 1

3

WP还没有完全支持分配是否是结果？

恰恰。事实上，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 的标准标题，事情就比较棘手了。一种可能性是禁用所有需要检查（-wp-prop="-@requires"），并有选择地启用其他检查（-wp-prop="r1,r2,r3,...,rn"如果您已为所有检查提供了名称。

于 2015-09-08T17:21:29.830 回答