Prooving freeable with frama-c WP plugin

Question

How can I prove that a pointer is \freeable, given it is a precondition?

#include <stdlib.h>

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

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

$ 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)

If it is not supported, why does WP generates the typed_fint_call_free_deallocation_pre_freeable condition, and how can I discard it?

P.S. I use sodium frama-c.

Answer 1

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

Precisely. In fact, WP tries to warn you about that with these messages

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

When WP encounters a construction that it does not know how to translate, it replaces it with \false in case the annotation is in some dead code path (hence always valid). As far as I know, this behavior cannot be deactivated.

If you name your annotations, you can selectively deselect some of them with -wp-prop="-name". For free, if you don't want to edit the Frama-C's standard header, things are more tricky. A possibility would be to disable all requires check (-wp-prop="-@requires"), and to selectively enable the other ones (-wp-prop="r1,r2,r3,...,rn" if you have provided names for all of them.