--- layout: fc_discuss_archives title: Message 125 from Frama-C-discuss on November 2013 ---
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?