Commit 59e6b23c by Arnaud Charlet

[multiple changes]

2011-08-29  Yannick Moy  <moy@adacore.com>

	* exp_ch13.adb (Expand_N_Freeze_Entity): Do nothing in Alfa mode.
	* exp_ch9.adb: Do not expand tasking constructs in Alfa mode.
	* gnat1drv.adb (Adjust_Global_Switches): Suppress the expansion of
	tagged types and dispatching calls in Alfa mode.

2011-08-29  Javier Miranda  <miranda@adacore.com>

	* sem_ch3.adb (Process_Discriminants): Add missing check to ensure that
	we do not report an error on an Empty node.

2011-08-29  Geert Bosch  <bosch@adacore.com>

	* Makefile.rtl (GNATRTL_NONTASKING_OBJECTS): Add a-nllrar.o,
	a-nlrear.o and a-nurear.o.

2011-08-29  Robert Dewar  <dewar@adacore.com>

	* freeze.adb: Minor code reorganization.
	Minor reformatting.
	* sem_util.adb, errout.adb, exp_ch11.adb, a-ngrear.adb, s-gearop.adb,
	sem_ch6.adb: Minor reformatting

2011-08-29  Tristan Gingold  <gingold@adacore.com>

	* s-except.ads, s-except.adb: Provide dummy body.

2011-08-29  Yannick Moy  <moy@adacore.com>

	* sem_warn.adb (Within_Postcondition): Take into account the case of
	an Ensures component in a Test_Case.

