Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

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

  • Subject: [Frama-c-discuss] Ghost variables and function prototypes
  • From: hollas at informatik.htw-dresden.de (Boris Hollas)
  • Date: Mon, 21 Feb 2011 14:48:35 +0100 (CET)
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