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 に答える