--- layout: fc_discuss_archives title: Message 27 from Frama-C-discuss on May 2015 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Assign clauses with ghost variables



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