--- layout: fc_discuss_archives title: Message 42 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"?



Hi Virgile,

that's an interesting idea. However, i think it is a bit
over-complicated at least for a single call - if there are long chains
of calls to be checked for a definite ordering, i'd agree. Disadvantage
is that this introduces yet another tool/spec language (which had to be
communicated)...

Thanks
	Daniel

Virgile Prevosto schrieb am 16.01.2014 09:38:

> 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
> 
> _______________________________________________
> Frama-c-discuss mailing list
> Frama-c-discuss at lists.gforge.inria.fr
> http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss