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

Hello Claude,

I'll have a look at the papers you cited. I know the problems that OO
introduces wrt type class invariants. Is it planned to introduce
ownership-based type invariants that can span over several struct types?
Eg,

typedef struc {
  int b;
} B;

typedef struc {
  int a;
  B b;
} A;
//@ type_invariant(A *this) = this->B.b == this a;

Invariants of this kind are allowed in Spec# and VCC. Major drawbacks
are that 
- the handling of type invariants is very difficult
- the whole verification language is centered around the invariant
concept, which complicates the verification even of programs that don't
use any invariants.

The workaround you proposed is the approach used in Havoc 0.1 for type
invariants. Havoc allows to specify pre- and postconditions that shall
hold for all functions that have a parameter of the specified type, or
for all locations in which a variable of the specified type is accessed.
That way, you can mimick weak or strong type invariants in the ACSL
sense.

Would it also be difficult to implement weak type invariants that are
limited to one type only, eg a range of type int that shall not exceed
its limits?
-- 
Regards,
Boris