From-SVN: r178222
parent 4d792549
2011-08-29 Yannick Moy <moy@adacore.com>
* exp_ch13.adb (Expand_N_Freeze_Entity): Do nothing in Alfa mode.
* exp_ch9.adb: Do not expand tasking constructs in Alfa mode.
* gnat1drv.adb (Adjust_Global_Switches): Suppress the expansion of
tagged types and dispatching calls in Alfa mode.
2011-08-29 Javier Miranda <miranda@adacore.com>
* sem_ch3.adb (Process_Discriminants): Add missing check to ensure that
we do not report an error on an Empty node.
2011-08-29 Geert Bosch <bosch@adacore.com>
* Makefile.rtl (GNATRTL_NONTASKING_OBJECTS): Add a-nllrar.o,
a-nlrear.o and a-nurear.o.
2011-08-29 Robert Dewar <dewar@adacore.com>
* freeze.adb: Minor code reorganization.
Minor reformatting.
* sem_util.adb, errout.adb, exp_ch11.adb, a-ngrear.adb, s-gearop.adb,
sem_ch6.adb: Minor reformatting
2011-08-29 Tristan Gingold <gingold@adacore.com>
* s-except.ads, s-except.adb: Provide dummy body.
2011-08-29 Yannick Moy <moy@adacore.com>
* sem_warn.adb (Within_Postcondition): Take into account the case of
an Ensures component in a Test_Case.
2011-08-29 Tristan Gingold <gingold@adacore.com> 2011-08-29 Tristan Gingold <gingold@adacore.com>
* s-excdeb.ads, s-excdeb.adb: New files, created from s-except. * s-excdeb.ads, s-excdeb.adb: New files, created from s-except.
......
...@@ -184,6 +184,9 @@ GNATRTL_NONTASKING_OBJS= \ ...@@ -184,6 +184,9 @@ GNATRTL_NONTASKING_OBJS= \
a-ngcoty$(objext) \ a-ngcoty$(objext) \
a-ngelfu$(objext) \ a-ngelfu$(objext) \
a-ngrear$(objext) \ a-ngrear$(objext) \
a-nllrar$(objext) \
a-nlrear$(objext) \
a-nurear$(objext) \
a-nlcefu$(objext) \ a-nlcefu$(objext) \
a-nlcoty$(objext) \ a-nlcoty$(objext) \
a-nlelfu$(objext) \ a-nlelfu$(objext) \
......
...@@ -48,24 +48,24 @@ package body Ada.Numerics.Generic_Real_Arrays is ...@@ -48,24 +48,24 @@ package body Ada.Numerics.Generic_Real_Arrays is
function Is_Non_Zero (X : Real'Base) return Boolean is (X /= 0.0); function Is_Non_Zero (X : Real'Base) return Boolean is (X /= 0.0);
procedure Back_Substitute is new Ops.Back_Substitute procedure Back_Substitute is new Ops.Back_Substitute
(Scalar => Real'Base, (Scalar => Real'Base,
Matrix => Real_Matrix, Matrix => Real_Matrix,
Is_Non_Zero => Is_Non_Zero); Is_Non_Zero => Is_Non_Zero);
function Diagonal is new Ops.Diagonal function Diagonal is new Ops.Diagonal
(Scalar => Real'Base, (Scalar => Real'Base,
Vector => Real_Vector, Vector => Real_Vector,
Matrix => Real_Matrix); Matrix => Real_Matrix);
procedure Forward_Eliminate is new Ops.Forward_Eliminate procedure Forward_Eliminate is new Ops.Forward_Eliminate
(Scalar => Real'Base, (Scalar => Real'Base,
Matrix => Real_Matrix, Matrix => Real_Matrix,
Zero => 0.0, Zero => 0.0,
One => 1.0); One => 1.0);
procedure Swap_Column is new Ops.Swap_Column procedure Swap_Column is new Ops.Swap_Column
(Scalar => Real'Base, (Scalar => Real'Base,
Matrix => Real_Matrix); Matrix => Real_Matrix);
procedure Transpose is new Ops.Transpose procedure Transpose is new Ops.Transpose
(Scalar => Real'Base, (Scalar => Real'Base,
...@@ -100,7 +100,7 @@ package body Ada.Numerics.Generic_Real_Arrays is ...@@ -100,7 +100,7 @@ package body Ada.Numerics.Generic_Real_Arrays is
-- Sort Values and associated Vectors by decreasing absolute value -- Sort Values and associated Vectors by decreasing absolute value
procedure Swap (Left, Right : in out Real); procedure Swap (Left, Right : in out Real);
-- Exchange Left and Right. -- Exchange Left and Right
function Sqrt (X : Real) return Real; function Sqrt (X : Real) return Real;
-- Sqrt is implemented locally here, in order to avoid dragging in all of -- Sqrt is implemented locally here, in order to avoid dragging in all of
...@@ -132,7 +132,6 @@ package body Ada.Numerics.Generic_Real_Arrays is ...@@ -132,7 +132,6 @@ package body Ada.Numerics.Generic_Real_Arrays is
if not (X > 0.0) then if not (X > 0.0) then
if X = 0.0 then if X = 0.0 then
return X; return X;
else else
raise Argument_Error; raise Argument_Error;
end if; end if;
...@@ -158,9 +157,7 @@ package body Ada.Numerics.Generic_Real_Arrays is ...@@ -158,9 +157,7 @@ package body Ada.Numerics.Generic_Real_Arrays is
for J in 1 .. 8 loop for J in 1 .. 8 loop
Next := (Root + X / Root) / 2.0; Next := (Root + X / Root) / 2.0;
exit when Root = Next; exit when Root = Next;
Root := Next; Root := Next;
end loop; end loop;
...@@ -401,29 +398,29 @@ package body Ada.Numerics.Generic_Real_Arrays is ...@@ -401,29 +398,29 @@ package body Ada.Numerics.Generic_Real_Arrays is
--------- ---------
function "+" (Right : Real_Vector) return Real_Vector function "+" (Right : Real_Vector) return Real_Vector
renames Instantiations."+"; renames Instantiations."+";
function "+" (Right : Real_Matrix) return Real_Matrix function "+" (Right : Real_Matrix) return Real_Matrix
renames Instantiations."+"; renames Instantiations."+";
function "+" (Left, Right : Real_Vector) return Real_Vector function "+" (Left, Right : Real_Vector) return Real_Vector
renames Instantiations."+"; renames Instantiations."+";
function "+" (Left, Right : Real_Matrix) return Real_Matrix function "+" (Left, Right : Real_Matrix) return Real_Matrix
renames Instantiations."+"; renames Instantiations."+";
--------- ---------
-- "-" -- -- "-" --
--------- ---------
function "-" (Right : Real_Vector) return Real_Vector function "-" (Right : Real_Vector) return Real_Vector
renames Instantiations."-"; renames Instantiations."-";
function "-" (Right : Real_Matrix) return Real_Matrix function "-" (Right : Real_Matrix) return Real_Matrix
renames Instantiations."-"; renames Instantiations."-";
function "-" (Left, Right : Real_Vector) return Real_Vector function "-" (Left, Right : Real_Vector) return Real_Vector
renames Instantiations."-"; renames Instantiations."-";
function "-" (Left, Right : Real_Matrix) return Real_Matrix function "-" (Left, Right : Real_Matrix) return Real_Matrix
renames Instantiations."-"; renames Instantiations."-";
...@@ -435,58 +432,58 @@ package body Ada.Numerics.Generic_Real_Arrays is ...@@ -435,58 +432,58 @@ package body Ada.Numerics.Generic_Real_Arrays is
-- Scalar multiplication -- Scalar multiplication
function "*" (Left : Real'Base; Right : Real_Vector) return Real_Vector function "*" (Left : Real'Base; Right : Real_Vector) return Real_Vector
renames Instantiations."*"; renames Instantiations."*";
function "*" (Left : Real_Vector; Right : Real'Base) return Real_Vector function "*" (Left : Real_Vector; Right : Real'Base) return Real_Vector
renames Instantiations."*"; renames Instantiations."*";
function "*" (Left : Real'Base; Right : Real_Matrix) return Real_Matrix function "*" (Left : Real'Base; Right : Real_Matrix) return Real_Matrix
renames Instantiations."*"; renames Instantiations."*";
function "*" (Left : Real_Matrix; Right : Real'Base) return Real_Matrix function "*" (Left : Real_Matrix; Right : Real'Base) return Real_Matrix
renames Instantiations."*"; renames Instantiations."*";
-- Vector multiplication -- Vector multiplication
function "*" (Left, Right : Real_Vector) return Real'Base function "*" (Left, Right : Real_Vector) return Real'Base
renames Instantiations."*"; renames Instantiations."*";
function "*" (Left, Right : Real_Vector) return Real_Matrix function "*" (Left, Right : Real_Vector) return Real_Matrix
renames Instantiations."*"; renames Instantiations."*";
function "*" (Left : Real_Vector; Right : Real_Matrix) return Real_Vector function "*" (Left : Real_Vector; Right : Real_Matrix) return Real_Vector
renames Instantiations."*"; renames Instantiations."*";
function "*" (Left : Real_Matrix; Right : Real_Vector) return Real_Vector function "*" (Left : Real_Matrix; Right : Real_Vector) return Real_Vector
renames Instantiations."*"; renames Instantiations."*";
-- Matrix Multiplication -- Matrix Multiplication
function "*" (Left, Right : Real_Matrix) return Real_Matrix function "*" (Left, Right : Real_Matrix) return Real_Matrix
renames Instantiations."*"; renames Instantiations."*";
--------- ---------
-- "/" -- -- "/" --
--------- ---------
function "/" (Left : Real_Vector; Right : Real'Base) return Real_Vector function "/" (Left : Real_Vector; Right : Real'Base) return Real_Vector
renames Instantiations."/"; renames Instantiations."/";
function "/" (Left : Real_Matrix; Right : Real'Base) return Real_Matrix function "/" (Left : Real_Matrix; Right : Real'Base) return Real_Matrix
renames Instantiations."/"; renames Instantiations."/";
----------- -----------
-- "abs" -- -- "abs" --
----------- -----------
function "abs" (Right : Real_Vector) return Real'Base function "abs" (Right : Real_Vector) return Real'Base
renames Instantiations."abs"; renames Instantiations."abs";
function "abs" (Right : Real_Vector) return Real_Vector function "abs" (Right : Real_Vector) return Real_Vector
renames Instantiations."abs"; renames Instantiations."abs";
function "abs" (Right : Real_Matrix) return Real_Matrix function "abs" (Right : Real_Matrix) return Real_Matrix
renames Instantiations."abs"; renames Instantiations."abs";
----------------- -----------------
-- Determinant -- -- Determinant --
...@@ -496,10 +493,8 @@ package body Ada.Numerics.Generic_Real_Arrays is ...@@ -496,10 +493,8 @@ package body Ada.Numerics.Generic_Real_Arrays is
M : Real_Matrix := A; M : Real_Matrix := A;
B : Real_Matrix (A'Range (1), 1 .. 0); B : Real_Matrix (A'Range (1), 1 .. 0);
R : Real'Base; R : Real'Base;
begin begin
Forward_Eliminate (M, B, R); Forward_Eliminate (M, B, R);
return R; return R;
end Determinant; end Determinant;
...@@ -527,7 +522,6 @@ package body Ada.Numerics.Generic_Real_Arrays is ...@@ -527,7 +522,6 @@ package body Ada.Numerics.Generic_Real_Arrays is
begin begin
Jacobi (A, Values, Vectors, Compute_Vectors => False); Jacobi (A, Values, Vectors, Compute_Vectors => False);
Sort_Eigensystem (Values, Vectors); Sort_Eigensystem (Values, Vectors);
return Values; return Values;
end Eigenvalues; end Eigenvalues;
...@@ -574,7 +568,6 @@ package body Ada.Numerics.Generic_Real_Arrays is ...@@ -574,7 +568,6 @@ package body Ada.Numerics.Generic_Real_Arrays is
-- values of type Real. -- values of type Real.
Max_Iterations : constant := 50; Max_Iterations : constant := 50;
N : constant Natural := Length (A); N : constant Natural := Length (A);
subtype Square_Matrix is Real_Matrix (1 .. N, 1 .. N); subtype Square_Matrix is Real_Matrix (1 .. N, 1 .. N);
...@@ -606,6 +599,7 @@ package body Ada.Numerics.Generic_Real_Arrays is ...@@ -606,6 +599,7 @@ package body Ada.Numerics.Generic_Real_Arrays is
function Sum_Strict_Upper (M : Square_Matrix) return Real is function Sum_Strict_Upper (M : Square_Matrix) return Real is
Sum : Real := 0.0; Sum : Real := 0.0;
begin begin
for Row in 1 .. N - 1 loop for Row in 1 .. N - 1 loop
for Col in Row + 1 .. N loop for Col in Row + 1 .. N loop
...@@ -803,7 +797,6 @@ package body Ada.Numerics.Generic_Real_Arrays is ...@@ -803,7 +797,6 @@ package body Ada.Numerics.Generic_Real_Arrays is
(Values : in out Real_Vector; (Values : in out Real_Vector;
Vectors : in out Real_Matrix) Vectors : in out Real_Matrix)
is is
procedure Swap (Left, Right : Integer); procedure Swap (Left, Right : Integer);
-- Swap Values (Left) with Values (Right), and also swap the -- Swap Values (Left) with Values (Right), and also swap the
-- corresponding eigenvectors. Note that lowerbounds may differ. -- corresponding eigenvectors. Note that lowerbounds may differ.
...@@ -834,7 +827,6 @@ package body Ada.Numerics.Generic_Real_Arrays is ...@@ -834,7 +827,6 @@ package body Ada.Numerics.Generic_Real_Arrays is
R : Real_Matrix (X'Range (2), X'Range (1)); R : Real_Matrix (X'Range (2), X'Range (1));
begin begin
Transpose (X, R); Transpose (X, R);
return R; return R;
end Transpose; end Transpose;
......
...@@ -2833,7 +2833,7 @@ package body Errout is ...@@ -2833,7 +2833,7 @@ package body Errout is
elsif Msg = "size for& too small, minimum allowed is ^" then elsif Msg = "size for& too small, minimum allowed is ^" then
-- Suppress "size too small" errors in CodePeer mode and ALFA mode, -- Suppress "size too small" errors in CodePeer mode and ALFA mode,
-- since pragma Pack is also ignored in this configuration. -- since pragma Pack is also ignored in these configurations.
if CodePeer_Mode or ALFA_Mode then if CodePeer_Mode or ALFA_Mode then
return True; return True;
......
...@@ -1665,7 +1665,6 @@ package body Exp_Ch11 is ...@@ -1665,7 +1665,6 @@ package body Exp_Ch11 is
-- does not have a choice parameter specification, then we provide one. -- does not have a choice parameter specification, then we provide one.
else else
-- Bypass expansion to a run-time call when back-end exception -- Bypass expansion to a run-time call when back-end exception
-- handling is active, unless the target is a VM or CodePeer. -- handling is active, unless the target is a VM or CodePeer.
......
...@@ -307,6 +307,13 @@ package body Exp_Ch13 is ...@@ -307,6 +307,13 @@ package body Exp_Ch13 is
Delete : Boolean := False; Delete : Boolean := False;
begin begin
-- In formal verification mode, do not generate useless and confusing
-- expansion for freeze nodes.
if ALFA_Mode then
return;
end if;
-- If there are delayed aspect specifications, we insert them just -- If there are delayed aspect specifications, we insert them just
-- before the freeze node. They are already analyzed so we don't need -- before the freeze node. They are already analyzed so we don't need
-- to reanalyze them (they were analyzed before the type was frozen), -- to reanalyze them (they were analyzed before the type was frozen),
......
...@@ -7440,8 +7440,8 @@ package body Exp_Ch7 is ...@@ -7440,8 +7440,8 @@ package body Exp_Ch7 is
------------------------------------ ------------------------------------
function Make_Set_Finalize_Address_Call function Make_Set_Finalize_Address_Call
(Loc : Source_Ptr; (Loc : Source_Ptr;
Typ : Entity_Id; Typ : Entity_Id;
Ptr_Typ : Entity_Id) return Node_Id Ptr_Typ : Entity_Id) return Node_Id
is is
Desig_Typ : constant Entity_Id := Desig_Typ : constant Entity_Id :=
...@@ -7502,12 +7502,12 @@ package body Exp_Ch7 is ...@@ -7502,12 +7502,12 @@ package body Exp_Ch7 is
return return
Make_Procedure_Call_Statement (Loc, Make_Procedure_Call_Statement (Loc,
Name => Name =>
New_Reference_To (RTE (RE_Set_Finalize_Address), Loc), New_Reference_To (RTE (RE_Set_Finalize_Address), Loc),
Parameter_Associations => New_List ( Parameter_Associations => New_List (
New_Reference_To (Finalization_Master (Ptr_Typ), Loc), New_Reference_To (Finalization_Master (Ptr_Typ), Loc),
Make_Attribute_Reference (Loc, Make_Attribute_Reference (Loc,
Prefix => Prefix =>
New_Reference_To (TSS (Utyp, TSS_Finalize_Address), Loc), New_Reference_To (TSS (Utyp, TSS_Finalize_Address), Loc),
Attribute_Name => Name_Unrestricted_Access))); Attribute_Name => Name_Unrestricted_Access)));
end Make_Set_Finalize_Address_Call; end Make_Set_Finalize_Address_Call;
......
...@@ -5290,6 +5290,12 @@ package body Exp_Ch9 is ...@@ -5290,6 +5290,12 @@ package body Exp_Ch9 is
Tasknm : Node_Id; Tasknm : Node_Id;
begin begin
-- Do not expand tasking constructs in formal verification mode
if ALFA_Mode then
return;
end if;
Aggr := Make_Aggregate (Loc, Component_Associations => New_List); Aggr := Make_Aggregate (Loc, Component_Associations => New_List);
Count := 0; Count := 0;
...@@ -5421,6 +5427,12 @@ package body Exp_Ch9 is ...@@ -5421,6 +5427,12 @@ package body Exp_Ch9 is
-- Start of processing for Expand_N_Accept_Statement -- Start of processing for Expand_N_Accept_Statement
begin begin
-- Do not expand tasking constructs in formal verification mode
if ALFA_Mode then
return;
end if;
-- If accept statement is not part of a list, then its parent must be -- If accept statement is not part of a list, then its parent must be
-- an accept alternative, and, as described above, we do not do any -- an accept alternative, and, as described above, we do not do any
-- expansion for such accept statements at this level. -- expansion for such accept statements at this level.
...@@ -5871,6 +5883,12 @@ package body Exp_Ch9 is ...@@ -5871,6 +5883,12 @@ package body Exp_Ch9 is
T : Entity_Id; -- Additional status flag T : Entity_Id; -- Additional status flag
begin begin
-- Do not expand tasking constructs in formal verification mode
if ALFA_Mode then
return;
end if;
Process_Statements_For_Controlled_Objects (Trig); Process_Statements_For_Controlled_Objects (Trig);
Process_Statements_For_Controlled_Objects (Abrt); Process_Statements_For_Controlled_Objects (Abrt);
...@@ -6820,6 +6838,12 @@ package body Exp_Ch9 is ...@@ -6820,6 +6838,12 @@ package body Exp_Ch9 is
S : Entity_Id; -- Primitive operation slot S : Entity_Id; -- Primitive operation slot
begin begin
-- Do not expand tasking constructs in formal verification mode
if ALFA_Mode then
return;
end if;
Process_Statements_For_Controlled_Objects (N); Process_Statements_For_Controlled_Objects (N);
if Ada_Version >= Ada_2005 if Ada_Version >= Ada_2005
...@@ -7136,6 +7160,12 @@ package body Exp_Ch9 is ...@@ -7136,6 +7160,12 @@ package body Exp_Ch9 is
procedure Expand_N_Delay_Relative_Statement (N : Node_Id) is procedure Expand_N_Delay_Relative_Statement (N : Node_Id) is
Loc : constant Source_Ptr := Sloc (N); Loc : constant Source_Ptr := Sloc (N);
begin begin
-- Do not expand tasking constructs in formal verification mode
if ALFA_Mode then
return;
end if;
Rewrite (N, Rewrite (N,
Make_Procedure_Call_Statement (Loc, Make_Procedure_Call_Statement (Loc,
Name => New_Reference_To (RTE (RO_CA_Delay_For), Loc), Name => New_Reference_To (RTE (RO_CA_Delay_For), Loc),
...@@ -7155,6 +7185,12 @@ package body Exp_Ch9 is ...@@ -7155,6 +7185,12 @@ package body Exp_Ch9 is
Typ : Entity_Id; Typ : Entity_Id;
begin begin
-- Do not expand tasking constructs in formal verification mode
if ALFA_Mode then
return;
end if;
if Is_RTE (Base_Type (Etype (Expression (N))), RO_CA_Time) then if Is_RTE (Base_Type (Etype (Expression (N))), RO_CA_Time) then
Typ := RTE (RO_CA_Delay_Until); Typ := RTE (RO_CA_Delay_Until);
else else
...@@ -7175,6 +7211,12 @@ package body Exp_Ch9 is ...@@ -7175,6 +7211,12 @@ package body Exp_Ch9 is
procedure Expand_N_Entry_Body (N : Node_Id) is procedure Expand_N_Entry_Body (N : Node_Id) is
begin begin
-- Do not expand tasking constructs in formal verification mode
if ALFA_Mode then
return;
end if;
-- Associate discriminals with the next protected operation body to be -- Associate discriminals with the next protected operation body to be
-- expanded. -- expanded.
...@@ -7196,6 +7238,12 @@ package body Exp_Ch9 is ...@@ -7196,6 +7238,12 @@ package body Exp_Ch9 is
Index : Node_Id; Index : Node_Id;
begin begin
-- Do not expand tasking constructs in formal verification mode
if ALFA_Mode then
return;
end if;
if No_Run_Time_Mode then if No_Run_Time_Mode then
Error_Msg_CRT ("entry call", N); Error_Msg_CRT ("entry call", N);
return; return;
...@@ -7252,6 +7300,12 @@ package body Exp_Ch9 is ...@@ -7252,6 +7300,12 @@ package body Exp_Ch9 is
Acc_Ent : Entity_Id; Acc_Ent : Entity_Id;
begin begin
-- Do not expand tasking constructs in formal verification mode
if ALFA_Mode then
return;
end if;
Formal := First_Formal (Entry_Ent); Formal := First_Formal (Entry_Ent);
Last_Decl := N; Last_Decl := N;
...@@ -7520,6 +7574,12 @@ package body Exp_Ch9 is ...@@ -7520,6 +7574,12 @@ package body Exp_Ch9 is
-- Start of processing for Expand_N_Protected_Body -- Start of processing for Expand_N_Protected_Body
begin begin
-- Do not expand tasking constructs in formal verification mode
if ALFA_Mode then
return;
end if;
if No_Run_Time_Mode then if No_Run_Time_Mode then
Error_Msg_CRT ("protected body", N); Error_Msg_CRT ("protected body", N);
return; return;
...@@ -7870,6 +7930,12 @@ package body Exp_Ch9 is ...@@ -7870,6 +7930,12 @@ package body Exp_Ch9 is
-- Start of processing for Expand_N_Protected_Type_Declaration -- Start of processing for Expand_N_Protected_Type_Declaration
begin begin
-- Do not expand tasking constructs in formal verification mode
if ALFA_Mode then
return;
end if;
if Present (Corresponding_Record_Type (Prot_Typ)) then if Present (Corresponding_Record_Type (Prot_Typ)) then
return; return;
else else
...@@ -9072,6 +9138,12 @@ package body Exp_Ch9 is ...@@ -9072,6 +9138,12 @@ package body Exp_Ch9 is
-- Start of processing for Expand_N_Requeue_Statement -- Start of processing for Expand_N_Requeue_Statement
begin begin
-- Do not expand tasking constructs in formal verification mode
if ALFA_Mode then
return;
end if;
-- Extract the components of the entry call -- Extract the components of the entry call
Extract_Entry (N, Concval, Ename, Index); Extract_Entry (N, Concval, Ename, Index);
...@@ -9658,6 +9730,12 @@ package body Exp_Ch9 is ...@@ -9658,6 +9730,12 @@ package body Exp_Ch9 is
-- Start of processing for Expand_N_Selective_Accept -- Start of processing for Expand_N_Selective_Accept
begin begin
-- Do not expand tasking constructs in formal verification mode
if ALFA_Mode then
return;
end if;
Process_Statements_For_Controlled_Objects (N); Process_Statements_For_Controlled_Objects (N);
-- First insert some declarations before the select. The first is: -- First insert some declarations before the select. The first is:
...@@ -10288,6 +10366,12 @@ package body Exp_Ch9 is ...@@ -10288,6 +10366,12 @@ package body Exp_Ch9 is
-- Used to determine the proper location of wrapper body insertions -- Used to determine the proper location of wrapper body insertions
begin begin
-- Do not expand tasking constructs in formal verification mode
if ALFA_Mode then
return;
end if;
-- Add renaming declarations for discriminals and a declaration for the -- Add renaming declarations for discriminals and a declaration for the
-- entry family index (if applicable). -- entry family index (if applicable).
...@@ -10493,6 +10577,12 @@ package body Exp_Ch9 is ...@@ -10493,6 +10577,12 @@ package body Exp_Ch9 is
Decl_Stack : Node_Id; Decl_Stack : Node_Id;
begin begin
-- Do not expand tasking constructs in formal verification mode
if ALFA_Mode then
return;
end if;
-- If already expanded, nothing to do -- If already expanded, nothing to do
if Present (Corresponding_Record_Type (Tasktyp)) then if Present (Corresponding_Record_Type (Tasktyp)) then
...@@ -11034,6 +11124,12 @@ package body Exp_Ch9 is ...@@ -11034,6 +11124,12 @@ package body Exp_Ch9 is
S : Entity_Id; -- Primitive operation slot S : Entity_Id; -- Primitive operation slot
begin begin
-- Do not expand tasking constructs in formal verification mode
if ALFA_Mode then
return;
end if;
-- Under the Ravenscar profile, timed entry calls are excluded. An error -- Under the Ravenscar profile, timed entry calls are excluded. An error
-- was already reported on spec, so do not attempt to expand the call. -- was already reported on spec, so do not attempt to expand the call.
......
...@@ -2247,13 +2247,12 @@ package body Freeze is ...@@ -2247,13 +2247,12 @@ package body Freeze is
and then RM_Size (Rec) >= Scalar_Component_Total_RM_Size and then RM_Size (Rec) >= Scalar_Component_Total_RM_Size
-- Never do implicit packing in CodePeer or ALFA modes since -- Never do implicit packing in CodePeer or ALFA modes since
-- we don't do any packing in this mode, since this generates -- we don't do any packing in these modes, since this generates
-- over-complex code that confuses static analysis, and in -- over-complex code that confuses static analysis, and in
-- general, neither CodePeer not GNATprove care about the -- general, neither CodePeer not GNATprove care about the
-- internal representation of objects. -- internal representation of objects.
and then not CodePeer_Mode and then not (CodePeer_Mode or ALFA_Mode)
and then not ALFA_Mode
then then
-- If implicit packing enabled, do it -- If implicit packing enabled, do it
...@@ -3067,8 +3066,7 @@ package body Freeze is ...@@ -3067,8 +3066,7 @@ package body Freeze is
and then not Is_Limited_Composite (E) and then not Is_Limited_Composite (E)
and then not Is_Packed (Root_Type (E)) and then not Is_Packed (Root_Type (E))
and then not Has_Component_Size_Clause (Root_Type (E)) and then not Has_Component_Size_Clause (Root_Type (E))
and then not CodePeer_Mode and then not (CodePeer_Mode or ALFA_Mode)
and then not ALFA_Mode
then then
Get_Index_Bounds (First_Index (E), Lo, Hi); Get_Index_Bounds (First_Index (E), Lo, Hi);
......
...@@ -455,14 +455,18 @@ procedure Gnat1drv is ...@@ -455,14 +455,18 @@ procedure Gnat1drv is
Reset_Style_Check_Options; Reset_Style_Check_Options;
-- Suppress compiler warnings, since what we are -- Suppress compiler warnings, since what we are interested in here
-- interested in here is what formal verification can find out. -- is what formal verification can find out.
Warning_Mode := Suppress; Warning_Mode := Suppress;
-- Suppress the generation of name tables for enumerations -- Suppress the generation of name tables for enumerations
Global_Discard_Names := True; Global_Discard_Names := True;
-- Suppress the expansion of tagged types and dispatching calls
Tagged_Type_Expansion := False;
end if; end if;
end Adjust_Global_Switches; end Adjust_Global_Switches;
......
...@@ -596,6 +596,7 @@ package Lib.Xref is ...@@ -596,6 +596,7 @@ package Lib.Xref is
(CU : Node_Id; (CU : Node_Id;
Process : Node_Processing; Process : Node_Processing;
Inside_Stubs : Boolean); Inside_Stubs : Boolean);
-- This procedure is undocumented ???
procedure Traverse_All_Compilation_Units (Process : Node_Processing); procedure Traverse_All_Compilation_Units (Process : Node_Processing);
-- Call Process on all declarations through all compilation units -- Call Process on all declarations through all compilation units
......
...@@ -722,7 +722,7 @@ package body Prj.Conf is ...@@ -722,7 +722,7 @@ package body Prj.Conf is
-- Hash table to keep the languages used in the project tree -- Hash table to keep the languages used in the project tree
IDE : constant Package_Id := IDE : constant Package_Id :=
Value_Of (Name_Ide, Project.Decl.Packages, Shared); Value_Of (Name_Ide, Project.Decl.Packages, Shared);
procedure Add_Config_Switches_For_Project procedure Add_Config_Switches_For_Project
(Project : Project_Id; (Project : Project_Id;
...@@ -744,6 +744,7 @@ package body Prj.Conf is ...@@ -744,6 +744,7 @@ package body Prj.Conf is
Lang : Name_Id; Lang : Name_Id;
List : String_List_Id; List : String_List_Id;
Elem : String_Element; Elem : String_Element;
begin begin
if Might_Have_Sources (Project) then if Might_Have_Sources (Project) then
Variable := Variable :=
...@@ -813,6 +814,9 @@ package body Prj.Conf is ...@@ -813,6 +814,9 @@ package body Prj.Conf is
procedure For_Every_Imported_Project is new For_Every_Project_Imported procedure For_Every_Imported_Project is new For_Every_Project_Imported
(State => Integer, Action => Add_Config_Switches_For_Project); (State => Integer, Action => Add_Config_Switches_For_Project);
-- Document this procedure ???
-- Local variables
Name : Name_Id; Name : Name_Id;
Count : Natural; Count : Natural;
...@@ -820,6 +824,8 @@ package body Prj.Conf is ...@@ -820,6 +824,8 @@ package body Prj.Conf is
Variable : Variable_Value; Variable : Variable_Value;
Dummy : Integer := 0; Dummy : Integer := 0;
-- Start of processing for Get_Config_Switches
begin begin
For_Every_Imported_Project For_Every_Imported_Project
(By => Project, (By => Project,
...@@ -839,6 +845,7 @@ package body Prj.Conf is ...@@ -839,6 +845,7 @@ package body Prj.Conf is
Count := 1; Count := 1;
Name := Language_Htable.Get_First; Name := Language_Htable.Get_First;
while Name /= No_Name loop while Name /= No_Name loop
-- Check if IDE'Compiler_Command is declared for the language. -- Check if IDE'Compiler_Command is declared for the language.
-- If it is, use its value to invoke gprconfig. -- If it is, use its value to invoke gprconfig.
......
...@@ -29,4 +29,17 @@ ...@@ -29,4 +29,17 @@
-- -- -- --
------------------------------------------------------------------------------ ------------------------------------------------------------------------------
pragma No_Body; -- This package does not require a body, since it is a package renaming. We
-- provide a dummy file containing a No_Body pragma so that previous versions
-- of the body (which did exist) will not interfere.
-- pragma No_Body;
-- The above pragma is commented out, since for now we can't use No_Body in
-- a unit marked as a Compiler_Unit, since this requires GNAT 6.1, and we
-- do not yet require this for bootstrapping. So instead we use a dummy Taft
-- amendment type to require the body:
package body System.Exceptions is
type Require_Body is new Integer;
end System.Exceptions;
...@@ -40,6 +40,21 @@ package System.Exceptions is ...@@ -40,6 +40,21 @@ package System.Exceptions is
-- Visible copy to allow Ada.Exceptions to know the exception model. -- Visible copy to allow Ada.Exceptions to know the exception model.
private private
type Require_Body;
-- Dummy Taft-amendment type to make it legal (and required) to provide
-- a body for this package.
--
-- We do this because this unit used to have a body in earlier versions
-- of GNAT, and it causes various bootstrap path problems etc if we remove
-- a body, since we may pick up old unwanted bodies.
--
-- Note: we use this standard Ada method of requiring a body rather
-- than the cleaner pragma No_Body because System.Exceptions is a compiler
-- unit, and older bootstrap compilers do not support pragma No_Body. This
-- type can be removed, and s-except.adb can be replaced by a source
-- containing just that pragma, when we decide to move to a 2008 compiler
-- as the minimal bootstrap compiler version. ???
ZCX_By_Default : constant Boolean := System.ZCX_By_Default; ZCX_By_Default : constant Boolean := System.ZCX_By_Default;
Foreign_Exception : exception; Foreign_Exception : exception;
......
...@@ -101,6 +101,7 @@ package body System.Generic_Array_Operations is ...@@ -101,6 +101,7 @@ package body System.Generic_Array_Operations is
procedure Back_Substitute (M, N : in out Matrix) is procedure Back_Substitute (M, N : in out Matrix) is
pragma Assert (M'First (1) = N'First (1) and then pragma Assert (M'First (1) = N'First (1) and then
M'Last (1) = N'Last (1)); M'Last (1) = N'Last (1));
Max_Col : Integer := M'Last (2); Max_Col : Integer := M'Last (2);
procedure Sub_Row procedure Sub_Row
...@@ -108,22 +109,27 @@ package body System.Generic_Array_Operations is ...@@ -108,22 +109,27 @@ package body System.Generic_Array_Operations is
Target : Integer; Target : Integer;
Source : Integer; Source : Integer;
Factor : Scalar); Factor : Scalar);
-- Needs comments ???
procedure Sub_Row procedure Sub_Row
(M : in out Matrix; (M : in out Matrix;
Target : Integer; Target : Integer;
Source : Integer; Source : Integer;
Factor : Scalar) is Factor : Scalar)
is
begin begin
for J in M'Range (2) loop for J in M'Range (2) loop
M (Target, J) := M (Target, J) - Factor * M (Source, J); M (Target, J) := M (Target, J) - Factor * M (Source, J);
end loop; end loop;
end Sub_Row; end Sub_Row;
-- Start of processing for Back_Substitute
begin begin
for Row in reverse M'Range (1) loop for Row in reverse M'Range (1) loop
Find_Non_Zero : for Col in M'First (2) .. Max_Col loop Find_Non_Zero : for Col in M'First (2) .. Max_Col loop
if Is_Non_Zero (M (Row, Col)) then if Is_Non_Zero (M (Row, Col)) then
-- Found first non-zero element, so subtract a multiple -- Found first non-zero element, so subtract a multiple
-- of this row from all higher rows, to reduce all other -- of this row from all higher rows, to reduce all other
-- elements in this column to zero. -- elements in this column to zero.
...@@ -160,16 +166,19 @@ package body System.Generic_Array_Operations is ...@@ -160,16 +166,19 @@ package body System.Generic_Array_Operations is
Target : Integer; Target : Integer;
Source : Integer; Source : Integer;
Factor : Scalar); Factor : Scalar);
-- Needs commenting ???
procedure Divide_Row procedure Divide_Row
(M, N : in out Matrix; (M, N : in out Matrix;
Row : Integer; Row : Integer;
Scale : Scalar); Scale : Scalar);
-- Needs commenting ???
procedure Switch_Row procedure Switch_Row
(M, N : in out Matrix; (M, N : in out Matrix;
Row_1 : Integer; Row_1 : Integer;
Row_2 : Integer); Row_2 : Integer);
-- Needs commenting ???
------------- -------------
-- Sub_Row -- -- Sub_Row --
...@@ -179,7 +188,8 @@ package body System.Generic_Array_Operations is ...@@ -179,7 +188,8 @@ package body System.Generic_Array_Operations is
(M : in out Matrix; (M : in out Matrix;
Target : Integer; Target : Integer;
Source : Integer; Source : Integer;
Factor : Scalar) is Factor : Scalar)
is
begin begin
for J in M'Range (2) loop for J in M'Range (2) loop
M (Target, J) := M (Target, J) - Factor * M (Source, J); M (Target, J) := M (Target, J) - Factor * M (Source, J);
...@@ -227,6 +237,8 @@ package body System.Generic_Array_Operations is ...@@ -227,6 +237,8 @@ package body System.Generic_Array_Operations is
Y := T; Y := T;
end Swap; end Swap;
-- Start of processing for Switch_Row
begin begin
if Row_1 /= Row_2 then if Row_1 /= Row_2 then
Det := Zero - Det; Det := Zero - Det;
...@@ -242,17 +254,22 @@ package body System.Generic_Array_Operations is ...@@ -242,17 +254,22 @@ package body System.Generic_Array_Operations is
end if; end if;
end Switch_Row; end Switch_Row;
I : Integer := M'First (1); I : Integer := M'First (1);
-- Avoid use of I ???
-- Start of processing for Forward_Eliminate
begin -- Forward_Eliminate begin
Det := One; Det := One;
for J in M'Range (2) loop for J in M'Range (2) loop
declare declare
Max_I : Integer := I; Max_I : Integer := I;
Max_Abs : Scalar := Zero; Max_Abs : Scalar := Zero;
begin begin
-- Find best pivot in column J, starting in row I. -- Find best pivot in column J, starting in row I
for K in I .. M'Last (1) loop for K in I .. M'Last (1) loop
declare declare
New_Abs : constant Scalar := abs M (K, J); New_Abs : constant Scalar := abs M (K, J);
...@@ -359,6 +376,7 @@ package body System.Generic_Array_Operations is ...@@ -359,6 +376,7 @@ package body System.Generic_Array_Operations is
return Result_Matrix return Result_Matrix
is is
R : Result_Matrix (Left'Range (1), Left'Range (2)); R : Result_Matrix (Left'Range (1), Left'Range (2));
begin begin
if Left'Length (1) /= Right'Length (1) if Left'Length (1) /= Right'Length (1)
or else Left'Length (2) /= Right'Length (2) or else Left'Length (2) /= Right'Length (2)
...@@ -557,6 +575,7 @@ package body System.Generic_Array_Operations is ...@@ -557,6 +575,7 @@ package body System.Generic_Array_Operations is
for K in R'Range (2) loop for K in R'Range (2) loop
declare declare
S : Result_Scalar := Zero; S : Result_Scalar := Zero;
begin begin
for M in Left'Range (2) loop for M in Left'Range (2) loop
S := S + Left (J, M) S := S + Left (J, M)
...@@ -590,6 +609,7 @@ package body System.Generic_Array_Operations is ...@@ -590,6 +609,7 @@ package body System.Generic_Array_Operations is
for J in Left'Range (1) loop for J in Left'Range (1) loop
declare declare
S : Result_Scalar := Zero; S : Result_Scalar := Zero;
begin begin
for K in Left'Range (2) loop for K in Left'Range (2) loop
S := S + Left (J, K) * Right (K - Left'First (2) + Right'First); S := S + Left (J, K) * Right (K - Left'First (2) + Right'First);
......
...@@ -17237,9 +17237,8 @@ package body Sem_Ch3 is ...@@ -17237,9 +17237,8 @@ package body Sem_Ch3 is
-- worst, and therefore defaults are not allowed if the parent is -- worst, and therefore defaults are not allowed if the parent is
-- a generic formal private type (see ACATS B370001). -- a generic formal private type (see ACATS B370001).
if Is_Access_Type (Discr_Type) then if Is_Access_Type (Discr_Type) and then Default_Present then
if Ekind (Discr_Type) /= E_Anonymous_Access_Type if Ekind (Discr_Type) /= E_Anonymous_Access_Type
or else not Default_Present
or else Is_Limited_Record (Current_Scope) or else Is_Limited_Record (Current_Scope)
or else Is_Concurrent_Type (Current_Scope) or else Is_Concurrent_Type (Current_Scope)
or else Is_Concurrent_Record_Type (Current_Scope) or else Is_Concurrent_Record_Type (Current_Scope)
......
...@@ -7052,8 +7052,13 @@ package body Sem_Ch6 is ...@@ -7052,8 +7052,13 @@ package body Sem_Ch6 is
function Controlling_Formal (Prim : Entity_Id) return Entity_Id; function Controlling_Formal (Prim : Entity_Id) return Entity_Id;
-- Return the controlling formal of Prim -- Return the controlling formal of Prim
------------------------
-- Controlling_Formal --
------------------------
function Controlling_Formal (Prim : Entity_Id) return Entity_Id is function Controlling_Formal (Prim : Entity_Id) return Entity_Id is
E : Entity_Id := First_Entity (Prim); E : Entity_Id := First_Entity (Prim);
begin begin
while Present (E) loop while Present (E) loop
if Is_Formal (E) and then Is_Controlling_Formal (E) then if Is_Formal (E) and then Is_Controlling_Formal (E) then
......
...@@ -7953,8 +7953,8 @@ package body Sem_Util is ...@@ -7953,8 +7953,8 @@ package body Sem_Util is
-------------------------------------------------- --------------------------------------------------
function Is_Subprogram_Stub_Without_Prior_Declaration function Is_Subprogram_Stub_Without_Prior_Declaration
(N : Node_Id) return Boolean is (N : Node_Id) return Boolean
is
begin begin
-- A subprogram stub without prior declaration serves as declaration for -- A subprogram stub without prior declaration serves as declaration for
-- the actual subprogram body. As such, it has an attached defining -- the actual subprogram body. As such, it has an attached defining
......
...@@ -1748,14 +1748,15 @@ package body Sem_Warn is ...@@ -1748,14 +1748,15 @@ package body Sem_Warn is
SE : constant Entity_Id := Scope (E); SE : constant Entity_Id := Scope (E);
function Within_Postcondition return Boolean; function Within_Postcondition return Boolean;
-- Returns True iff N is within a Precondition -- Returns True iff N is within a Postcondition or
-- Ensures component in a Test_Case.
-------------------------- --------------------------
-- Within_Postcondition -- -- Within_Postcondition --
-------------------------- --------------------------
function Within_Postcondition return Boolean is function Within_Postcondition return Boolean is
Nod : Node_Id; Nod, P : Node_Id;
begin begin
Nod := Parent (N); Nod := Parent (N);
...@@ -1764,6 +1765,17 @@ package body Sem_Warn is ...@@ -1764,6 +1765,17 @@ package body Sem_Warn is
and then Pragma_Name (Nod) = Name_Postcondition and then Pragma_Name (Nod) = Name_Postcondition
then then
return True; return True;
elsif Present (Parent (Nod)) then
P := Parent (Nod);
if Nkind (P) = N_Pragma
and then Pragma_Name (P) = Name_Test_Case
and then
Nod = Get_Ensures_From_Test_Case_Pragma (P)
then
return True;
end if;
end if; end if;
Nod := Parent (Nod); Nod := Parent (Nod);
...@@ -1893,8 +1905,8 @@ package body Sem_Warn is ...@@ -1893,8 +1905,8 @@ package body Sem_Warn is
end if; end if;
-- One more check, don't bother if we are within a -- One more check, don't bother if we are within a
-- postcondition pragma, since the expression occurs -- postcondition, since the expression occurs in a
-- in a place unrelated to the actual test. -- place unrelated to the actual test.
if not Within_Postcondition then if not Within_Postcondition then
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment