This is the mail archive of the gcc-patches@gcc.gnu.org mailing list for the GCC project.
| Index Nav: | [Date Index] [Subject Index] [Author Index] [Thread Index] | |
|---|---|---|
| Message Nav: | [Date Prev] [Date Next] | [Thread Prev] [Thread Next] |
| Other format: | [Raw text] | |
This patch reimplements the processing of type invariants in order to plug
various static and run-time semantic holes. The invariants of a private type
are resolved and checked at run-time by a "partial" invariant procedure. The
invariants of a private type's full view, any inherited class-wide invariants
of parent types or interfaces, any invariants on array elements or record
components, and the invariants of the partial view are resolved and checked at
run-time by a "full" invariant procedure.
------------
-- Source --
------------
-- tester.ads
package Tester is
type Type_Id is
(Ext_1_Id,
Ext_1_FV_Id,
Ext_2_Id,
Ext_3_Id,
Ext_4_Id,
Ext_4_FV_Id,
Ext_5_Id,
Ext_6_Id,
Ext_6_FV_Id,
Ext_7_Id,
Ext_8_Id,
Iface_1_Id,
Iface_2_Id,
Iface_3_Id,
Iface_4_Id,
Par_1_Id,
Par_2_FV_Id,
Par_3_Id,
Par_4_Id,
Par_4_FV_Id,
Prot_1_FV_Id,
Prot_2_Id,
Prot_3_Id,
Prot_3_FV_Id,
Synch_1_Id,
Synch_2_Id,
Tag_1_Id,
Tag_2_Id,
Tag_3_Id,
Tag_4_Id,
Tag_4_FV_Id,
Tag_5_Id,
Tag_6_Id,
Tag_7_Id,
Tag_8_Id,
Tag_9_Id,
Tag_10_Id,
Tag_11_Id,
Tag_12_Id,
Tag_13_Id,
Tag_14_Id,
Tag_15_Id,
Tag_15_FV_Id,
Tag_16_Id,
Tag_17_Id,
Tag_18_Id,
Tag_19_Id,
Tag_20_Id,
Tag_20_FV_Id,
Tag_21_Id,
Tag_22_Id,
Tag_23_Id,
Tag_24_Id,
Tag_24_FV_Id,
Tag_25_Id,
Tag_26_Id,
Tag_27_Id,
Tag_28_Id,
Task_1_Id,
Task_2_Id,
Task_2_FV_Id,
Untag_1_Id,
Untag_2_Id,
Untag_3_Id,
Untag_4_Id,
Untag_5_Id,
Untag_6_Id,
Untag_7_Id,
Untag_8_Id,
Untag_9_Id);
type Results is array (Type_Id) of Boolean;
function Mark (Typ : Type_Id) return Boolean;
-- Mark the result for a particular type as verified. The function always
-- returns True.
procedure Reset_Results;
-- Reset the internally kept result state
procedure Test_Results (Test_Id : String; Exp : Results);
-- Ensure that the internally kept result state agrees with expected
-- results Exp. Emit an error if this is not the case.
end Tester;
-- tester.adb
with Ada.Text_IO; use Ada.Text_IO;
package body Tester is
State : Results;
----------
-- Mark --
----------
function Mark (Typ : Type_Id) return Boolean is
begin
State (Typ) := True;
return True;
end Mark;
-------------------
-- Reset_Results --
-------------------
procedure Reset_Results is
begin
State := (others => False);
end Reset_Results;
------------------
-- Test_Results --
------------------
procedure Test_Results (Test_Id : String; Exp : Results) is
Exp_Val : Boolean;
Posted : Boolean := False;
State_Val : Boolean;
begin
for Index in Results'Range loop
Exp_Val := Exp (Index);
State_Val := State (Index);
if State_Val /= Exp_Val then
if not Posted then
Posted := True;
Put_Line (Test_Id & ": ERROR");
end if;
Put_Line (" Expected: " & Exp_Val'Img & " for " & Index'Img);
Put_Line (" Got: " & State_Val'Img);
end if;
end loop;
if not Posted then
Put_Line (Test_Id & ": OK");
end if;
end Test_Results;
end Tester;
-- invariants_aspects.ads
with Tester; use Tester;
package Invariants_Aspects is
----------------
-- Interfaces --
----------------
type Iface_1 is interface
with Type_Invariant'Class => Mark (Iface_1_Id);
type Iface_2 is interface
with Type_Invariant'Class => Mark (Iface_2_Id);
type Iface_3 is interface and Iface_1 and Iface_2;
type Iface_4 is interface and Iface_3
with Type_Invariant'Class => Mark (Iface_4_Id);
type Synch_1 is synchronized interface
with Type_Invariant'Class => Mark (Synch_1_Id);
type Synch_2 is synchronized interface and Synch_1
with Type_Invariant'Class => Mark (Synch_2_Id);
------------------
-- Tagged types --
------------------
type Tag_1 is tagged private;
type Tag_2 is tagged private;
type Tag_3 is tagged private
with Type_Invariant => Mark (Tag_3_Id);
type Tag_4 is tagged private
with Type_Invariant'Class => Mark (Tag_4_Id);
-- Derivations without invariants
type Tag_5 is new Tag_2 with private;
type Tag_6 is new Tag_3 with private;
type Tag_7 is new Tag_4 with private;
-- Derivations with invariants on the full view
type Tag_8 is new Tag_2 with private;
type Tag_9 is new Tag_3 with private;
type Tag_10 is new Tag_4 with private;
-- Derivations with invariants
type Tag_11 is new Tag_2 with private
with Type_Invariant => Mark (Tag_11_Id);
type Tag_12 is new Tag_3 with private
with Type_Invariant => Mark (Tag_12_Id);
type Tag_13 is new Tag_4 with private
with Type_Invariant => Mark (Tag_13_Id);
-- Derivations with class-wide invariants
type Tag_14 is new Tag_2 with private
with Type_Invariant'Class => Mark (Tag_14_Id);
type Tag_15 is new Tag_3 with private
with Type_Invariant'Class => Mark (Tag_15_Id);
type Tag_16 is new Tag_4 with private
with Type_Invariant'Class => Mark (Tag_16_Id);
-- Derivations with interfaces
type Tag_17 is new Tag_1 and Iface_1 and Iface_2
and Iface_3 and Iface_4 with private;
type Tag_18 is new Tag_6 and Iface_1 and Iface_4 with private;
type Tag_19 is new Tag_10 and Iface_2 and Iface_3 with private
with Type_Invariant => Mark (Tag_19_Id);
type Tag_20 is new Tag_11 and Iface_4 with private
with Type_Invariant'Class => Mark (Tag_20_Id);
-- Derivations with a hidden parent
type Tag_21 is tagged private;
type Tag_22 is tagged private;
type Tag_23 is tagged private
with Type_Invariant => Mark (Tag_23_Id);
type Tag_24 is tagged private
with Type_Invariant'Class => Mark (Tag_24_Id);
-- Derivations with more derived parents
type Tag_25 is new Tag_4 with private;
type Tag_26 is new Tag_3 with private;
type Tag_27 is new Tag_2 with private
with Type_Invariant => Mark (Tag_27_Id);
type Tag_28 is new Tag_4 with private
with Type_Invariant'Class => Mark (Tag_28_Id);
-- Parents of extensions
type Par_1 (Discr_1 : Boolean) is tagged private;
type Par_2 is tagged private;
type Par_3 is tagged private
with Type_Invariant => Mark (Par_3_Id);
type Par_4 (Discr_1 : Boolean) is tagged private
with Type_Invariant'Class => Mark (Par_4_Id);
-- Extensions
type Ext_1 is new Par_1 with private;
type Ext_2 is new Par_1 with private
with Type_Invariant => Mark (Ext_2_Id);
type Ext_3 is new Par_2 with private;
type Ext_4 is new Par_2 with private
with Type_Invariant'Class => Mark (Ext_4_Id);
type Ext_5 is new Par_3 with private
with Type_Invariant => Mark (Ext_5_Id);
type Ext_6 is new Par_3 with private;
type Ext_7 is new Par_4 with private;
type Ext_8 is new Par_4 with private
with Type_Invariant => Mark (Ext_8_Id);
-- Protected types
type Prot_1 is limited private;
type Prot_2 is limited private
with Type_Invariant => Mark (Prot_2_Id);
type Prot_3 is synchronized new Synch_2 with private
with Type_Invariant'Class => Mark (Prot_3_Id);
-- Task types
type Task_1 is limited private
with Type_Invariant => Mark (Task_1_Id);
type Task_2 is synchronized new Synch_1 with private
with Type_Invariant'Class => Mark (Task_2_Id);
--------------------
-- Untagged types --
--------------------
type Untag_1 is private;
type Untag_2 is private;
type Untag_3 is private
with Type_Invariant => Mark (Untag_3_Id);
-- Composite types with invariants carrying invariants
type Untag_4 is private;
type Untag_5 is private;
type Untag_6 is private;
type Untag_7 is private;
type Untag_8 (Discr : Boolean) is private;
type Untag_9 (<>) is private;
procedure Test_Deriv_1;
procedure Test_Deriv_2;
procedure Test_Deriv_3;
procedure Test_Deriv_4;
procedure Test_Deriv_5;
procedure Test_Sub_1;
procedure Test_Sub_2;
procedure Test_Sub_3;
procedure Test_Sub_4;
procedure Test_Sub_5;
procedure Test_Untag_9_TT;
procedure Test_Untag_9_TF;
procedure Test_Untag_9_FT;
procedure Test_Untag_9_FF;
private
type Tag_1 is tagged null record;
-- none
type Tag_2 is tagged null record
with Type_Invariant => Mark (Tag_2_Id);
-- own: Tag_2_Id
type Tag_3 is tagged null record;
-- own: Tag_3_Id
type Tag_4 is tagged null record
with Type_Invariant => Mark (Tag_4_FV_Id);
-- own: Tag_4_Id, Tag_4_FV_Id
-- inheritable: Tag_4_Id
type Tag_5 is new Tag_2 with null record;
-- none
type Tag_6 is new Tag_3 with null record;
-- none
type Tag_7 is new Tag_4 with null record;
-- inherited: Tag_4_Id
type Tag_8 is new Tag_2 with null record
with Type_Invariant => Mark (Tag_8_Id);
-- own: Tag_8_Id
type Tag_9 is new Tag_3 with null record
with Type_Invariant => Mark (Tag_9_Id);
-- own: Tag_9_Id
type Tag_10 is new Tag_4 with null record
with Type_Invariant => Mark (Tag_10_Id);
-- own: Tag_10_Id
-- inherited: Tag_4_Id
type Tag_11 is new Tag_2 with null record;
-- own: Tag_11_Id
type Tag_12 is new Tag_3 with null record;
-- own: Tag_12_Id
type Tag_13 is new Tag_4 with null record;
-- own: Tag_13_Id
-- inherited: Tag_4_Id
type Tag_14 is new Tag_2 with null record;
-- own: Tag_14_Id
type Tag_15 is new Tag_3 with null record
with Type_Invariant => Mark (Tag_15_FV_Id);
-- own: Tag_15_Id, Tag_15_FV_Id
type Tag_16 is new Tag_4 with null record;
-- own: Tag_16_Id
-- inheritable: Tag_16_Id
-- inherited: Tag_4_Id
type Tag_17 is new Tag_1 and Iface_1 and Iface_2
and Iface_3 and Iface_4 with null record;
-- inherited: Iface_1_Id, Iface_2_Id, Iface_4_Id
type Tag_18 is new Tag_6 and Iface_1 and Iface_4 with null record
with Type_Invariant => Mark (Tag_18_Id);
-- own: Tag_18_Id
-- inherited: Iface_1_Id, Iface_2_Id, Iface_4_Id
type Tag_19 is new Tag_10 and Iface_2 and Iface_3 with null record;
-- own: Tag_19_Id
-- inherited: Iface_1_Id, Iface_2_Id, Tag_4_Id
type Tag_20 is new Tag_11 and Iface_4 with null record
with Type_Invariant => Mark (Tag_20_FV_Id);
-- own: Tag_20_Id, Tag_20_FV_Id
-- inheritable: Tag_20_Id
-- inherited : Iface_1_Id, Iface_2_Id, Iface_4_Id
type Tag_21 is new Tag_15 with null record;
-- inherited: Tag_15_Id
type Tag_22 is new Tag_13 with null record
with Type_Invariant => Mark (Tag_22_Id);
-- own: Tag_22_Id
-- inherited: Tag_4_Id
type Tag_23 is new Tag_9 with null record;
-- own: Tag_23_Id
type Tag_24 is new Tag_15 with null record
with Type_Invariant => Mark (Tag_24_FV_Id);
-- own: Tag_24_Id, Tag_24_FV_Id
-- inheritable: Tag_24_Id
-- inherited: Tag_15_Id
type Tag_25 is new Tag_13 with null record;
-- inherited: Tag_4_Id
type Tag_26 is new Tag_15 with null record
with Type_Invariant => Mark (Tag_26_Id);
-- own: Tag_26_Id
-- inherited: Tag_15_Id
type Tag_27 is new Tag_14 with null record;
-- own: Tag_27_Id
-- inherited: Tag_14_Id
type Tag_28 is new Tag_13 with null record;
-- own: Tag_28_Id
-- inherited: Tag_4_Id
type Par_1 (Discr_1 : Boolean) is tagged record
Comp_1 : Tag_8; -- Tag_8_Id
case Discr_1 is
when True =>
Comp_2 : Tag_10; -- Tag_4_Id, Tag_10_Id
when others =>
Comp_3 : Tag_19; -- Iface_1_Id, Iface_2_Id, Tag_4_Id, Tag_19_Id
end case;
end record;
type Par_2 is tagged record
Comp_1 : Tag_22; -- Tag_4_Id, Tag_22_Id
Comp_2 : Tag_24; -- Tag_15_Id, Tag_24_Id, Tag_24_FV_Id
end record
with Type_Invariant => Mark (Par_2_FV_Id);
-- own: Par_2_FV_Id
-- calls: Tag_4_Id, Tag_15_Id, Tag_22_Id, Tag_24_Id, Tag_24_FV_Id
type Par_3 is tagged record
Comp_1 : Tag_1; -- none
Comp_2 : Tag_6; -- none
end record;
-- own: Par_3_Id
type Par_4 (Discr_1 : Boolean) is tagged record
case Discr_1 is
when True =>
Comp_1 : Tag_5; -- none
when others =>
Comp_2 : Tag_6; -- none
end case;
end record
with Type_Invariant => Mark (Par_4_FV_Id);
-- own: Par_4_Id, Par_4_FV_Id
-- inheritable: Par_4_Id
type Ext_1 is new Par_1 with record
Comp_4 : Tag_26; -- Tag_15_Id, Tag_26_Id
Comp_5 : Tag_20; -- Iface_1_Id, Iface_2_Id, Iface_4_Id, Tag_20_Id,
-- Tag_20_FV_Id
end record
with Type_Invariant => Mark (Ext_1_FV_Id);
-- calls: must be calculated
-- own: Ext_1_FV_Id
type Ext_2 is new Par_1 with record
Comp_4 : Tag_1; -- none
end record;
-- calls: must be calculated
-- own: Ext_2_Id
type Ext_3 is new Par_2 with record
Comp_3 : Tag_19; -- Iface_1_Id, Iface_2_Id, Tag_4_Id, Tag_19_Id
end record;
-- calls: Iface_1_Id, Iface_2_Id, Tag_4_Id, Tag_15_Id, Tag_19_Id,
-- Tag_22_Id, Tag_24_Id, Tag_24_FV_Id
type Ext_4 is new Par_2 with record
Comp_3 : Tag_14; -- Tag_14_Id
Comp_4 : Tag_25; -- Tag_4_Id
end record
with Type_Invariant => Mark (Ext_4_FV_Id);
-- calls: Tag_4_Id, Tag_14_Id, Tag_15_Id, Tag_22_Id, Tag_24_Id,
-- Tag_24_FV_Id
-- own: Ext_4_Id, Ext_4_FV_Id
-- inheritable: Ext_4_Id
type Ext_5 is new Par_3 with record
Comp_3 : Tag_18; -- Iface_1_Id, Iface_2_Id, Iface_4_Id, Tag_18_Id
end record;
-- calls: Iface_1_Id, Iface_2_Id, Iface_4_Id, Tag_18_Id
-- own: Ext_5_Id
type Ext_6 is new Par_3 with record
Comp_4 : Tag_4; -- Tag_4_Id, Tag_4_FV_Id
end record
with Type_Invariant => Mark (Ext_6_FV_Id);
-- calls: Tag_4_Id, Tag_4_FV_Id
-- own: Ext_6_FV_Id
type Ext_7 is new Par_4 with record
Comp_3 : Tag_6; -- none
Comp_4 : Tag_28; -- Tag_4_Id, Tag_28_Id
end record;
-- calls: must be calculated
type Ext_8 is new Par_4 with record
Comp_3 : Tag_20; -- Iface_1_Id, Iface_2_Id, Iface_4_Id, Tag_20_Id,
-- Tag_20_FV_Id
end record;
-- calls: Iface_1_Id, Iface_2_Id, Iface_4_Id, Par_4_Id, Tag_20_Id,
-- Tag_20_FV_Id
-- own: Ext_8_Id
protected type Prot_1
with Type_Invariant => Mark (Prot_1_FV_Id)
is
entry E;
private
Comp_1 : Tag_18; -- Iface_1_Id, Iface_2_Id, Iface_4_Id, Tag_18_Id
end Prot_1;
-- calls: Iface_1_Id, Iface_2_Id, Iface_4_Id, Tag_18_Id
-- own: Prot_1_FV_Id
protected type Prot_2 is
entry E;
private
Comp_1 : Tag_5; -- none
Comp_2 : Tag_21; -- Tag_15_Id
end Prot_2;
-- calls: Tag_15_Id
-- own: Prot_2_Id
protected type Prot_3
with Type_Invariant => Mark (Prot_3_FV_Id) is new Synch_2
with
entry E;
private
Comp_1 : Tag_24; -- Tag_15_Id, Tag_24_Id, Tag_24_FV_Id
end Prot_3;
-- calls: Tag_15_Id, Tag_24_Id, Tag_24_FV_Id
-- own: Prot_3_Id, Prot_3_FV_Id
-- inheritable: Prot_3_Id
-- inherited: Synch_1_Id, Synch_2_Id
task type Task_1 is
entry E;
end Task_1;
-- own: Task_1_Id
task type Task_2
with Type_Invariant => Mark (Task_2_FV_Id) is new Synch_1
with
entry E;
end Task_2;
-- own: Task_2_Id, Task_2_FV_Id
-- inherited: Synch_1_Id
type Untag_1 is new Integer;
-- none
type Untag_2 is record
Comp : Integer;
end record
with Type_Invariant => Mark (Untag_2_Id);
-- own: Untag_2_Id
type Untag_3 is array (1 .. 5) of Boolean;
-- own: Untag_3_Id
type Untag_4 is record
Comp_1 : Tag_16; -- Tag_4_Id, Tag_16_Id
Comp_2 : Tag_18; -- Iface_1_Id, Iface_2_Id, Iface_4_Id, Tag_18_Id
Comp_3 : Tag_26; -- Tag_15_Id, Tag_26_Id
end record;
-- calls: Iface_1_Id, Iface_2_Id, Iface_4_Id, Tag_4_Id, Tag_15_Id,
-- Tag_16_Id, Tag_18_Id, Tag_26_Id
type Untag_5 is record
Comp_1 : Tag_17; -- Iface_1_Id, Iface_2_Id, Iface_4_Id
Comp_2 : Tag_19; -- Iface_1_Id, Iface_2_Id, Tag_4_Id, Tag_19_Id
Comp_3 : Tag_27; -- Tag_14_Id, Tag_27_Id
end record
with Type_Invariant => Mark (Untag_5_Id);
-- own: Untag_5_Id
-- calls: Iface_1_Id, Iface_2_Id, Iface_4_Id, Tag_4_Id, Tag_14_Id,
-- Tag_19_Id, Tag_27_Id
type Untag_6 is array (1 .. 3, 5 .. 9) of Tag_10;
-- calls: Tag_4_Id, Tag_10_Id
type Untag_7 is array (1 .. 3) of Tag_13
with Type_Invariant => Mark (Untag_7_Id);
-- own: Untag_7_Id
-- calls: Tag_4_Id, Tag_13_Id
type Untag_8 (Discr : Boolean) is record
Comp_1 : Tag_18; -- Iface_1_Id, Iface_2_Id, Iface_4_Id, Tag_18_Id
case Discr is
when True =>
Comp_2 : Tag_1; -- none
when others =>
Comp_3 : Untag_5; -- Iface_1_Id, Iface_2_Id, Iface_4_Id,
-- Tag_4_Id, Tag_14_Id, Tag_19_Id, Tag_27_Id,
-- Untag_5_Id
end case;
end record;
type Untag_9 (Discr_1 : Boolean; Discr_2 : Boolean) is record
Comp_1 : Tag_22; -- Tag_4_Id, Tag_22_Id
case Discr_1 is
when True =>
Comp_2 : Tag_28; -- Tag_4_Id, Tag_28_Id
case Discr_2 is
when True =>
Comp_3 : Untag_1; -- none
when others =>
Comp_4 : Tag_1; -- none
end case;
when others =>
Comp_5 : Tag_4; -- Tag_4_Id, Tag_4_FV_Id
Comp_6 : Tag_24; -- Tag_15_Id, Tag_24_Id, Tag_24_FV_Id
case Discr_2 is
when True =>
Comp_7 : Tag_27; -- Tag_14_Id, Tag_27_Id
when others =>
Comp_8 : Untag_4; -- Iface_1_Id, Iface_2_Id, Iface_4_Id,
-- Tag_4_Id, Tag_15_Id, Tag_16_Id,
-- Tag_18_Id, Tag_26_Id
end case;
end case;
end record
with Type_Invariant => Mark (Untag_9_Id);
-- own: Untag_9_Id
-------------------
-- Derived types --
-------------------
type Deriv_1 is new Tag_4 with null record;
-- inherited: Tag_4_Id
type Deriv_2 is new Tag_16 with null record;
-- inherited: Tag_4_Id, Tag_16_Id
type Deriv_3 is new Tag_18 with null record;
-- inherited: Iface_1_Id, Iface_2_Id, Iface_4_Id
type Deriv_4 is new Untag_4;
-- inherited: Iface_1_Id, Iface_2_Id, Iface_4_Id, Tag_4_Id, Tag_15_Id,
-- Tag_16_Id, Tag_18_Id, Tag_26_Id
type Deriv_5 is new Untag_7;
-- inherited: Tag_4_Id, Tag_13_Id, Untag_7_Id
--------------
-- Subtypes --
--------------
subtype Sub_1 is Tag_9;
-- inherited: Tag_9_Id
subtype Sub_2 is Tag_17;
-- inherited: Iface_1_Id, Iface_2_Id, Iface_4_Id
subtype Sub_3 is Untag_2;
-- inherited: Untag_2_Id
subtype Sub_4 is Untag_5;
-- inherited: Iface_1_Id, Iface_2_Id, Iface_4_Id, Tag_4_Id, Tag_14_Id,
-- Tag_19_Id, Tag_27_Id, Untag_5_Id
subtype Sub_5 is Untag_6;
-- inherited: Tag_4_Id, Tag_10_Id
end Invariants_Aspects;
-- invariants_aspects.adb
package body Invariants_Aspects is
protected body Prot_1 is
entry E when True is begin null; end E;
end Prot_1;
protected body Prot_2 is
entry E when True is begin null; end E;
end Prot_2;
protected body Prot_3 is
entry E when True is begin null; end E;
end Prot_3;
task body Task_1 is
begin
select
accept E do null; end E;
or
terminate;
end select;
end Task_1;
task body Task_2 is
begin
select
accept E do null; end E;
or
terminate;
end select;
end Task_2;
procedure Test_Deriv_1 is
begin
Reset_Results;
declare
Obj : Deriv_1;
begin
Test_Results ("Deriv_1", (Tag_4_Id => True,
others => False));
end;
end Test_Deriv_1;
procedure Test_Deriv_2 is
begin
Reset_Results;
declare
Obj : Deriv_2;
begin
Test_Results ("Deriv_2", (Tag_4_Id => True,
Tag_16_Id => True,
others => False));
end;
end Test_Deriv_2;
procedure Test_Deriv_3 is
begin
Reset_Results;
declare
Obj : Deriv_3;
begin
Test_Results ("Deriv_3", (Iface_1_Id => True,
Iface_2_Id => True,
Iface_4_Id => True,
others => False));
end;
end Test_Deriv_3;
procedure Test_Deriv_4 is
begin
Reset_Results;
declare
Obj : Deriv_4;
begin
Test_Results ("Deriv_4", (Iface_1_Id => True,
Iface_2_Id => True,
Iface_4_Id => True,
Tag_4_Id => True,
Tag_15_Id => True,
Tag_16_Id => True,
Tag_18_Id => True,
Tag_26_Id => True,
others => False));
end;
end Test_Deriv_4;
procedure Test_Deriv_5 is
begin
Reset_Results;
declare
Obj : Deriv_5;
begin
Test_Results ("Deriv_5", (Tag_4_Id => True,
Tag_13_Id => True,
others => False));
end;
end Test_Deriv_5;
procedure Test_Sub_1 is
begin
Reset_Results;
declare
Obj : Sub_1;
begin
Test_Results ("Sub_1", (Tag_9_Id => True,
others => False));
end;
end Test_Sub_1;
procedure Test_Sub_2 is
begin
Reset_Results;
declare
Obj : Sub_2;
begin
Test_Results ("Sub_2", (Iface_1_Id => True,
Iface_2_Id => True,
Iface_4_Id => True,
others => False));
end;
end Test_Sub_2;
procedure Test_Sub_3 is
begin
Reset_Results;
declare
Obj : Sub_3;
begin
Test_Results ("Sub_3", (Untag_2_Id => True,
others => False));
end;
end Test_Sub_3;
procedure Test_Sub_4 is
begin
Reset_Results;
declare
Obj : Sub_4;
begin
Test_Results ("Sub_4", (Iface_1_Id => True,
Iface_2_Id => True,
Iface_4_Id => True,
Tag_4_Id => True,
Tag_14_Id => True,
Tag_19_Id => True,
Tag_27_Id => True,
Untag_5_Id => True,
others => False));
end;
end Test_Sub_4;
procedure Test_Sub_5 is
begin
Reset_Results;
declare
Obj : Sub_5;
begin
Test_Results ("Sub_5", (Tag_4_Id => True,
Tag_10_Id => True,
others => False));
end;
end Test_Sub_5;
procedure Test_Untag_9_TT is
begin
Reset_Results;
declare
Obj : Untag_9 (True, True);
begin
Test_Results ("Untag_9_TT", (Tag_4_Id => True,
Tag_22_Id => True,
Tag_28_Id => True,
Untag_9_Id => True,
others => False));
end;
end Test_Untag_9_TT;
procedure Test_Untag_9_TF is
begin
Reset_Results;
declare
Obj : Untag_9 (True, False);
begin
Test_Results ("Untag_9_TF", (Tag_4_Id => True,
Tag_22_Id => True,
Tag_28_Id => True,
Untag_9_Id => True,
others => False));
end;
end Test_Untag_9_TF;
procedure Test_Untag_9_FT is
begin
Reset_Results;
declare
Obj : Untag_9 (False, True);
begin
Test_Results ("Untag_9_FT", (Tag_4_Id => True,
Tag_4_FV_Id => True,
Tag_14_Id => True,
Tag_15_Id => True,
Tag_22_Id => True,
Tag_24_Id => True,
Tag_24_FV_Id => True,
Tag_27_Id => True,
Untag_9_Id => True,
others => False));
end;
end Test_Untag_9_FT;
procedure Test_Untag_9_FF is
begin
Reset_Results;
declare
Obj : Untag_9 (False, False);
begin
Test_Results ("Untag_9_FF", (Iface_1_Id => True,
Iface_2_Id => True,
Iface_4_Id => True,
Tag_4_Id => True,
Tag_4_FV_Id => True,
Tag_15_Id => True,
Tag_16_Id => True,
Tag_18_Id => True,
Tag_22_Id => True,
Tag_24_Id => True,
Tag_24_FV_Id => True,
Tag_26_Id => True,
Untag_9_Id => True,
others => False));
end;
end Test_Untag_9_FF;
end Invariants_Aspects;
-- invariants_main.adb
with Invariants_Aspects; use Invariants_Aspects;
with Tester; use Tester;
procedure Invariants_Main is
begin
Reset_Results;
declare
Obj : Tag_1;
begin
Test_Results ("Tag_1", (others => False));
end;
Reset_Results;
declare
Obj : Tag_2;
begin
Test_Results ("Tag_2", (Tag_2_Id => True,
others => False));
end;
Reset_Results;
declare
Obj : Tag_3;
begin
Test_Results ("Tag_3", (Tag_3_Id => True,
others => False));
end;
Reset_Results;
declare
Obj : Tag_4;
begin
Test_Results ("Tag_4", (Tag_4_Id => True,
Tag_4_FV_Id => True,
others => False));
end;
Reset_Results;
declare
Obj : Tag_5;
begin
Test_Results ("Tag_5", (others => False));
end;
Reset_Results;
declare
Obj : Tag_6;
begin
Test_Results ("Tag_6", (others => False));
end;
Reset_Results;
declare
Obj : Tag_7;
begin
Test_Results ("Tag_7", (Tag_4_Id => True,
others => False));
end;
Reset_Results;
declare
Obj : Tag_8;
begin
Test_Results ("Tag_8", (Tag_8_Id => True,
others => False));
end;
Reset_Results;
declare
Obj : Tag_9;
begin
Test_Results ("Tag_9", (Tag_9_Id => True,
others => False));
end;
Reset_Results;
declare
Obj : Tag_10;
begin
Test_Results ("Tag_10", (Tag_4_Id => True,
Tag_10_Id => True,
others => False));
end;
Reset_Results;
declare
Obj : Tag_11;
begin
Test_Results ("Tag_11", (Tag_11_Id => True,
others => False));
end;
Reset_Results;
declare
Obj : Tag_12;
begin
Test_Results ("Tag_12", (Tag_12_Id => True,
others => False));
end;
Reset_Results;
declare
Obj : Tag_13;
begin
Test_Results ("Tag_13", (Tag_4_Id => True,
Tag_13_Id => True,
others => False));
end;
Reset_Results;
declare
Obj : Tag_14;
begin
Test_Results ("Tag_14", (Tag_14_Id => True,
others => False));
end;
Reset_Results;
declare
Obj : Tag_15;
begin
Test_Results ("Tag_15", (Tag_15_Id => True,
Tag_15_FV_Id => True,
others => False));
end;
Reset_Results;
declare
Obj : Tag_16;
begin
Test_Results ("Tag_16", (Tag_4_Id => True,
Tag_16_Id => True,
others => False));
end;
Reset_Results;
declare
Obj : Tag_17;
begin
Test_Results ("Tag_17", (Iface_1_Id => True,
Iface_2_Id => True,
Iface_4_Id => True,
others => False));
end;
Reset_Results;
declare
Obj : Tag_18;
begin
Test_Results ("Tag_18", (Iface_1_Id => True,
Iface_2_Id => True,
Iface_4_Id => True,
Tag_18_Id => True,
others => False));
end;
Reset_Results;
declare
Obj : Tag_19;
begin
Test_Results ("Tag_19", (Iface_1_Id => True,
Iface_2_Id => True,
Tag_4_Id => True,
Tag_19_Id => True,
others => False));
end;
Reset_Results;
declare
Obj : Tag_20;
begin
Test_Results ("Tag_20", (Iface_1_Id => True,
Iface_2_Id => True,
Iface_4_Id => True,
Tag_20_Id => True,
Tag_20_FV_Id => True,
others => False));
end;
Reset_Results;
declare
Obj : Tag_21;
begin
Test_Results ("Tag_21", (Tag_15_Id => True,
others => False));
end;
Reset_Results;
declare
Obj : Tag_22;
begin
Test_Results ("Tag_22", (Tag_4_Id => True,
Tag_22_Id => True,
others => False));
end;
Reset_Results;
declare
Obj : Tag_23;
begin
Test_Results ("Tag_23", (Tag_23_Id => True,
others => False));
end;
Reset_Results;
declare
Obj : Tag_24;
begin
Test_Results ("Tag_24", (Tag_15_Id => True,
Tag_24_Id => True,
Tag_24_FV_Id => True,
others => False));
end;
Reset_Results;
declare
Obj : Tag_25;
begin
Test_Results ("Tag_25", (Tag_4_Id => True,
others => False));
end;
Reset_Results;
declare
Obj : Tag_26;
begin
Test_Results ("Tag_26", (Tag_15_Id => True,
Tag_26_Id => True,
others => False));
end;
Reset_Results;
declare
Obj : Tag_27;
begin
Test_Results ("Tag_27", (Tag_14_Id => True,
Tag_27_Id => True,
others => False));
end;
Reset_Results;
declare
Obj : Tag_28;
begin
Test_Results ("Tag_28", (Tag_4_Id => True,
Tag_28_Id => True,
others => False));
end;
Reset_Results;
declare
Obj : Ext_1 (True);
begin
Test_Results ("Ext_1_T", (Ext_1_FV_Id => True,
Iface_1_Id => True,
Iface_2_Id => True,
Iface_4_Id => True,
Tag_4_Id => True,
Tag_8_Id => True,
Tag_10_Id => True,
Tag_15_Id => True,
Tag_20_Id => True,
Tag_20_FV_Id => True,
Tag_26_Id => True,
others => False));
end;
Reset_Results;
declare
Obj : Ext_1 (False);
begin
Test_Results ("Ext_1_F", (Ext_1_FV_Id => True,
Iface_1_Id => True,
Iface_2_Id => True,
Iface_4_Id => True,
Tag_4_Id => True,
Tag_8_Id => True,
Tag_15_Id => True,
Tag_19_Id => True,
Tag_20_Id => True,
Tag_20_FV_Id => True,
Tag_26_Id => True,
others => False));
end;
Reset_Results;
declare
Obj : Ext_2 (True);
begin
Test_Results ("Ext_2_T", (Ext_2_Id => True,
Tag_4_Id => True,
Tag_8_Id => True,
Tag_10_Id => True,
others => False));
end;
Reset_Results;
declare
Obj : Ext_2 (False);
begin
Test_Results ("Ext_2_F", (Ext_2_Id => True,
Iface_1_Id => True,
Iface_2_Id => True,
Tag_4_Id => True,
Tag_8_Id => True,
Tag_19_Id => True,
others => False));
end;
Reset_Results;
declare
Obj : Ext_3;
begin
Test_Results ("Ext_3", (Iface_1_Id => True,
Iface_2_Id => True,
Tag_4_Id => True,
Tag_15_Id => True,
Tag_19_Id => True,
Tag_22_Id => True,
Tag_24_Id => True,
Tag_24_FV_Id => True,
others => False));
end;
Reset_Results;
declare
Obj : Ext_4;
begin
Test_Results ("Ext_4", (Ext_4_Id => True,
Ext_4_FV_Id => True,
Tag_4_Id => True,
Tag_14_Id => True,
Tag_15_Id => True,
Tag_22_Id => True,
Tag_24_Id => True,
Tag_24_FV_Id => True,
others => False));
end;
Reset_Results;
declare
Obj : Ext_5;
begin
Test_Results ("Ext_5", (Ext_5_Id => True,
Iface_1_Id => True,
Iface_2_Id => True,
Iface_4_Id => True,
Tag_18_Id => True,
others => False));
end;
Reset_Results;
declare
Obj : Ext_6;
begin
Test_Results ("Ext_6", (Ext_6_FV_Id => True,
Tag_4_Id => True,
Tag_4_FV_Id => True,
others => False));
end;
Reset_Results;
declare
Obj : Ext_7 (True);
begin
Test_Results ("Ext_7_T", (Par_4_Id => True,
Tag_4_Id => True,
Tag_28_Id => True,
others => False));
end;
Reset_Results;
declare
Obj : Ext_7 (False);
begin
Test_Results ("Ext_7_F", (Par_4_Id => True,
Tag_4_Id => True,
Tag_28_Id => True,
others => False));
end;
Reset_Results;
declare
Obj : Ext_8 (True);
begin
Test_Results ("Ext_8_T", (Ext_8_Id => True,
Iface_1_Id => True,
Iface_2_Id => True,
Iface_4_Id => True,
Par_4_Id => True,
Tag_20_Id => True,
Tag_20_FV_Id => True,
others => False));
end;
Reset_Results;
declare
Obj : Ext_8 (False);
begin
Test_Results ("Ext_8_F", (Ext_8_Id => True,
Iface_1_Id => True,
Iface_2_Id => True,
Iface_4_Id => True,
Par_4_Id => True,
Tag_20_Id => True,
Tag_20_FV_Id => True,
others => False));
end;
Reset_Results;
declare
Obj : Prot_1;
begin
Test_Results ("Prot_1", (Iface_1_Id => True,
Iface_2_Id => True,
Iface_4_Id => True,
Prot_1_FV_Id => True,
Tag_18_Id => True,
others => False));
end;
Reset_Results;
declare
Obj : Prot_2;
begin
Test_Results ("Prot_2", (Prot_2_Id => True,
Tag_15_Id => True,
others => False));
end;
Reset_Results;
declare
Obj : Prot_3;
begin
Test_Results ("Prot_3", (Prot_3_Id => True,
Prot_3_FV_Id => True,
Synch_1_Id => True,
Synch_2_Id => True,
Tag_15_Id => True,
Tag_24_Id => True,
Tag_24_FV_Id => True,
others => False));
end;
Reset_Results;
declare
Obj : Task_1;
begin
Test_Results ("Task_1", (Task_1_Id => True,
others => False));
end;
Reset_Results;
declare
Obj : Task_2;
begin
Test_Results ("Task_2", (Synch_1_Id => True,
Task_2_Id => True,
Task_2_FV_Id => True,
others => False));
end;
Reset_Results;
declare
Obj : Untag_1;
begin
Test_Results ("Untag_1", (others => False));
end;
Reset_Results;
declare
Obj : Untag_2;
begin
Test_Results ("Untag_2", (Untag_2_Id => True,
others => False));
end;
Reset_Results;
declare
Obj : Untag_3;
begin
Test_Results ("Untag_3", (Untag_3_Id => True,
others => False));
end;
Reset_Results;
declare
Obj : Untag_4;
begin
Test_Results ("Untag_4", (Iface_1_Id => True,
Iface_2_Id => True,
Iface_4_Id => True,
Tag_4_Id => True,
Tag_15_Id => True,
Tag_16_Id => True,
Tag_18_Id => True,
Tag_26_Id => True,
others => False));
end;
Reset_Results;
declare
Obj : Untag_5;
begin
Test_Results ("Untag_5", (Iface_1_Id => True,
Iface_2_Id => True,
Iface_4_Id => True,
Tag_4_Id => True,
Tag_14_Id => True,
Tag_19_Id => True,
Tag_27_Id => True,
Untag_5_Id => True,
others => False));
end;
Reset_Results;
declare
Obj : Untag_6;
begin
Test_Results ("Untag_6", (Tag_4_Id => True,
Tag_10_Id => True,
others => False));
end;
Reset_Results;
declare
Obj : Untag_7;
begin
Test_Results ("Untag_7", (Tag_4_Id => True,
Tag_13_Id => True,
Untag_7_Id => True,
others => False));
end;
Reset_Results;
declare
Obj : Untag_8 (True);
begin
Test_Results ("Untag_8_T", (Iface_1_Id => True,
Iface_2_Id => True,
Iface_4_Id => True,
Tag_18_Id => True,
others => False));
end;
Reset_Results;
declare
Obj : Untag_8 (False);
begin
Test_Results ("Untag_8_F", (Iface_1_Id => True,
Iface_2_Id => True,
Iface_4_Id => True,
Tag_4_Id => True,
Tag_14_Id => True,
Tag_18_Id => True,
Tag_19_Id => True,
Tag_27_Id => True,
Untag_5_Id => True,
others => False));
end;
Test_Untag_9_TT;
Test_Untag_9_TF;
Test_Untag_9_FT;
Test_Untag_9_FF;
Test_Deriv_1;
Test_Deriv_2;
Test_Deriv_3;
Test_Deriv_4;
Test_Deriv_5;
Test_Sub_1;
Test_Sub_2;
Test_Sub_3;
Test_Sub_4;
Test_Sub_5;
end Invariants_Main;
----------------------------
-- Compilation and output --
----------------------------
$ gnatmake -q -gnata -gnatws invariants_main.adb
$ ./invariants_main
Tag_1: OK
Tag_2: OK
Tag_3: OK
Tag_4: OK
Tag_5: OK
Tag_6: OK
Tag_7: OK
Tag_8: OK
Tag_9: OK
Tag_10: OK
Tag_11: OK
Tag_12: OK
Tag_13: OK
Tag_14: OK
Tag_15: OK
Tag_16: OK
Tag_17: OK
Tag_18: OK
Tag_19: OK
Tag_20: OK
Tag_21: OK
Tag_22: OK
Tag_23: OK
Tag_24: OK
Tag_25: OK
Tag_26: OK
Tag_27: OK
Tag_28: OK
Ext_1_T: OK
Ext_1_F: OK
Ext_2_T: OK
Ext_2_F: OK
Ext_3: OK
Ext_4: OK
Ext_5: OK
Ext_6: OK
Ext_7_T: OK
Ext_7_F: OK
Ext_8_T: OK
Ext_8_F: OK
Prot_1: OK
Prot_2: OK
Prot_3: OK
Task_1: OK
Task_2: OK
Untag_1: OK
Untag_2: OK
Untag_3: OK
Untag_4: OK
Untag_5: OK
Untag_6: OK
Untag_7: OK
Untag_8_T: OK
Untag_8_F: OK
Untag_9_TT: OK
Untag_9_TF: OK
Untag_9_FT: OK
Untag_9_FF: OK
Deriv_1: OK
Deriv_2: OK
Deriv_3: OK
Deriv_4: OK
Deriv_5: OK
Sub_1: OK
Sub_2: OK
Sub_3: OK
Sub_4: OK
Sub_5: OK
Tested on x86_64-pc-linux-gnu, committed on trunk
2016-06-16 Hristian Kirtchev <kirtchev@adacore.com>
* atree.ads, atree.adb (Elist29): New routine.
(Set_Elist29): New routine.
* atree.h New definition for Elist29.
* einfo.adb Subprograms_For_Type is now an Elist rather than
a node. Has_Invariants is now a synthesized attribute
and does not require a flag. Has_Own_Invariants
is now Flag232. Has_Inherited_Invariants is
Flag291. Is_Partial_Invariant_Procedure is Flag292.
(Default_Init_Cond_Procedure): Reimplemented.
(Has_Inherited_Invariants): New routine.
(Has_Invariants): Reimplemented.
(Has_Own_Invariants): New routine.
(Invariant_Procedure): Reimplemented.
(Is_Partial_Invariant_Procedure): New routine.
(Partial_Invariant_Procedure): Reimplemented.
(Predicate_Function): Reimplemented.
(Predicate_Function_M): Reimplemented.
(Set_Default_Init_Cond_Procedure): Reimplemented.
(Set_Has_Inherited_Invariants): New routine.
(Set_Has_Invariants): Removed.
(Set_Has_Own_Invariants): New routine.
(Set_Invariant_Procedure): Reimplemented.
(Set_Is_Partial_Invariant_Procedure): New routine.
(Set_Partial_Invariant_Procedure): Reimplemented.
(Set_Predicate_Function): Reimplemented.
(Set_Predicate_Function_M): Reimplemented.
(Set_Subprograms_For_Type): Reimplemented.
(Subprograms_For_Type): Reimplemented.
(Write_Entity_Flags): Output Flag232 and Flag291.
* einfo.ads Add new attributes Has_Inherited_Invariants
Has_Own_Invariants Is_Partial_Invariant_Procedure
Partial_Invariant_Procedure Change the documentation
of attributes Has_Inheritable_Invariants Has_Invariants
Invariant_Procedure Is_Invariant_Procedure Subprograms_For_Type
(Has_Inherited_Invariants): New routine along with pragma Inline.
(Has_Own_Invariants): New routine along with pragma Inline.
(Is_Partial_Invariant_Procedure): New routine along with pragma Inline.
(Partial_Invariant_Procedure): New routine.
(Set_Has_Inherited_Invariants): New routine along with pragma Inline.
(Set_Has_Invariants): Removed along with pragma Inline.
(Set_Has_Own_Invariants): New routine along with pragma Inline.
(Set_Is_Partial_Invariant_Procedure): New routine
along with pragma Inline.
(Set_Partial_Invariant_Procedure): New routine.
(Set_Subprograms_For_Type): Update the signature.
(Subprograms_For_Type): Update the signature.
* exp_ch3.adb Remove with and use clauses for Sem_Ch13.
(Build_Array_Invariant_Proc): Removed.
(Build_Record_Invariant_Proc): Removed.
(Freeze_Type): Build the body of the invariant procedure.
(Insert_Component_Invariant_Checks): Removed.
* exp_ch7.adb Add with and use clauses for Sem_Ch6, Sem_Ch13,
and Stringt.
(Build_Invariant_Procedure_Body): New routine.
(Build_Invariant_Procedure_Declaration): New routine.
* exp_ch7.ads (Build_Invariant_Procedure_Body): New routine.
(Build_Invariant_Procedure_Declaration): New routine.
* exp_ch9.adb (Build_Corresponding_Record): Do not propagate
attributes related to invariants to the corresponding record
when building the corresponding record. This is done by
Build_Invariant_Procedure_Declaration.
* exp_util.adb (Make_Invariant_Call): Reimplemented.
* freeze.adb (Freeze_Array_Type): An array type requires an
invariant procedure when its component type has invariants.
(Freeze_Record_Type): A record type requires an invariant
procedure when at least one of its components has an invariant.
* sem_ch3.adb (Analyze_Private_Extension_Declaration): Inherit
invariant-related attributes.
(Analyze_Subtype_Declaration):
Inherit invariant-related attributes.
(Build_Derived_Record_Type): Inherit invariant-related attributes.
(Check_Duplicate_Aspects): Reimplemented.
(Get_Partial_View_Aspect): New routine.
(Process_Full_View): Inherit invariant-related attributes. Reimplement
the check on hidden inheritance of class-wide invariants.
(Remove_Default_Init_Cond_Procedure): Reimplemented.
* sem_ch6.adb (Analyze_Subprogram_Specification): Do not modify
the controlling type for an invariant procedure declaration
or body.
(Is_Invariant_Procedure_Or_Body): New routine.
* sem_ch7.adb (Analyze_Package_Specification): Build the partial
invariant body in order to preanalyze and resolve all invariants
of a private type at the end of the visible declarations. Build
the full invariant body in order to preanalyze and resolve
all invariants of a private type's full view at the end of
the private declarations.
(Preserve_Full_Attributes): Inherit invariant-related attributes.
* sem_ch9.adb (Analyze_Protected_Type_Declaration): Ensure that
aspects are analyzed with the proper view when the protected type
is a completion of a private type. Inherit invariant-related attributes.
(Analyze_Task_Type_Declaration): Ensure that
aspects are analyzed with the proper view when the task type
is a completion of a private type. Inherit invariant-related
attributes.
* sem_ch13.adb Remove with and use clauses for Stringt.
(Build_Invariant_Procedure_Declaration): Removed.
(Build_Invariant_Procedure): Removed.
(Freeze_Entity_Checks): Do not build the body of the invariant
procedure here.
The body is built when the type is frozen in Freeze_Type.
(Inherit_Aspects_At_Freeze_Point): Do not inherit any attributes
related to invariants here because this leads to erroneous
inheritance.
(Replace_Node): Rename to Replace_Type_Ref.
* sem_ch13.ads (Build_Invariant_Procedure_Declaration): Removed.
(Build_Invariant_Procedure): Removed.
* sem_prag.adb Add with and use clauses for Exp_Ch7.
(Analyze_Pragma): Reimplement the analysis of pragma Invariant.
* sem_res.adb (Resolve_Actuals): Emit a specialized error when
the context is an invariant.
* sem_util.adb (Get_Views): New routine.
(Incomplete_Or_Partial_View): Consider generic packages when
examining declarations.
(Inspect_Decls): Consider full type
declarations because they may denote a derivation from a
private type.
(Propagate_Invariant_Attributes): New routine.
* sem_util.ads (Get_Views): New routine.
(Propagate_Invariant_Attributes): New routine.
Attachment:
difs
Description: Text document
| Index Nav: | [Date Index] [Subject Index] [Author Index] [Thread Index] | |
|---|---|---|
| Message Nav: | [Date Prev] [Date Next] | [Thread Prev] [Thread Next] |