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: Claude.Marche at inria.fr (Claude Marché)
  • Date: Tue Nov 18 17:40:09 2008
  • In-reply-to: <20081118105028.43944c37@is005115>
  • References: <5501DEB6D1BA4B4E8DF1E885137E4DB5@AHARDPLACE> <20081118105028.43944c37@is005115>

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                    |