--- layout: fc_discuss_archives title: Message 8 from Frama-C-discuss on November 2010 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] beginners problem - pointer swap example



> Although it is precise for the values contained in the variables
> during execution, it cannot tell you that the post-condition is
> satisfied in this execution because it does not handle the \old
> construct.

By the way, making sure the value analysis concludes that this
post-condition is satisfied during the execution of this program is
one of the tasks that one could tackle as part of this post-doctoral
position : http://frama-c.com/download/postdoc_interpretation_ACSL.pdf

Or someone could just do it and release their patch under a license
that allows us to integrate it, in the spirit of Free and Open Source
Software.

Pascal