--- layout: fc_discuss_archives title: Message 31 from Frama-C-discuss on January 2014 ---
Hello, I think one way to achieve that would be to write a definition for function foo in ghost code. This definition could update a counter, or register its argument, in a global ghost variable; then you can use ACSL for stating statements on this ghost variable. Best regards, Matthieu ds.verification at flecsim.com writes: > 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