--- layout: fc_discuss_archives title: Message 32 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,

many thanks for your answers, expecially for the sample.
So i take from this that there is no off-the-shelf \called() predicate
available, but the ghosts offer a loophole ;-) (looks a bit like
test instrumentation code to me).
I will try this in my project.

Thanks again,

	Daniel

Lo?c Correnson schrieb am 14.01.2014 13:49:

> Hi,
> Yes you can simulate this by collecting the parameters send to function foo.
> It is a bit complicated, but it should does the job.
> Just define two ghost variables:
> 
> /*@ghost 
> int foo_calls ;
> int foo_params[] ;
> */
> 
> Then add the following contract for function foo:
> 
> /*@
> ensures foo_params[ foo_calls ] == p ;
> ensures foo_calls == \old(foo_calls+1) ;
> assigns foo_calls , foo_params [ foo_calls+1 ] ;
> */
> void foo( int p ) ;
> 
> You can now prove something like:
> 
> /*@
> ensures foo_calls == \old(foo_calls) + 2;
> ensures foo_params [ \old(foo_calls)+1 ] == 1 ;
> ensures foo_params [ \old(foo_calls)+2 ] == 2 ;
> */
> void test2()
> {
> foo(1);
> foo(2);
> }
> 
> L.
> 
> Le 14 janv. 2014 ? 12:38, <ds.verification at flecsim.com>
> <ds.verification at flecsim.com> a ?crit :
> 
>> Hello everybody,
>> 
>> i have browsed the ACSL reference manual in search for a predicate or other
>> gear to express and prove whether some function is called by some other
>> function.
>> 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?
>> 
>> Thanks in advance
>> 
>> 	Daniel
>> 
>> 
>> _______________________________________________
>> 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
> 
> 
> _______________________________________________
> 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
>