--- layout: fc_discuss_archives title: Message 29 from Frama-C-discuss on January 2014 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Can i specify/proove a function to be "just called"?



Hi,

You should add assign clause for function foo

/*@ assigns \nothing; */
extern void foo(int val);


On 14 January 2014 19:38,  <ds.verification at flecsim.com> wrote:
> 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