--- layout: fc_discuss_archives title: Message 65 from Frama-C-discuss on February 2011 ---
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