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] 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: moy at adacore.com (Yannick Moy)
  • Date: Thu, 08 Dec 2011 11:37:57 +0100
  • In-reply-to: <CAC3Lx=Y-vLYLcqaWCBrTnTf10VtqqDORrV9eeXkhqYt-gy+-HA@mail.gmail.com>
  • References: <CAC3Lx=aPPQOx6_pVXvyvy2qwCmzTPK8iJpk8rqR05R=Dr7AVbA@mail.gmail.com> <4EDF715E.5010601@cea.fr> <CAC3Lx=Y-vLYLcqaWCBrTnTf10VtqqDORrV9eeXkhqYt-gy+-HA@mail.gmail.com>
On 12/07/2011 03:36 PM, David MENTRE wrote:

> Anyway, I'm just curious on how other people are using strong invariants.

Hi David,

Ada 2012 provides an interesting notion of strong invariants, that is only
checked at certain program points: after object creation, when converting to the
type, when passing an object as input parameter, or returning it as output
parameter.

See http://www.ada-auth.org/standards/12rm/html/RM-3-2-4.html#I1430 for more
details on this "subtype predicate" feature. Here is an implementation of your
code that uses it:

---
procedure P is
   type T is record
      Access_Count : Natural := 0;
      Locked       : Boolean := False;
   end record with
     Predicate => (T.Locked = (T.Access_Count > 3));

   procedure Bad (V : in out T) is
   begin
      V.Access_Count := V.Access_Count + 1;
      V.Locked := True;
   end Bad;

   Var : T;  --  predicate checked at object creation
begin
   --  predicate checked when passing Var as input
   Bad (Var);
   --  predicate checked when returning Var as output
end P;
---

Just compile the code above with assertions (-gnata):

$ gcc -c -gnat12 -gnata p.adb
$ gnatbind p
$ gnatlink p
$ ./p

and at run-time you get the error (placed on Bad declaration because the check
is done inside Bad code for both inputs and outputs):

raised SYSTEM.ASSERTIONS.ASSERT_FAILURE : predicate failed at p.adb:8

Ada 2012 also has a notion of weak invariants, that only applies to private
types defined in a package, and which are checked only on public subprograms
defined in this package, on output parameters of the type.

See http://www.ada-auth.org/standards/12rm/html/RM-7-3-2.html for all details.
Here is your code using a type invariant:

--- p.ads
package P is
   type T is private;
   procedure Bad (V : in out T);
private
   type T is record
      Access_Count : Natural := 0;
      Locked       : Boolean := False;
   end record with
     Predicate => (T.Locked = (T.Access_Count > 3));
end P;
--- p.adb
package body P is
   procedure Bad (V : in out T) is
   begin
      V.Access_Count := V.Access_Count + 1;
      V.Locked := True;
   end Bad;
end P;
--- main.adb
with P; use P;
procedure Main is
   Var : T;
begin
   Bad (Var);
end Main;
--- test.gpr
project Test is
  for Main use ("main.adb");
  package Compiler is
      for Default_Switches ("Ada") use ("-gnat12", "-gnata");
  end Compiler;
end Test;
---

Compile the code using the project file above:

$ gnatmake -P test
$ ./main

and you get a run-time exception:

raised SYSTEM.ASSERTIONS.ASSERT_FAILURE : predicate failed at p.adb:2

Of course, we plan to be able to prove both uses of subtypes predicates and type
invariants statically with the tool gnatprove.

Best regards,
-- 
Yannick