--- layout: fc_discuss_archives title: Message 21 from Frama-C-discuss on December 2011 ---
Hello David, On 12/07/2011 12:24 PM, David MENTRE wrote: > What is the current status of global variable invariant ("//@ global > invariant ..." notation) in Frama-C? > > From what I have gathered for Nitrogen release: > * ACSL: supported, defined in ACSL documentation; > > * Jessie: Not supported, according to ?5.2.3; > > * WP: Not supported, according to a warning printed on console; > > * Value Analysis: Not supported? (a warning is printed on console > "warning: ignoring status of global invariant ...") Actually this warning is emitted by the Frama-C kernel, not by Value Analysis. Global invariants are correctly parsed and typed by Frama-C, but it is not possible yet to assign them a validity status. > Is there any plan to support global invariant in future releases[1]? It could be fully supported by the kernel in Frama-C Oxygen or Frama-C Fluorine, but it is not 100% guarantee. For the above plug-ins, I don't know what is planned. > Global invariant seems to me quite important to ensure correctness of > a software (for safety or security properties). > > What are current work-arounds with Nitrogen? The only possibility I > can think of is to #define the property and add it as pre- and > post-conditions to all the functions of a module (with appropriate > option to preprocess annotations). Cumbersome to say the least. ;-) Boris Hollas' workaround is correct for weak invariants but not for strong invariant: in this last case, you have to insert a corresponding annotation at each sequence point of your program (see ACSL Reference Manual, Section 2.11). Definitively cumbersome to do such a task manually, but writing a small plug-ins in order to insert these annotations should be a not-so-much amount of work. Best regards, Julien