How to demonstrate prerequisites set by instantiate plugin with WP

When using the instantiate plugin with frama-c (version 27), I'm unable to prove a precondition set by this plugin using either eva or eva and wp plugins.

This very simple piece of code illustrates the problem.

#include <string.h>

int main(void)
{
    unsigned long var;

    memset(&var, 0, sizeof(unsigned long));
    return var;
}

Running the analyser with the following command shows no error : frama-c test.c -eva, but running it with the command frama-c test.c -instantiate -eva gives an unknown status for this precondition :

requires valid_dest: \let __fc_len=len/8; \valid(ptr + (0 .. __fc_len-1));

I tried without any success to prove this properties using wp and alt-ergo prover.

When I translate this precondition to the @assert valid_dest: \let __fc_len=sizeof(unsigned long)/8; \valid(&var + (0 .. __fc_len-1)); assertion, eva is still unable to prove it but WP is (WP is still unable to prove the precondition).

When I translate this precondition to this simplified assertion @assert valid_dest: \valid(&var + (0 .. (sizeof(unsigned long)/8)-1));, eva is able to prove it, but neither eva nor wp are able to prove the precondition.

As a summary :

#include <string.h>

int main(void)
{
    unsigned long var;

    /*@assert valid_dest: \valid(&var + (0 .. (sizeof(unsigned long)/8)-1));*/ /*Success (EVA)*/
    /*@assert valid_dest: \let __fc_len=sizeof(unsigned long)/8; \valid(&var + (0 .. __fc_len-1));*/ /* Success (WP) */
    memset(&var, 0, sizeof(unsigned long)); /* A precondition fails with either EVA or WP if instantiate plugin is used */
    return var;
}

Do you have any ideas how to prove these preconditions when using instantiate plugin ?

Solution

On Frama-C 27.1 Cobalt, the code that you present is entirely proved via the command:

$ frama-c ex.c -instantiate -then -wp
[kernel] Parsing ex.c (with preprocessing)
[wp] Warning: Missing RTE guards
[wp] :0: Warning: 
  Cast with incompatible pointers types (source: uint64*) (target: sint8*)
[wp] :0: Warning: 
  Cast with incompatible pointers types (source: sint8*) (target: uint64*)
[wp] 2 goals scheduled
[wp] [Cache] not used
[wp] Proved goals:    2 / 2
  Qed:             2

WP does not even need to call SMT solvers. (Note: the warning are due to the original memset function that is still in the AST, even though properties are already proved, WP still looks at the code).

Eva cannot prove the precondition because of the \let construct introduced by the Frama-C kernel during the normalization, which is not supported by Eva for now. This could indeed be improved, either by removing this \let introduction or by adding the support of \let in Eva.