--- layout: fc_discuss_archives title: Message 42 from Frama-C-discuss on January 2014 ---
Hi Virgile, that's an interesting idea. However, i think it is a bit over-complicated at least for a single call - if there are long chains of calls to be checked for a definite ordering, i'd agree. Disadvantage is that this introduces yet another tool/spec language (which had to be communicated)... Thanks Daniel Virgile Prevosto schrieb am 16.01.2014 09:38: > 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 > > _______________________________________________ > 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