--- layout: fc_discuss_archives title: Message 125 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?



The ACSL importer plug-in (used to import external ACSL file) takes care 
of that situation.
Unfortunately, this plugin isn't free.
Without it, your code have to be transformed.

Patrick.

Le 27/11/2013 10:30, David MENTRE wrote:
> At work we have a situation where we want to use C static variables
> (variables visible only to a C file) to hide some internal state of a
> module. However, we have an issue with the assigns clause: as this
> variable is private to the module, it is not visible outside it and
> thus cannot be used in the assigns clause of calling functions. But
> those calling functions needs nonetheless to refer to it, otherwise
> the assigns clause is not proved. How would you handle this properly
> in Frama-C?