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

Hello Frank

2014-04-15 21:42 GMT+02:00 Frank Dordowsky <frank at dordowsky.de>:
> 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.

> 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?
>

Anne is right, there is no way to properly relate the ghost and the
static variable, and without this information it will be difficult to
prove anything.
Replacing the assignment by an (unprovable) assertion should do the trick.

Another possibility to specify your program is to use the Aora?
plug-in to generate ACSL specifications from an automaton describing
the sequence of event you want to observe, as follows
(see http://frama-c.com/download/frama-c-aorai-manual.pdf for
information about the syntax).

%init: init;
%accept: init, press_1, press_2;

init: { btnpress(){‌{ \result == 0 }‌} } -> press_1
    | other -> init
    ;

press_1: { btnpress(){‌{ \result == 0 }‌} } -> press_2
       | other -> press_1
       ;

press_2: { btnpress(){‌{ \result == 1 }‌} } -> init
       | other -> press_2
       ;


You will then need a wrapper function above btnpress to simulate
successive calls, such as

int main (unsigned int c) {
  while(c) {
    btnpress();
    c--;
  }
}

frama-c -aorai-automata automaton.ya button.c -aorai-output-c-file
button_instrumented.i

will then output in button_instrumented.i an ACSL-annotated code. If
you can prove the contracts of main and btnpress, then you know that
they're conforming to the automaton. However, Aora?-generated ACSL is
not sufficient, as it is also lacking the correspondance between the
state of the automaton and the static variable governing the btnpress
function. Adding manually in the instrumented file a predicate

/*@ predicate glue{L} =
  (0 == presscnt <==> 1 == init) &&
  (1 == presscnt <==> 1 == press_1) &&
  (2 == presscnt <==> 1 == press_2);
*/

and stating that it must be true at the entry and return of btnpress,
as well as being a loop invariant of main gives a provable
specification.

Best regards,
-- 
E tutto per oggi, a la prossima volta
Virgile