Frama-c: Function calls and static variables

I'm currently discovering frama-c's features, and especially WP & Value's analysis tools. My final goal is to be able to use frama-c on larger codes that involves several layers with:

a lot of function calls
use of complex data structures
static and/or global variables

So far I've been trying to apply a bottom-up method i.e starting specifying functions that does not includes any function calls and analyze their behaviors by isolating them thanks to -lib-entry and -main kernel options. By doing that I make sure that if pre conditions are assumed to be true, then the whole function contract is verified. As soon as I tried to specify upper layers that invokes those functions, things gets complicated. First I often have to specify the behavior of the called functions which is not always easy because those functions may deal with variables/functions out of the scope of the current function.

Let me give you an easy example:

Let's say that in file1.h we define a data structure "my_struct" that contains a field number and a field parity.

In file1.c I have two functions:

A first function "check_parity" that just tests if the parity field of the static variable _sVar is correct.
A second function "correct_parity" that calls the first function, and corrects the parity if the field was not correct.

In file2.c, I have a function "outside_caller" that just calls correct_parity(). My objective is to be able to specify outside_caller the same way I'm specifying correct_parity. Below is the corresponding source code:

file1.h

/* parity = 0 => even ; 1 => odd */

typedef unsigned char TYP_U08;
typedef unsigned short TYP_U16;
typedef unsigned int TYP_U32;
typedef unsigned long TYP_U64;

typedef struct {
    unsigned char parity;
    unsigned int number;
} my_stuct;

typedef enum
{
    S_ERROR        =  -1
    ,S_OK          =  0
    ,S_WARNING     =  1
} TYPE_STATUS;

/*@ ghost my_stuct* g_sVar; */

/*@ predicate fc_pre_is_parity_ok{Labl}(my_stuct* i_sVar) =
        (
      \at(i_sVar->parity, Labl) == ((TYP_U08) (\at(i_sVar->number,Labl) % 2u))
    );

  @ predicate fc_pre_valid_parity{Labl}(my_stuct* i_sVar) = 
    (
        (\at(i_sVar->parity,Labl) == 0) ||
        (\at(i_sVar->parity, Labl) == 1)
    );

  @ predicate fc_pre_is_parity_readable(my_stuct* i_sVar) =
    (
        \valid_read(&i_sVar->parity)
    );

  @ predicate fc_pre_is_parity_writeable(my_stuct* i_sVar) =
    (
        \valid(&i_sVar->parity)
    );

  @ predicate fc_pre_is_number_readable(my_stuct* i_sVar) =
    (
        \valid_read(&i_sVar->number)
    );

  @ predicate fc_pre_is_number_writeable(my_stuct* i_sVar) =
    (
        \valid(&i_sVar->number)
    );
*/

TYPE_STATUS check_parity(void);
TYPE_STATUS correct_parity(void);

file1.c

static my_stuct* _sVar;

  /*@ requires check_req_parity_readable:
    fc_pre_is_parity_readable(_sVar);

    @ requires check_req_number_readable:
      fc_pre_is_number_readable(_sVar);

    @ assigns check_assigns:
      g_sVar;

    @ ensures check_ensures_error:
      !fc_pre_valid_parity{Post}(g_sVar) ==> \result == S_ERROR;

    @ ensures check_ensures_ok:
      (
        fc_pre_valid_parity{Post}(g_sVar) &&
        fc_pre_is_parity_ok{Post}(g_sVar) 
      ) ==> \result == S_OK;

    @ ensures check_ensures_warning:
      (
        fc_pre_valid_parity{Post}(g_sVar) &&
        !fc_pre_is_parity_ok{Post}(g_sVar)
      ) ==> \result == S_WARNING;

    @ ensures check_ensures_ghost_consistency:
      \at(g_sVar, Post) == _sVar;
  */
