--- layout: fc_discuss_archives title: Message 14 from Frama-C-discuss on April 2014 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Internal state represented by ghost variable not provable



I am trying to model functional behavior that depends on the call
history, i.e. the function shall behave differently when a certain
condition occurs several times in a row. In my example, a function
returns zero if called once or twice, and returns one when called for
the third time, starting this behavior all over.

This can be implemented with a static variable. I have modelled
this behaviour with a ghost variable as it had been suggested on this 
list. Here is my specification:

//file: button.h
/*
   Returns True if pressed three times, otherwise False.
  */

//@ ghost unsigned int no_btn_press = 0;

/*@
   @  behavior FewPresses:
   @    assumes no_btn_press < 2;
   @    ensures no_btn_press == \old(no_btn_press) + 1;
   @    ensures \result == 0;
   @  behavior EnoughPresses:
   @    assumes no_btn_press >= 2;
   @    ensures no_btn_press == 0;
   @    ensures \result != 0;
   @  complete behaviors FewPresses,EnoughPresses;
   @  disjoint behaviors FewPresses,EnoughPresses;
   @*/
char btnpress(void);

In the implementation, I equate the ghost variable with the internal
static variable that represents the number of calls:

//file: button.c
#include "button.h"

char btnpress(void)
{
   static unsigned int presscnt = 0;
   char retval;

   //@ ghost no_btn_press = presscnt;
   if (presscnt >= 2 )
     {
       presscnt = 0;
       retval = 1;
       //@ ghost no_btn_press = presscnt;
     } else
     {
       //@ assert no_btn_press < 2;
       presscnt++;
       retval = 0;
       //@ ghost no_btn_press = presscnt;
     }
   return retval;
}

When I call frama-c with the wp plug-in, I get 7 goals of which 4
cannot be proven. These four are related to the post conditions
of the two behaviors, see session log at the end.

Playing around with assertions a bit I have got the suspicion that the
ghost variable and the internal counter are not in sync for the
prover. I have tried to enforce this with a global data invariant, but
I then got syntax errors (even on the example from the ACSL
specification).

My questions are now:
1. Is this the proper way to specify such a behaviour anyway?
2. If so, how can I prove it?

Here is my log:

> frama-c -wp -wp-rte button.c -then -report
[kernel] preprocessing with "gcc -C -E -I.  button.c"
[wp] Running WP plugin...
[wp] Collecting axiomatic usage
[rte] annotating function btnpress
[wp] 7 goals scheduled
[wp] [Alt-Ergo] Goal typed_btnpress_EnoughPresses_post : Unknown (Qed:3ms)
[wp] [Alt-Ergo] Goal typed_btnpress_assert_rte_unsigned_overflow : Valid (33ms) (2)
[wp] [Alt-Ergo] Goal typed_btnpress_disjoint_FewPresses_EnoughPresses : Valid (40ms) (2)
[wp] [Alt-Ergo] Goal typed_btnpress_complete_FewPresses_EnoughPresses : Valid (27ms) (2)
[wp] [Alt-Ergo] Goal typed_btnpress_EnoughPresses_post_2 : Unknown (Qed:3ms)
[wp] [Alt-Ergo] Goal typed_btnpress_FewPresses_post_2 : Unknown
[wp] [Alt-Ergo] Goal typed_btnpress_FewPresses_post : Unknown (Qed:3ms)
[report] Computing properties status...

--------------------------------------------------------------------------------
--- Properties of Function 'btnpress'
--------------------------------------------------------------------------------

[    -    ] Post-condition for 'FewPresses' (file button.h, line 11)
             tried with Wp.typed.
[    -    ] Post-condition for 'FewPresses' (file button.h, line 12)
             tried with Wp.typed.
[    -    ] Post-condition for 'EnoughPresses' (file button.h, line 15)
             tried with Wp.typed.
[    -    ] Post-condition for 'EnoughPresses' (file button.h, line 16)
             tried with Wp.typed.
[  Valid  ] Assertion 'rte,unsigned_overflow' (file button.c, line 17)
             by Wp.typed.
[  Valid  ] Complete behaviors 'FewPresses', 'EnoughPresses'
             by Wp.typed.
[  Valid  ] Disjoint behaviors 'FewPresses', 'EnoughPresses'
             by Wp.typed.
[    -    ] Behavior 'EnoughPresses'
             tried with Frama-C kernel.
[    -    ] Behavior 'FewPresses'
             tried with Frama-C kernel.

--------------------------------------------------------------------------------
--- Status Report Summary
--------------------------------------------------------------------------------
      3 Completely validated
      6 To be validated
      9 Total
--------------------------------------------------------------------------------




Frank