--- layout: fc_discuss_archives title: Message 30 from Frama-C-discuss on January 2014 ---
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