If a composite type has a declared invariant, and some of its compoents are of
types that have their own invariants, the invariant checks on those compoents
must be added to the invariant checks for the enclosing type.
The command;
gnatmake -q -gnat12 -gnata test_bars
test_bars
must yield:
chart invariant violation detected
value invariant violation detected
with Ada.Assertions; use Ada.Assertions;
with Bars; use Bars;
with Text_IO; use Text_IO;
procedure Test_Bars is
B : Bar_chart := Bare_Bar (5);
D : Data (1 .. 5) := (20, 20, 20, 20, 19);
begin
begin
Assemble (D, B);
exception
when Assertion_Error => Put_Line ("chart invariant violation detected");
end;
declare
D : Data (1 .. 5) := (30, 30, 30, 30, -20);
begin
Assemble (D, B);
exception
when Assertion_Error => Put_Line ("value invariant violation detected");
end;
end;
---
package Bars is
type Value is private
with Invariant => Legal (Value);
type Bar_Chart (<>) is private
with Invariant => Complete (Bar_Chart);
type Data is array (positive range <>) of Integer;
function Legal (It : Value) return Boolean;
function Complete (It : Bar_Chart) return Boolean;
function Bare_Bar (N : Positive) return Bar_Chart;
procedure Assemble (From : Data; Result : out Bar_Chart);
private
type Value is new Integer;
type Bar_Chart is array (positive range <>) of Value;
end;
---
package body Bars is
-- type Value is private
-- with Invariant => Legal (Value);
-- type Bar_Chart is private
-- with Invariant => Complete (Bar_Chart);
function Legal (It : Value) return Boolean is
begin
return It >= 0 and It <= 100;
end;
function Complete (It : Bar_Chart) return Boolean is
Total : Value := 0;
begin
for B of It loop Total := Total + B; end loop;
return Total = 100;
end;
function Bare_Bar (N : Positive) return Bar_Chart is
Result : Bar_Chart (1 .. N) := (100, others => 0);
begin
return Result;
end;
procedure Assemble (From : Data; Result : out Bar_Chart) is
begin
for J in From'range loop
Result (J) := Value (From (J));
end loop;
end;
end;
Tested on x86_64-pc-linux-gnu, committed on trunk
2012-10-01 Ed Schonberg <schonb...@adacore.com>
* exp_ch3.ads (Build_Array_Invariant_Proc): moved to body.
* exp_ch3.adb (Build_Array_Invariant_Proc,
Build_Record_Invariant_Proc): transform into functions.
(Insert_Component_Invariant_Checks): for composite types that have
components with specified invariants, build a checking procedure,
and make into the invariant procedure of the composite type,
or incorporate it into the user- defined invariant procedure if
one has been created.
* sem_ch3.adb (Array_Type_Declaration): Checking for invariants
on the component type is defered to the expander.
Index: exp_ch3.adb
===================================================================
--- exp_ch3.adb (revision 191902)
+++ exp_ch3.adb (working copy)
@@ -88,6 +88,22 @@
-- used for attachment of any actions required in its construction.
-- It also supplies the source location used for the procedure.
+ function Build_Array_Invariant_Proc
+ (A_Type : Entity_Id;
+ Nod : Node_Id) return Node_Id;
+ -- If the component of type of array type has invariants, build procedure
+ -- that checks invariant on all components of the array. Ada 2012 specifies
+ -- that an invariant on some type T must be applied to in-out parameters
+ -- and return values that include a part of type T. If the array type has
+ -- an otherwise specified invariant, the component check procedure is
+ -- called from within the user-specified invariant. Otherwise this becomes
+ -- the invariant procedure for the array type.
+
+ function Build_Record_Invariant_Proc
+ (R_Type : Entity_Id;
+ Nod : Node_Id) return Node_Id;
+ -- Ditto for record types.
+
function Build_Discriminant_Formals
(Rec_Id : Entity_Id;
Use_Dl : Boolean) return List_Id;
@@ -118,10 +134,6 @@
-- Build record initialization procedure. N is the type declaration
-- node, and Rec_Ent is the corresponding entity for the record type.
- procedure Build_Record_Invariant_Proc (R_Type : Entity_Id; Nod : Node_Id);
- -- If the record type has components whose types have invariant, build
- -- an invariant procedure for the record type itself.
-
procedure Build_Slice_Assignment (Typ : Entity_Id);
-- Build assignment procedure for one-dimensional arrays of controlled
-- types. Other array and slice assignments are expanded in-line, but
@@ -184,6 +196,14 @@
-- Treat user-defined stream operations as renaming_as_body if the
-- subprogram they rename is not frozen when the type is frozen.
+ procedure Insert_Component_Invariant_Checks
+ (N : Node_Id;
+ Typ : Entity_Id;
+ Proc : Node_Id);
+ -- If a composite type has invariants and also has components with defined
+ -- invariants. the component invariant procedure is inserted into the user-
+ -- defined invariant procedure and added to the checks to be performed.
+
procedure Initialization_Warning (E : Entity_Id);
-- If static elaboration of the package is requested, indicate
-- when a type does meet the conditions for static initialization. If
@@ -788,7 +808,10 @@
-- Build_Array_Invariant_Proc --
--------------------------------
- procedure Build_Array_Invariant_Proc (A_Type : Entity_Id; Nod : Node_Id) is
+ function Build_Array_Invariant_Proc
+ (A_Type : Entity_Id;
+ Nod : Node_Id) return Node_Id
+ is
Loc : constant Source_Ptr := Sloc (Nod);
Object_Name : constant Name_Id := New_Internal_Name ('I');
@@ -882,9 +905,7 @@
Proc_Id :=
Make_Defining_Identifier (Loc,
- Chars => New_External_Name (Chars (A_Type), "Invariant"));
- Set_Has_Invariants (Proc_Id);
- Set_Invariant_Procedure (A_Type, Proc_Id);
+ Chars => New_External_Name (Chars (A_Type), "CInvariant"));
Body_Stmts := Check_One_Dimension (1);
@@ -912,10 +933,7 @@
Set_Debug_Info_Off (Proc_Id);
end if;
- -- The procedure body is placed after the freeze node for the type.
-
- Insert_After (Nod, Proc_Body);
- Analyze (Proc_Body);
+ return Proc_Body;
end Build_Array_Invariant_Proc;
--------------------------------
@@ -3619,7 +3637,10 @@
-- Build_Record_Invariant_Proc --
--------------------------------
- procedure Build_Record_Invariant_Proc (R_Type : Entity_Id; Nod : Node_Id) is
+ function Build_Record_Invariant_Proc
+ (R_Type : Entity_Id;
+ Nod : Node_Id) return Node_Id
+ is
Loc : constant Source_Ptr := Sloc (Nod);
Object_Name : constant Name_Id := New_Internal_Name ('I');
@@ -3745,19 +3766,16 @@
then
Stmts := Build_Invariant_Checks (Component_List (Type_Def));
else
- return;
+ return Empty;
end if;
if not Invariant_Found then
- return;
+ return Empty;
end if;
Proc_Id :=
Make_Defining_Identifier (Loc,
Chars => New_External_Name (Chars (R_Type), "Invariant"));
- Set_Has_Invariants (Proc_Id);
- Set_Has_Invariants (R_Type);
- Set_Invariant_Procedure (R_Type, Proc_Id);
Proc_Body :=
Make_Subprogram_Body (Loc,
@@ -3779,10 +3797,9 @@
Set_Is_Internal (Proc_Id);
Set_Has_Completion (Proc_Id);
- -- The procedure body is placed after the freeze node for the type.
-
- Insert_After (Nod, Proc_Body);
- Analyze (Proc_Body);
+ return Proc_Body;
+ -- Insert_After (Nod, Proc_Body);
+ -- Analyze (Proc_Body);
end Build_Record_Invariant_Proc;
----------------------------
@@ -5843,7 +5860,11 @@
end if;
if Has_Invariants (Component_Type (Base)) then
- Build_Array_Invariant_Proc (Base, N);
+
+ -- Generate component invariant checking procedure.
+
+ Insert_Component_Invariant_Checks
+ (N, Base, Build_Array_Invariant_Proc (Base, N));
end if;
end Expand_Freeze_Array_Type;
@@ -6812,9 +6833,11 @@
end;
end if;
- if not Has_Invariants (Def_Id) then
- Build_Record_Invariant_Proc (Def_Id, N);
- end if;
+ -- Check whether individual components have a defined invariant,
+ -- and add the corresponding component invariant checks.
+
+ Insert_Component_Invariant_Checks
+ (N, Def_Id, Build_Record_Invariant_Proc (Def_Id, N));
end Expand_Freeze_Record_Type;
------------------------------
@@ -7579,6 +7602,63 @@
return Is_RTU (S1, System) or else Is_RTU (S1, Ada);
end In_Runtime;
+ ---------------------------------------
+ -- Insert_Component_Invariant_Checks --
+ ---------------------------------------
+
+ procedure Insert_Component_Invariant_Checks
+ (N : Node_Id;
+ Typ : Entity_Id;
+ Proc : Node_Id)
+ is
+ Loc : constant Source_Ptr := Sloc (Typ);
+ Proc_Id : Entity_Id;
+
+ begin
+ if Present (Proc) then
+ Proc_Id := Defining_Entity (Proc);
+
+ if not Has_Invariants (Typ) then
+ Set_Has_Invariants (Typ);
+ Set_Has_Invariants (Proc_Id);
+ Set_Invariant_Procedure (Typ, Proc_Id);
+ Insert_After (N, Proc);
+ Analyze (Proc);
+
+ else
+
+ -- Find already created invariant body, insert body of component
+ -- invariant proc in it, and add call after other checks.
+
+ declare
+ Bod : Node_Id;
+ Inv_Id : constant Entity_Id := Invariant_Procedure (Typ);
+ Call : constant Node_Id :=
+ Make_Procedure_Call_Statement (Loc,
+ Name => New_Occurrence_Of (Proc_Id, Loc),
+ Parameter_Associations =>
+ New_List
+ (New_Reference_To (First_Formal (Inv_Id), Loc)));
+
+ begin
+
+ -- The invariant body has not been analyzed yet, so we do a
+ -- sequential search forward, and retrieve it by name.
+
+ Bod := Next (N);
+ while Present (Bod) loop
+ exit when Nkind (Bod) = N_Subprogram_Body
+ and then Chars (Defining_Entity (Bod)) = Chars (Inv_Id);
+ Next (Bod);
+ end loop;
+
+ Append_To (Declarations (Bod), Proc);
+ Append_To (Statements (Handled_Statement_Sequence (Bod)), Call);
+ end;
+ end if;
+ end if;
+ end Insert_Component_Invariant_Checks;
+
----------------------------
-- Initialization_Warning --
----------------------------
Index: exp_ch3.ads
===================================================================
--- exp_ch3.ads (revision 191888)
+++ exp_ch3.ads (working copy)
@@ -46,12 +46,6 @@
procedure Expand_Record_Extension (T : Entity_Id; Def : Node_Id);
-- Add a field _parent in the extension part of the record
- procedure Build_Array_Invariant_Proc (A_Type : Entity_Id; Nod : Node_Id);
- -- If the component of type of array type has invariants, build procedure
- -- that checks invariant on all components of the array. Ada 2012 specifies
- -- that an invariant on some type T must be applied to in-out parameters
- -- and return values that include a part of type T.
-
procedure Build_Discr_Checking_Funcs (N : Node_Id);
-- Builds function which checks whether the component name is consistent
-- with the current discriminants. N is the full type declaration node,
Index: sem_ch3.adb
===================================================================
--- sem_ch3.adb (revision 191898)
+++ sem_ch3.adb (working copy)
@@ -4974,12 +4974,9 @@
Subtype_Indication (Component_Def));
end if;
- -- Ada 2012: if the element type has invariants we must create an
- -- invariant procedure for the array type as well.
-
- if Has_Invariants (Element_Type) then
- Set_Has_Invariants (T);
- end if;
+ -- There may be an invariant declared for the component type, but
+ -- the construction of the component invariant checking procedure
+ -- takes place during expansion.
end Array_Type_Declaration;
------------------------------------------------------
