---
layout: fc_discuss_archives
title: Message 42 from Frama-C-discuss on December 2011
---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[Frama-c-discuss] Status of global invariant in Jessie, WP and Value Analysis?
- Subject: [Frama-c-discuss] Status of global invariant in Jessie, WP and Value Analysis?
- From: dmentre at linux-france.org (David MENTRE)
- Date: Fri, 9 Dec 2011 15:22:06 +0100
- In-reply-to: <4EE09385.9040506@adacore.com>
- References: <CAC3Lx=aPPQOx6_pVXvyvy2qwCmzTPK8iJpk8rqR05R=Dr7AVbA@mail.gmail.com> <4EDF715E.5010601@cea.fr> <CAC3Lx=Y-vLYLcqaWCBrTnTf10VtqqDORrV9eeXkhqYt-gy+-HA@mail.gmail.com> <4EE09385.9040506@adacore.com>
Hello Yannick,
2011/12/8 Yannick Moy <moy at adacore.com>:
> Of course, we plan to be able to prove both uses of subtypes predicates and type
> invariants statically with the tool gnatprove.
That's interesting! I cannot comment on the practical use of the
different kind of invariants you have shown.