+2017-09-08 Javier Miranda <miranda@adacore.com>
+
+ * exp_ch4.adb (Expand_N_Op_Divide): Reordering code that handles
+ divisions with fixed point results to avoid generating twice
+ the runtime check on divide by zero.
+ * checks.adb (Apply_Divide_Checks): Ensure that operands are
+ not evaluated twice (once for their runtime checks and once for
+ their regular computation).
+
+2017-09-08 Yannick Moy <moy@adacore.com>
+
+ * sem_prag.adb (Analyze_Part_Of): Add missing
+ return statements after issuing errors. Add detection of
+ out-of-order item and single concurrent type.
+
2017-09-08 Nicolas Roche <roche@adacore.com>
* gcc-interface/Makefile.in, a-extiti.ads, s-taprop-linux.adb,
if Is_Fixed_Point_Type (Typ) then
+ -- No special processing if Treat_Fixed_As_Integer is set, since
+ -- from a semantic point of view such operations are simply integer
+ -- operations and will be treated that way.
+
+ if not Treat_Fixed_As_Integer (N) then
+ if Is_Integer_Type (Rtyp) then
+ Expand_Divide_Fixed_By_Integer_Giving_Fixed (N);
+ else
+ Expand_Divide_Fixed_By_Fixed_Giving_Fixed (N);
+ end if;
+ end if;
+
-- Deal with divide-by-zero check if back end cannot handle them
-- and the flag is set indicating that we need such a check. Note
-- that we don't need to bother here with the case of mixed-mode
-- (Right operand an integer type), since these will be rewritten
-- with conversions to a divide with a fixed-point right operand.
- if Do_Division_Check (N)
+ if Nkind (N) = N_Op_Divide
+ and then Do_Division_Check (N)
and then not Backend_Divide_Checks_On_Target
and then not Is_Integer_Type (Rtyp)
then
Reason => CE_Divide_By_Zero));
end if;
- -- No special processing if Treat_Fixed_As_Integer is set, since
- -- from a semantic point of view such operations are simply integer
- -- operations and will be treated that way.
-
- if not Treat_Fixed_As_Integer (N) then
- if Is_Integer_Type (Rtyp) then
- Expand_Divide_Fixed_By_Integer_Giving_Fixed (N);
- else
- Expand_Divide_Fixed_By_Fixed_Giving_Fixed (N);
- end if;
- end if;
-
-- Other cases of division of fixed-point operands. Again we exclude the
-- case where Treat_Fixed_As_Integer is set.
SPARK_Msg_NE
("\& is not part of the hidden state of package %",
Indic, Item_Id);
+ return;
-- The item appears in the visible state space of some package. In
-- general this scenario does not warrant Part_Of except when the
("indicator Part_Of must denote abstract state or public "
& "descendant of & (SPARK RM 7.2.6(3))",
Indic, Parent_Unit);
+ return;
elsif Scope (Encap_Id) = Parent_Unit
or else
("indicator Part_Of must denote abstract state or public "
& "descendant of & (SPARK RM 7.2.6(3))",
Indic, Parent_Unit);
+ return;
end if;
-- Indicator Part_Of is not needed when the related package is not
SPARK_Msg_NE
("\& is declared in the visible part of package %",
Indic, Item_Id);
+ return;
end if;
-- When the item appears in the private state space of a package, the
SPARK_Msg_NE
("\& is declared in the private part of package %",
Indic, Item_Id);
+ return;
end if;
-- Items declared in the body state space of a package do not need
SPARK_Msg_NE
("\& is declared in the body of package %", Indic, Item_Id);
end if;
+
+ return;
end if;
-- The encapsulator is a single concurrent type
SPARK_Msg_NE
(Fix_Msg (Encap_Typ, "constant & cannot act as constituent of "
& "single protected type %"), Indic, Item_Id);
+ return;
-- The constituent is a package instantiation
SPARK_Msg_NE
(Fix_Msg (Encap_Typ, "package instantiation & cannot act as "
& "constituent of single protected type %"), Indic, Item_Id);
+ return;
end if;
-- When the item denotes an abstract state of a nested package, use
(Fix_Msg (Encap_Typ, "constituent & must be declared "
& "immediately within the same region as single protected "
& "type %"), Indic, Item_Id);
+ return;
end if;
+
+ -- The declaration of the item should follow the declaration of its
+ -- encapsulating single concurrent type and must appear in the same
+ -- declarative region (SPARK RM 9.3).
+
+ declare
+ N : Node_Id;
+
+ begin
+ N := Next (Declaration_Node (Encap_Id));
+ while Present (N) loop
+ exit when N = Item_Decl;
+ Next (N);
+ end loop;
+
+ -- The single concurrent type might be in the visible part of a
+ -- package, and the declaration of the item in the private part
+ -- of the same package.
+
+ if No (N) then
+ declare
+ Pack : constant Node_Id :=
+ Parent (Declaration_Node (Encap_Id));
+ begin
+ if Nkind (Pack) = N_Package_Specification
+ and then not In_Private_Part (Encap_Id)
+ then
+ N := First (Private_Declarations (Pack));
+ while Present (N) loop
+ exit when N = Item_Decl;
+ Next (N);
+ end loop;
+ end if;
+ end;
+ end if;
+
+ if No (N) then
+ SPARK_Msg_N
+ ("indicator Part_Of must denote a previously declared "
+ & "single protected type or single task type", Encap);
+ return;
+ end if;
+ end;
end if;
Legal := True;
projects / gcc.git / commitdiff