+2016-06-22 Ed Schonberg <schonberg@adacore.com>
+
+ * exp_ch4.adb (In_Range_Chec)): New predicate, subsidiary of
+ Expand_N_In: within an expanded range check that might raise
+ Constraint_Error do not generate a predicate check as well. It
+ is redundant because the context will add an explicit predicate
+ check, and it will raise the wrong exception if it fails.
+ * lib-xref-spark_specific.adb (Add_SPARK_File): Remove useless checks
+ since dependency units always have an associated compilation unit.
+
2016-06-22 Arnaud Charlet <charlet@adacore.com>
* lib.ads: Code cleanup.
-- (the check is only done when the right operand is a subtype; see
-- RM12-4.5.2 (28.1/3-30/3)).
- declare
+ Predicate_Check : declare
+ function In_Range_Check return Boolean;
+ -- Within an expanded range check that may raise Constraint_Error do
+ -- not generate a predicate check as well. It is redundant because
+ -- the context will add an explicit predicate check, and it will
+ -- raise the wrong exception if it fails.
+
+ --------------------
+ -- In_Range_Check --
+ --------------------
+
+ function In_Range_Check return Boolean is
+ P : Node_Id;
+ begin
+ P := Parent (N);
+ while Present (P) loop
+ if Nkind (P) = N_Raise_Constraint_Error then
+ return True;
+
+ elsif Nkind (P) in N_Statement_Other_Than_Procedure_Call
+ or else Nkind (P) = N_Procedure_Call_Statement
+ or else Nkind (P) in N_Declaration
+ then
+ return False;
+ end if;
+
+ P := Parent (P);
+ end loop;
+
+ return False;
+ end In_Range_Check;
+
+ -- Local variables
+
PFunc : constant Entity_Id := Predicate_Function (Rtyp);
+ R_Op : Node_Id;
+
+ -- Start of processing for Predicate_Check
begin
if Present (PFunc)
and then Current_Scope /= PFunc
and then Nkind (Rop) /= N_Range
then
+ if not In_Range_Check then
+ R_Op := Make_Predicate_Call (Rtyp, Lop, Mem => True);
+ else
+ R_Op := New_Occurrence_Of (Standard_True, Loc);
+ end if;
+
Rewrite (N,
Make_And_Then (Loc,
Left_Opnd => Relocate_Node (N),
- Right_Opnd => Make_Predicate_Call (Rtyp, Lop, Mem => True)));
+ Right_Opnd => R_Op));
-- Analyze new expression, mark left operand as analyzed to
-- avoid infinite recursion adding predicate calls. Similarly,
return;
end if;
- end;
+ end Predicate_Check;
end Expand_N_In;
--------------------------------
-- Subunits are traversed as part of the top-level unit to which they
-- belong.
- if Present (Cunit (Ubody))
- and then Nkind (Unit (Cunit (Ubody))) = N_Subunit
- then
+ if Nkind (Unit (Cunit (Ubody))) = N_Subunit then
return;
end if;
From := SPARK_Scope_Table.Last + 1;
- -- Unit might not have an associated compilation unit, as seen in code
- -- filling Sdep_Table in Write_ALI.
-
- if Present (Cunit (Ubody)) then
- Traverse_Compilation_Unit
- (CU => Cunit (Ubody),
- Process => Detect_And_Add_SPARK_Scope'Access,
- Inside_Stubs => True);
- end if;
+ Traverse_Compilation_Unit
+ (CU => Cunit (Ubody),
+ Process => Detect_And_Add_SPARK_Scope'Access,
+ Inside_Stubs => True);
-- When two units are present for the same compilation unit, as it
-- happens for library-level instantiations of generics, then add all
-- scopes to the same SPARK file.
if Ubody /= Uspec then
- if Present (Cunit (Uspec)) then
- Traverse_Compilation_Unit
- (CU => Cunit (Uspec),
- Process => Detect_And_Add_SPARK_Scope'Access,
- Inside_Stubs => True);
- end if;
+ Traverse_Compilation_Unit
+ (CU => Cunit (Uspec),
+ Process => Detect_And_Add_SPARK_Scope'Access,
+ Inside_Stubs => True);
end if;
-- Update scope numbers
-- For subunits, also retrieve the file name of the unit. Only do so if
-- unit has an associated compilation unit.
- if Present (Cunit (Uspec))
- and then Present (Cunit (Unit (File)))
+ if Present (Cunit (Unit (File)))
and then Nkind (Unit (Cunit (Unit (File)))) = N_Subunit
then
Get_Name_String (Reference_Name (Main_Source_File));