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

On 01/11/2011 11:22 AM, Boris Hollas wrote:
> 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?
>    

To tell the complete story: indeed yes, an experimental ownership-based 
type invariants
exists in the current Jessie. This is not secret, and indeed appears in 
the doc: see pragma InvariantPolicy
and its parameter "ownership" (use it at your own risks!)

The point is that we were not satisfied by the results, in particular 
because we had to adapt the approach
to the burstall-bornat memory model of Jessie (which is different from 
the one of Spec# and VCC), which complicated
too much the VCs. Also a lot of additional manual annotations were 
required (it seems that Spec# implements heuristics to
discharge such a task more or less automatically)

The current plan is to consider alternative approaches, for which we 
believe VCs will be simpler. But as I said before, it will not be 
implemented in the current Jessie/why 2.xx.

> 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?
>    

You're perfectly right. We already discussed about such an option in the 
"ACSL designing team". We agreed
that it would be a good compromise. But I'm afraid that because of the 
lack of demand, this remained only a plan for the future.

May be the designers of the WP plugin have plans to go further in this 
direction soon?

- Claude

-- 
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                    |