TYPE_STATUS check_parity(void)
{
    //@ ghost g_sVar = _sVar;
    TYPE_STATUS status = S_OK;
    if(!(_sVar->parity == 0 || _sVar->parity == 1)) {
        status = S_ERROR;
    } else if ( _sVar->parity == (TYP_U08)(_sVar->number % 2u) ){
        status = S_OK;
    } else {
        status = S_WARNING;
    }
  return status;
}


  /*@ requires correct_req_is_parity_writeable:
    fc_pre_is_parity_writeable(_sVar);

    @ requires correct_req_is_number_readable:
    fc_pre_is_number_readable(_sVar);

    @ assigns correct_assigns:
    _sVar->parity,
    g_sVar,
    g_sVar->parity;

    @ ensures correct_ensures_error:
    !fc_pre_valid_parity{Pre}(g_sVar) ==> \result == S_ERROR;

    @ ensures correct_ensures_ok:
    (
      fc_pre_valid_parity{Pre}(g_sVar) &&
      fc_pre_is_parity_ok{Pre}(g_sVar)
    ) ==> \result == S_OK;

    @ ensures correct_ensures_warning:
    (
      fc_pre_valid_parity{Pre}(g_sVar) &&
      !fc_pre_is_parity_ok{Pre}(g_sVar)
    ) ==> \result == S_WARNING;

    @ ensures correct_ensures_consistency:
      fc_pre_is_parity_ok{Post}(g_sVar);

    @ ensures correct_ensures_validity :
      fc_pre_valid_parity{Post}(g_sVar);

    @ ensures correct_ensures_ghost_consistency:
      \at(g_sVar, Post) == _sVar;
  */
TYPE_STATUS correct_parity(void)
{
    //@ ghost g_sVar = _sVar;
    TYPE_STATUS parity_status = check_parity();

    if(parity_status == S_ERROR || parity_status == S_WARNING) {
        _sVar->parity = (TYP_U08)(_sVar->number % 2u);
        /*@ assert (\at(g_sVar->parity,Here) == 0) ||
               (\at(g_sVar->parity, Here) == 1);
     */
        //@ assert \at(g_sVar->parity, Here) == (TYP_U08)(\at(g_sVar->number,Here) % 2u);
    }
    return parity_status;
}

file2.c

/*@ requires out_req_parity_writable:
    fc_pre_is_parity_writeable(g_sVar);

  @ requires out_req_number_writeable:
    fc_pre_is_number_readable(g_sVar);

  @ assigns out_assigns:
    g_sVar,
    g_sVar->parity;

  @ ensures out_ensures_error:
    !fc_pre_valid_parity{Pre}(g_sVar) ==> \result == S_ERROR;

  @ ensures out_ensures_ok:
    (
      fc_pre_valid_parity{Pre}(g_sVar) &&
      fc_pre_is_parity_ok{Pre}(g_sVar)
    ) ==> \result == S_OK;

  @ ensures out_ensures_warning:
    (
      fc_pre_valid_parity{Pre}(g_sVar) &&
      !fc_pre_is_parity_ok{Pre}(g_sVar)
    ) ==> \result == S_WARNING;

  @ ensures out_ensures_consistency:
    fc_pre_is_parity_ok{Post}(g_sVar);

  @ ensures out_ensures_validity:
    fc_pre_valid_parity{Post}(g_sVar);
*/

TYPE_STATUS outside_caller(void)
{
    TYPE_STATUS status = correct_parity();
    //@ assert fc_pre_is_parity_ok{Here}(g_sVar) ==> status == S_OK;
    /*@ assert !fc_pre_is_parity_ok{Here}(g_sVar) && 
               fc_pre_valid_parity{Here}(g_sVar) ==> status == S_WARNING; */
    //@ assert !fc_pre_valid_parity{Here}(g_sVar) ==> status == S_ERROR;
    return status;
}

Here the main issue is that in order to specify outside_caller(), I need to access _sVar which is out of scope in file2.c. That implies to deal with a ghost variable (g_sVar) that is declared in file1.h and updated in correct_parity function. In order to make the caller (correct_parity) able to use the callee's contracts, the ghost variable g_sVar must be used inside the contracts of the callees.

