--- layout: fc_discuss_archives title: Message 31 from Frama-C-discuss on May 2015 ---
-- 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>