--- layout: fc_discuss_archives title: Message 62 from Frama-C-discuss on February 2011 ---
On Fri, Feb 18, 2011 at 3:07 PM, Boris Hollas <hollas at informatik.htw-dresden.de> wrote: > In the following code, I use a ghost variable foo_result to express a > specification on the return value of function foo. If I don't specify > assigns foo_result; in the contract of foo, the code verifies. See the discussion at http://bts.frama-c.com/view.php?id=615 > However, shouldn't Jessie automatically deduce from foo's postcondition > that foo may modify foo_result? Why should it do that? If the postcondition was x == y, should it deduce that the function assigns x, assigns y, assigns both, or assigns none but has a precondition that implies that x is already equal to y when it is called? Our position on generated assigns clauses is: if you don't like them, write assigns clauses by hand or write your own plug-in that generates assigns clauses for functions that do not have them. Pascal