Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] type invariants

  • Subject: [Frama-c-discuss] type invariants
  • From: virgile.prevosto at cea.fr (Virgile Prevosto)
  • Date: Tue Nov 18 10:51:01 2008
  • In-reply-to: <5501DEB6D1BA4B4E8DF1E885137E4DB5@AHARDPLACE>
  • References: <5501DEB6D1BA4B4E8DF1E885137E4DB5@AHARDPLACE>
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.