--- layout: fc_discuss_archives title: Message 31 from Frama-C-discuss on May 2015 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Assign clauses with ghost variables



-- Virgile Prevosto (2015-05-28)
> 
> You're perfectly right, we lack an option of an abstract memory region
> (and probably some separation formulas saying that the visible part of
> the memory is separated from it).

Or you make this the default, when you define the semantics of these new "abstract state" variables. FWIW, it's how it's done in SPARK: the abstract state of a package can only represent the concrete state defined in the private part and body of the package.

> This shows up for static variables
> C, but would be much more widespread for private members of C++
> classes.

You could then allow defining these abstract state variable for a given file, or a given C++ class (for its static private members).
--
Yannick Moy, Senior Software Engineer, AdaCore




-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20150528/3ea52098/attachment.html>