--- layout: fc_discuss_archives title: Message 14 from Frama-C-discuss on April 2014 ---
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