--- layout: fc_discuss_archives title: Message 65 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, 2011-02-18 at 15:56 +0100, Pascal Cuoq wrote:
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.
>
In the example I've given, the verification is unsound if the user doesn't
provide a correct assign clause for the function prototype. If only the
prototype is know, it's not possible to have a plug-in generate an assigns
clauses for the function. In this case, the function may modify anything
in global namespace, including ghost variables. Does Jessie assume this in
the absence of an (explicit or generated) assign clause?
-- 
Regards,
Boris