--- layout: fc_discuss_archives title: Message 37 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?



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