--- layout: fc_discuss_archives title: Message 41 from Frama-C-discuss on January 2014 ---
Hello, 2014/1/14 <ds.verification at flecsim.com>: > 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? > You might be interested in the Aora? plug-in (http://frama-c.com/download/frama-c-aorai-manual.pdf), whose main aim is to specify the sequences of function calls that can occur during the execution of a program. Such a specification is then translated into a set of ACSL contracts which have to be discharged by WP, Jessie or Value analysis (or any other plug-in that can check the validity of ACSL formulas). From what you describe, I'd say that the following automaton (not tested) should do the trick: %init: Init; %accept: OK; %deterministic; Init: { CALL(test1) } -> FOO; FOO: { foo() } -> OK | { RETURN(test1) } -> KO | other -> FOO; OK: -> OK; KO: -> KO; Note that Aora?'s current version only considers defined functions, so that you'd have to provide a dummy body for foo in order to use this plugin. Best regards, -- E tutto per oggi, a la prossima volta Virgile