--- layout: fc_discuss_archives title: Message 129 from Frama-C-discuss on November 2013 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Information hiding: how to handle module's private static variables in Frama-C?



-- David MENTRE (2013-11-27)
> 
> 
>> I think that Frama-C and ACSL should natively incorporate some of these
>> ideas, but as of yet, they do not.
> 
> Yes. B Method and SPARK 2014 probably have an advantage in this
> regard. For example, SPARK 2014 has a mechanism to abstract some
> internal module variables into abstract ones (see
> http://www.spark-2014.org/entries/detail/spark-2014-rationale-global-state).
> But I haven't played with this mechanism so I don't know how useful it
> is in practice.

Hi David,

It is a critical feature for current SPARK industrial users, to solve the scalability issue: when you have dozens or hundreds of global variables in different parts of your program, you want to be able to refer to them abstractly in the specifications, and it can also make a difference for the efficiency of the underlying analysis/proof tools.
--
Yannick Moy, Senior Software Engineer, AdaCore