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 Wed, 2011-01-12 at 13:12 +0100, Claude Marche wrote:
> 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!)

>From my, albeit limited, experience with embedded C-code, which is one
of the major applications of this language, I can tell that complex
object structures, as discussed in the first paper you cited, are rare.
C code usually has a flat structure, although much of it could be
refactored into a hierarchy of aggregate classes. Complex data
structures such a linked lists or trees that require dynamic memory
management are avoided or not allowed to fulfill coding rules.
Therefore, I believe that there's little use for complex class
invariants, at least for embedded C-code. For system code, the situation
may be different. Eg, dynamic data structures are used a lot in the
Hypervisor kernel.

On the other hand, there are more important challenges than complex
class invariants or those discussed in the second paper you cited for
embedded code. Eg, there's little research on the functional
verification of code for hybrid (mixed discrete & continuous) systems.
That means there's always something you'd like to verify but it can't be
expressed in the specification language.

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

With a few exceptions, you have to introduce lots of expose-blocks in
Spec# if you use aggregate classes and you have to specify ownership.
There's some automatism in the ownership system, though. Anyway, it
doesn't may verification easier for users, as even KRML admits.

Dafny, KRML's latest invention, uses a different approach to type
invariants.

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

Number types with a restricted range are quite common in embedded code
and preservation of ranges is given much focus in testing. Therefore, I
believe that invariants for primitive types would be useful and reduce
annotation overhead compared to the workaround solution.
-- 
Regards,
Boris