--- layout: fc_discuss_archives title: Message 27 from Frama-C-discuss on May 2015 ---
Hello, Le 28/05/2015 09:28, Frank Dordowsky a ?crit : > 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) In my humble opinion, there is lack of abstraction of Frama-C in such situations. You need to mention every modified variable in contracts, even those that you would like to be hidden. For example, I see no way to use static variables (variable local to a file, but if used should be mentioned in contract therefore seen from outside!). Best regards, david