--- layout: fc_discuss_archives title: Message 62 from Frama-C-discuss on February 2011 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Ghost variables and function prototypes



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