--- layout: fc_discuss_archives title: Message 28 from Frama-C-discuss on May 2015 ---
Hi, The use of the nonfree ACSL importer plug-in is the industrial solution to that scoping problem. It solves most of the real industrial needs since industrials use naming rules. In your example, an alternative based on the merge of several contracts done by Frama-C tool could help ; but that functionality is undocumented : Just add //@assigns the_state; in your C source file between line static int the_state = 0; and void set_state(int val) { Then, Frama-C tool will generate the clause //@assigns the_state, gState; for the contract of the function set_state. As you see, there are some ways to solve that kind of problems for the use and deployment of Frama-C in industrial contexts. Patrick. Le 28/05/2015 09:28, Frank Dordowsky a ?crit : > Thank you for the explanation. But I then have a follow on: How can > you handle variables of file scope in general? To be more specific: > > 1. separate header and source (.c) file > 2. header contains declaration of a function with assign clauses in > ACSL annotations > 3. definition of function in the source file modifies variable of file > scope not listed in the assigns clause because not visible in the > header. > > What is the best way to handle this situation with assigns clauses? > Has it been discussed somewhere else (pointer welcome) > > Thanks in advance > Frank >