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

[Frama-c-discuss] Can i specify/proove a function to be "just called"?



Hello,

2014/1/14  <ds.verification at flecsim.com>:

> So, the idea is that for the function being called that its call has no
> (visible-to-Frama-C) effect but i only need to ensure it is called: The
> function is "trustable" and has side effects which are out of scope of the
> verification.
>
> I thought of something like:
>
> /* Does some magic (e.g. external assembly module), but has no contract
>  * its own
>  */
> extern void foo(int val);
>
> int counter = 0;
>
> /* @ensures \called(foo(\old(counter)));
>    @ensures \counter=\old(counter)+1;
>  */
> void test1()
> {
>     foo(counter);
>     counter++;
> }
>
> Is this possible in ACSL?
>

You might be interested in the Aora? plug-in
(http://frama-c.com/download/frama-c-aorai-manual.pdf), whose main aim
is to specify the sequences of function calls that can occur during
the execution of a program. Such a specification is then translated
into a set of ACSL contracts which have to be discharged by WP, Jessie
or Value analysis (or any other plug-in that can check the validity of
ACSL formulas). From what you describe, I'd say that the following
automaton (not tested) should do the trick:

%init: Init;
%accept: OK;
%deterministic;

Init: { CALL(test1) } -> FOO;

FOO: {  foo() } -> OK
      |  { RETURN(test1) } -> KO
      |  other -> FOO;

OK: -> OK;

KO: -> KO;

Note that Aora?'s current version only considers defined functions, so
that you'd have to provide a dummy body for foo in order to use this
plugin.

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