--- layout: fc_discuss_archives title: Message 49 from Frama-C-discuss on November 2008 ---
Hallo Christoph, Le mar 18 nov 2008 09:14:03 CET, "Christoph Weber" <Christoph.Weber@first.fraunhofer.de> a ?crit : > void out_char(char c) > { > int col = 0; > //@ global invariant I : 0 <= col <= 79; > col++; > if (col >= 80) col = 0; > } There is indeed a mistake in acsl-implementation.pdf. In the current implementation, global invariants can only be specified as global specification, not inside a block of code. In addition, such a global invariant could only refer to local variables that are static(1), as is the case in the example 2.42, but not in the code above. There would be little point in stating a "global invariant" that would depend on local variables whose existence is limited to a function execution (especially for a weak global invariant which is checked only at the entrance and exit of functions). There is currently no way to express an invariant on local variables that has to be verified at each point statement (short of writing assert annotations everywhere). Anyway, thanks for your feedback. I hope that the situation is a bit clearer now. Regards, -- E tutto per oggi, a la prossima volta. Virgile (1) As any global invariant, it can also refer to global variables of course.