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