Prooving freeable with frama-c WP plugin

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. Я использую натриевую рамку-с.

Answer 1

Является ли это последствием того, что распределение еще не полностью поддерживается 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", если вы указали имена для всех них.