--- layout: fc_discuss_archives title: Message 8 from Frama-C-discuss on November 2010 ---
> 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