Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

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

  • Subject: [Frama-c-discuss] Internal state represented by ghost variable not provable
  • From: frank at dordowsky.de (Frank Dordowsky)
  • Date: Tue, 15 Apr 2014 21:42:11 +0200 (CEST)
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