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