Here are the results of WP analysis:

(1) check_parity()

frama-c -wp src/main.c src/test.c -cpp-command 'gcc -C -E -Isrc/' -main 'check_parity' -lib-entry -wp-timeout 1 -wp-fct check_parity -wp-rte -wp-fct check_parity -then -report
[rte] annotating function check_parity
[wp] 14 goals scheduled
[wp] Proved goals: 14 / 14
Qed: 9 (4ms)
Alt-Ergo: 5 (8ms-12ms-20ms) (30)

(2) correct_parity()

frama-c -wp src/main.c src/test.c -cpp-command 'gcc -C -E -Isrc/' -main 'correct_parity' -lib-entry -wp-timeout 1 -wp-fct correct_parity -wp-rte -wp-fct correct_parity -then -report
[rte] annotating function correct_parity [wp] 18 goals scheduled
[wp] Proved goals: 18 / 18
Qed: 12 (4ms)
Alt-Ergo: 6 (4ms-37ms-120ms) (108)

(3) outside_caller()

frama-c -wp src/main.c src/test.c -cpp-command 'gcc -C -E -Isrc/' -main 'outside_caller' -lib-entry -wp-timeout 1 -wp-fct outside_caller -wp-rte -wp-fct outside_caller -then -report
[rte] annotating function outside_caller
[wp] 14 goals scheduled
[wp] [Alt-Ergo] Goal typed_outside_caller_assign_exit : Unknown (Qed:4ms) (515ms)
[wp] [Alt-Ergo] Goal typed_outside_caller_call_correct_parity_pre_correct_req_is_par___ : Unknown (636ms)
[wp] [Alt-Ergo] Goal typed_outside_caller_assert : Timeout
[wp] [Alt-Ergo] Goal typed_outside_caller_assign_normal_part1 : Timeout
[wp] [Alt-Ergo] Goal typed_outside_caller_call_correct_parity_pre_correct_req_is_num___ : Unknown (205ms)
[wp] Proved goals: 9 / 14
Qed: 9 (4ms)
Alt-Ergo: 0 (interrupted: 2) (unknown: 3)

==> WP : GUI Output

In this configuration, the callees are specified with g_sVar ghost variable, except for requires and assings clauses for 2 reasons:

I need to check _sVar R/W accesses with \valid & \valid_read since its a pointer
When I tried to specify assigns clauses of the callees with g_sVar, I was not able to verify the corresponding clause.

But by doing so, I somehow made the specification of the caller invalid, as you can see on WP's output.

Why does it seems the more functions calls I have, the more it becomes complicated to prove the behavior of the functions? Is there a proper way to deal with multiple function calls and static variables?

Thank you a lot in advance!

PS: I'm working with Magnesium-20151002 version, on a VM running with Ubuntu 14.04, 64-bit machine. I know that getting started with WhyML and Why3 could help me a lot but so far I haven't been able to install Why3 ide neither on windows nor on Ubuntu following each step of this tutorial.

Solution

First of all, please note that -main and -lib-entry aren't that useful for WP (you mentioned that you are also interested in EVA/Value Analysis, but your question is directed towards WP).

Your issue with static variables is a known one, and the easiest way to deal with it is indeed to declare a ghost variable in the header. But then you must express your contracts in terms of the ghost variable and not the static one. Otherwise, the callers will not be able to make use of these contracts, since they do not know anything about _sVar. As a rule of thumb, it is better to put the contract in the header: this way, you're bound to only use identifiers that are visible outside of the translation unit.

Regarding function calls, the main point is that any function that is called by the function you're trying to prove with WP must come with a contract that at least contain an assigns clause (and possibly more precise specifications, depending on how much the effects of the callee are relevant for the property that you want to prove on the caller). The important thing to remember here is that, from WP's point of view, after the call, only what is explicitly stated in the callee's contract through ensures is true, plus the fact that any location not in the assigns clause has been left unchanged.