--- layout: fc_discuss_archives title: Message 52 from Frama-C-discuss on November 2008 ---
Virgile Prevosto wrote: > 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). Not quite true: //@ strong invariant .... is supposed to have this semantics. But it isn't implemented yet... > Anyway, thanks for your feedback. I hope that the situation is a bit > clearer now. > > Regards, -- Claude March? | tel: +33 1 72 92 59 69 INRIA Saclay - ?le-de-France | mobile: +33 6 33 14 57 93 Parc Orsay Universit? | fax: +33 1 74 85 42 29 4, rue Jacques Monod - B?timent N | http://www.lri.fr/~marche/ F-91893 ORSAY Cedex |