+2013-10-17 Robert Dewar <dewar@adacore.com>
+
+ * sem_prag.adb (Record_Possible_Body_Reference): Fix test for
+ being in body.
+ (Add_Constituent): Merged into Check_Refined_Global_Item.
+ (Check_Matching_Constituent): A constituent that has the proper Part_Of
+ option and comes from a private child or a sibling is now collected.
+ (Check_Matching_Modes): Merged into Check_Refined_Global_Item.
+ (Check_Refined_Global_Item): Code cleanup.
+ (Collect_Constituent): New routine.
+ (Inconsistent_Mode_Error): Moved out from Check_Matching_Modes.
+
+2013-10-17 Ed Schonberg <schonberg@adacore.com>
+
+ * freeze.adb (Check_Current_Instance, Process): Add RM reference
+ and mention immutably limited types, when the current instance
+ is illegal in Ada 2012.
+
+2013-10-17 Ed Schonberg <schonberg@adacore.com>
+
+ * sem_warn.adb (Check_Unused_Withs): If the main unit is a
+ subunit, apply the check to the units mentioned in its context
+ only. This provides additional warnings on with_clauses that
+ are superfluous.
+
+2013-10-17 Hristian Kirtchev <kirtchev@adacore.com>
+
+ * sem_ch3.adb (Analyze_Declarations): Emit an
+ error message concerning state refinement when the spec defines at
+ least one non-null abstract state and the body's SPARK mode is On.
+ (Requires_State_Refinement): New routine.
+
+2013-10-17 Robert Dewar <dewar@adacore.com>
+
+ * sem_ch7.ads: Comment fixes.
+
+2013-10-17 Robert Dewar <dewar@adacore.com>
+
+ * sem_ch7.adb (Analyze_Package_Specification): Remove circuit
+ for ensuring that a package spec requires a body for some other
+ reason than that it contains the declaration of an abstract state.
+
+2013-10-17 Tristan Gingold <gingold@adacore.com>
+
+ * exp_ch11.adb (Expand_N_Raise_Expression): Fix call of
+ Possible_Local_Raise.
+
+2013-10-17 Thomas Quinot <quinot@adacore.com>
+
+ * exp_pakd.adb (Expand_Bit_Packed_Element_Set): Unchecked
+ conversion of Or_Rhs to Etype of New_Rhs is required only when
+ the latter is the result of a byte swap operation.
+
+2013-10-17 Thomas Quinot <quinot@adacore.com>
+
+ * exp_dist.adb (Build_To_Any_Function): For a type with opaque
+ representation that is not transmitted as an unconstrained value,
+ use 'Write, not 'Output, to generate the opaque representation.
+
+2013-10-17 Yannick Moy <moy@adacore.com>
+
+ * sem_res.adb (Resolve_Short_Circuit): Only
+ generate expression-with-action when full expansion is set.
+
+2013-10-17 Yannick Moy <moy@adacore.com>
+
+ * debug.adb Remove obsolete comment.
+
+2013-10-17 Thomas Quinot <quinot@adacore.com>
+
+ * exp_ch4.adb (Process_Transient_Object.Find_Enclosing_Contexts):
+ Avoid late insertion when expanding an expression with action
+ nested within a transient block; Do not inconditionally generate
+ a finalization call if the generated object is from a specific
+ branch of a conditional expression.
+
+2013-10-17 Pascal Obry <obry@adacore.com>
+
+ * g-arrspl.adb: Ensure Finalize call is idempotent.
+ * g-arrspl.adb (Finalize): Makes the call idempotent.
+
2013-10-17 Hristian Kirtchev <kirtchev@adacore.com>
* sem_prag.adb (Is_Matching_Input): Account
RCE : Node_Id;
begin
- Possible_Local_Raise (N, Name (N));
+ Possible_Local_Raise (N, Entity (Name (N)));
-- Later we must teach the back end/gigi how to deal with this, but
-- for now we will assume the type is Standard_Boolean and transform
-- Constrained and unconstrained array types
declare
- Constrained : constant Boolean := Is_Constrained (Typ);
+ Constrained : constant Boolean :=
+ not Transmit_As_Unconstrained (Typ);
procedure TA_Ary_Add_Process_Element
(Stmts : List_Id;
-- Generate:
-- T'Output (Strm'Access, E);
+ -- or
+ -- T'Write (Strm'Access, E);
+ -- depending on whether to transmit as unconstrained
- Append_To (Stms,
- Make_Attribute_Reference (Loc,
- Prefix => New_Occurrence_Of (Typ, Loc),
- Attribute_Name => Name_Output,
- Expressions => New_List (
- Make_Attribute_Reference (Loc,
- Prefix => New_Occurrence_Of (Strm, Loc),
- Attribute_Name => Name_Access),
- New_Occurrence_Of (Expr_Parameter, Loc))));
+ declare
+ Attr_Name : Name_Id;
+ begin
+ if Transmit_As_Unconstrained (Typ) then
+ Attr_Name := Name_Output;
+ else
+ Attr_Name := Name_Write;
+ end if;
+
+ Append_To (Stms,
+ Make_Attribute_Reference (Loc,
+ Prefix => New_Occurrence_Of (Typ, Loc),
+ Attribute_Name => Attr_Name,
+ Expressions => New_List (
+ Make_Attribute_Reference (Loc,
+ Prefix => New_Occurrence_Of (Strm, Loc),
+ Attribute_Name => Name_Access),
+ New_Occurrence_Of (Expr_Parameter, Loc))));
+ end;
-- Generate:
-- BS_To_Any (Strm, A);
Set_Etype (New_Rhs, Etype (Left_Opnd (New_Rhs)));
end if;
+ -- If New_Rhs has been byte swapped, need to convert Or_Rhs
+ -- to the return type of the byte swapping function now.
+
+ if Require_Byte_Swapping then
+ Or_Rhs := Unchecked_Convert_To (Etype (New_Rhs), Or_Rhs);
+ end if;
+
New_Rhs :=
Make_Op_Or (Loc,
Left_Opnd => New_Rhs,
- Right_Opnd => Unchecked_Convert_To
- (Etype (New_Rhs), Or_Rhs));
+ Right_Opnd => Or_Rhs);
end;
end if;
and then Is_Type (Entity (Prefix (N)))
and then Entity (Prefix (N)) = E
then
- Error_Msg_N
- ("current instance must be a limited type", Prefix (N));
+ if Ada_Version < Ada_2012 then
+ Error_Msg_N
+ ("current instance must be a limited type",
+ Prefix (N));
+ else
+ Error_Msg_N
+ ("current instance must be an immutably limited " &
+ "type (RM-2012, 7.5 (8.1/3))",
+ Prefix (N));
+ end if;
return Abandon;
else
return OK;
-- If the states have visible refinement, remove the visibility of each
-- constituent at the end of the package body declarations.
+ function Requires_State_Refinement
+ (Spec_Id : Entity_Id;
+ Body_Id : Entity_Id) return Boolean;
+ -- Determine whether a package denoted by its spec and body entities
+ -- requires refinement of abstract states.
+
-----------------
-- Adjust_Decl --
-----------------
end if;
end Remove_Visible_Refinements;
+ -------------------------------
+ -- Requires_State_Refinement --
+ -------------------------------
+
+ function Requires_State_Refinement
+ (Spec_Id : Entity_Id;
+ Body_Id : Entity_Id) return Boolean
+ is
+ function Mode_Is_Off (Prag : Node_Id) return Boolean;
+ -- Given pragma SPARK_Mode, determine whether the mode is Off
+
+ -----------------
+ -- Mode_Is_Off --
+ -----------------
+
+ function Mode_Is_Off (Prag : Node_Id) return Boolean is
+ Mode : Node_Id;
+
+ begin
+ -- The default SPARK mode is On
+
+ if No (Prag) then
+ return False;
+ end if;
+
+ Mode :=
+ Get_Pragma_Arg (First (Pragma_Argument_Associations (Prag)));
+
+ -- Then the pragma lacks an argument, the default mode is On
+
+ if No (Mode) then
+ return False;
+ else
+ return Chars (Mode) = Name_Off;
+ end if;
+ end Mode_Is_Off;
+
+ -- Start of processing for Requires_State_Refinement
+
+ begin
+ -- A package that does not define at least one abstract state cannot
+ -- possibly require refinement.
+
+ if No (Abstract_States (Spec_Id)) then
+ return False;
+
+ -- The package instroduces a single null state which does not merit
+ -- refinement.
+
+ elsif Has_Null_Abstract_State (Spec_Id) then
+ return False;
+
+ -- Check whether the package body is subject to pragma SPARK_Mode. If
+ -- it is and the mode is Off, the package body is considered to be in
+ -- regular Ada and does not require refinement.
+
+ elsif Mode_Is_Off (SPARK_Mode_Pragmas (Body_Id)) then
+ return False;
+
+ -- The body's SPARK_Mode may be inherited from a similar pragma that
+ -- appears in the private declarations of the spec. The pragma we are
+ -- interested appears as the second entry in SPARK_Mode_Pragmas.
+
+ elsif Present (SPARK_Mode_Pragmas (Spec_Id))
+ and then Mode_Is_Off (Next_Pragma (SPARK_Mode_Pragmas (Spec_Id)))
+ then
+ return False;
+
+ -- The spec defines at least one abstract state and the body has no
+ -- way of circumventing the refinement.
+
+ else
+ return True;
+ end if;
+ end Requires_State_Refinement;
+
-- Local variables
Body_Id : Entity_Id;
-- State refinement is required when the package declaration has
-- abstract states. Null states are not considered.
- elsif Present (Abstract_States (Spec_Id))
- and then not Has_Null_Abstract_State (Spec_Id)
- then
+ elsif Requires_State_Refinement (Spec_Id, Body_Id) then
Error_Msg_NE
("package & requires state refinement", Context, Spec_Id);
end if;
Check_One_Tagged_Type_Or_Extension_At_Most;
- -- Issue an error if a package that is a library unit does not require a
- -- body, and we have a non-null abstract state (SPARK LRM 7.1.5(4)).
-
- if not Unit_Requires_Body (Id, Ignore_Abstract_State => True)
- and then Present (Abstract_States (Id))
-
- -- We use Scope_Depth of 1 to identify library units, which seems a
- -- bit ugly, but there doesn't seem to be an easier way.
-
- and then Scope_Depth (Id) = 1
-
- -- A null abstract state always appears as the sole element of the
- -- state list.
-
- and then not Is_Null_State (Node (First_Elmt (Abstract_States (Id))))
- then
- declare
- P : constant Node_Id := Get_Pragma (Id, Pragma_Abstract_State);
- begin
- Error_Msg_NE
- ("package & specifies a non-null abstract state", P, Id);
- Error_Msg_N
- ("\but package does not otherwise require a body", P);
- Error_Msg_N
- ("\pragma Elaborate_Body is required in this case", P);
- end;
- end if;
-
-- If switch set, output information on why body required
if List_Body_Required_Info
-- Ignore_Abstract_State is set True, then the test for a non-null abstract
-- state (which normally requires a body) is not carried out. This allows
-- the use of this routine to tell if there is some other reason that a
- -- body is required (as is required for analyzing Abstract_State).
+ -- body is required (as is required for analyzing Abstract_State). This
+ -- is not currently used, but may be useful in future if we implement a
+ -- compatibility mode which warns about possible incompatibilities if a
+ -- SPARK 2014 program is compiled with a SPARK-unaware compiler.
procedure May_Need_Implicit_Body (E : Entity_Id);
-- If a package declaration contains tasks or RACWs and does not require
Analyze (Par_State);
- -- Part_Of specified a legal state
+ -- Part_Of specified a legal state, this automatically
+ -- makes the state a constituent.
if Is_Entity_Name (Par_State)
and then Present (Entity (Par_State))
(Item : Node_Id;
Global_Mode : Name_Id)
is
- procedure Add_Constituent (Item_Id : Entity_Id);
- -- Add a single constituent to one of the three constituent lists
- -- depending on Global_Mode.
+ Item_Id : constant Entity_Id := Entity_Of (Item);
- procedure Check_Matching_Modes (Item_Id : Entity_Id);
- -- Verify that the global modes of item Item_Id are the same in
- -- both pragmas Global and Refined_Global.
+ procedure Inconsistent_Mode_Error (Expect : Name_Id);
+ -- Issue a common error message for all mode mismatches. Expect
+ -- denotes the expected mode.
- ---------------------
- -- Add_Constituent --
- ---------------------
+ -----------------------------
+ -- Inconsistent_Mode_Error --
+ -----------------------------
- procedure Add_Constituent (Item_Id : Entity_Id) is
+ procedure Inconsistent_Mode_Error (Expect : Name_Id) is
begin
+ Error_Msg_NE
+ ("global item & has inconsistent modes", Item, Item_Id);
+
+ Error_Msg_Name_1 := Global_Mode;
+ Error_Msg_N ("\ expected mode %", Item);
+
+ Error_Msg_Name_1 := Expect;
+ Error_Msg_N ("\ found mode %", Item);
+ end Inconsistent_Mode_Error;
+
+ -- Start of processing for Check_Refined_Global_Item
+
+ begin
+ -- The state or variable acts as a constituent of a state, collect
+ -- it for the state completeness checks performed later on.
+
+ if Present (Refined_State (Item_Id)) then
if Global_Mode = Name_Input then
Add_Item (Item_Id, In_Constits);
elsif Global_Mode = Name_Output then
Add_Item (Item_Id, Out_Constits);
end if;
- end Add_Constituent;
-
- --------------------------
- -- Check_Matching_Modes --
- --------------------------
-
- procedure Check_Matching_Modes (Item_Id : Entity_Id) is
- procedure Inconsistent_Mode_Error (Expect : Name_Id);
- -- Issue a common error message for all mode mismatche. Expect
- -- denotes the expected mode.
- -----------------------------
- -- Inconsistent_Mode_Error --
- -----------------------------
+ -- When not a constituent, ensure that both occurrences of the
+ -- item in pragmas Global and Refined_Global match.
- procedure Inconsistent_Mode_Error (Expect : Name_Id) is
- begin
- Error_Msg_NE
- ("global item & has inconsistent modes", Item, Item_Id);
-
- Error_Msg_Name_1 := Global_Mode;
- Error_Msg_N ("\ expected mode %", Item);
-
- Error_Msg_Name_1 := Expect;
- Error_Msg_N ("\ found mode %", Item);
- end Inconsistent_Mode_Error;
-
- -- Start processing for Check_Matching_Modes
-
- begin
- if Contains (In_Items, Item_Id) then
- if Global_Mode /= Name_Input then
- Inconsistent_Mode_Error (Name_Input);
- end if;
-
- elsif Contains (In_Out_Items, Item_Id) then
- if Global_Mode /= Name_In_Out then
- Inconsistent_Mode_Error (Name_In_Out);
- end if;
-
- elsif Contains (Out_Items, Item_Id) then
- if Global_Mode /= Name_Output then
- Inconsistent_Mode_Error (Name_Output);
- end if;
-
- -- The item does not appear in the corresponding Global aspect,
- -- it must be an extra.
-
- else
- Error_Msg_NE ("extra global item &", Item, Item_Id);
+ elsif Contains (In_Items, Item_Id) then
+ if Global_Mode /= Name_Input then
+ Inconsistent_Mode_Error (Name_Input);
end if;
- end Check_Matching_Modes;
-
- -- Local variables
- Item_Id : constant Entity_Id := Entity_Of (Item);
-
- -- Start of processing for Check_Refined_Global_Item
-
- begin
- if Ekind (Item_Id) = E_Abstract_State then
-
- -- The state is neither a constituent of an ancestor state nor
- -- has a visible refinement. Ensure that the modes of both its
- -- occurrences in Global and Refined_Global match.
-
- if No (Refined_State (Item_Id))
- and then not Has_Visible_Refinement (Item_Id)
- then
- Check_Matching_Modes (Item_Id);
+ elsif Contains (In_Out_Items, Item_Id) then
+ if Global_Mode /= Name_In_Out then
+ Inconsistent_Mode_Error (Name_In_Out);
end if;
- else pragma Assert (Ekind (Item_Id) = E_Variable);
-
- -- The variable acts as a constituent of a state, collect it
- -- for the state completeness checks performed later on.
-
- if Present (Refined_State (Item_Id)) then
- Add_Constituent (Item_Id);
+ elsif Contains (Out_Items, Item_Id) then
+ if Global_Mode /= Name_Output then
+ Inconsistent_Mode_Error (Name_Output);
+ end if;
- -- The variable is not a constituent. Ensure that the modes of
- -- both its occurrences in Global and Refined_Global match.
+ -- The item does not appear in the corresponding Global pragma, it
+ -- must be an extra.
- else
- Check_Matching_Modes (Item_Id);
- end if;
+ else
+ Error_Msg_NE ("extra global item &", Item, Item_Id);
end if;
end Check_Refined_Global_Item;
--------------------------------
procedure Check_Matching_Constituent (Constit_Id : Entity_Id) is
+ procedure Collect_Constituent;
+ -- Add constituent Constit_Id to the refinements of State_Id
+
+ -------------------------
+ -- Collect_Constituent --
+ -------------------------
+
+ procedure Collect_Constituent is
+ begin
+ -- Add the constituent to the lis of processed items to aid
+ -- with the detection of duplicates.
+
+ Add_Item (Constit_Id, Constituents_Seen);
+
+ -- Collect the constituent in the list of refinement items.
+ -- Establish a relation between the refined state and its
+ -- constituent.
+
+ Append_Elmt (Constit_Id, Refinement_Constituents (State_Id));
+ Set_Refined_State (Constit_Id, State_Id);
+
+ -- The state has at least one legal constituent, mark the
+ -- start of the refinement region. The region ends when the
+ -- body declarations end (see routine Analyze_Declarations).
+
+ Set_Has_Visible_Refinement (State_Id);
+ end Collect_Constituent;
+
+ -- Local variables
+
State_Elmt : Elmt_Id;
+ -- Start of processing for Check_Matching_Constituent
+
begin
-- Detect a duplicate use of a constituent
-- The constituent has the proper Part_Of option, but may
-- not appear in the immediate hidden state of the related
- -- package. This case arises when the constituent comes from
- -- a private child or a private sibling. Recognize these
- -- scenarios to avoid generating a bogus error message.
+ -- package. This case arises when the constituent appears
+ -- in a private child or a private sibling. Recognize these
+ -- scenarios and collect the constituent.
elsif Is_Child_Or_Sibling
(Pack_1 => Scope (State_Id),
Pack_2 => Scope (Constit_Id),
Private_Child => True)
then
+ Collect_Constituent;
return;
end if;
end if;
Add_Item (Constit_Id, Constituents_Seen);
Remove_Elmt (Hidden_States, State_Elmt);
- -- Collect the constituent in the list of refinement
- -- items. Establish a relation between the refined
- -- state and its constituent.
-
- Append_Elmt
- (Constit_Id, Refinement_Constituents (State_Id));
- Set_Refined_State (Constit_Id, State_Id);
-
- -- The state has at least one legal constituent, mark
- -- the start of the refinement region. The region ends
- -- when the body declarations end (see routine
- -- Analyze_Declarations).
-
- Set_Has_Visible_Refinement (State_Id);
-
+ Collect_Constituent;
return;
end if;
Item_Id : Entity_Id)
is
begin
- if In_Package_Body
+ if Is_Body_Name (Unit_Name (Get_Source_Unit (Item)))
and then Ekind (Item_Id) = E_Abstract_State
then
if not Has_Body_References (Item_Id) then
return;
end if;
- -- Flag any unused with clauses, but skip this step if we are compiling
- -- a subunit on its own, since we do not have enough information to
- -- determine whether with's are used. We will get the relevant warnings
- -- when we compile the parent. This is the normal style of GNAT
- -- compilation in any case.
+ -- Flag any unused with clauses. For a subunit, check only the units
+ -- in its context, not those of the parent, which may be needed by other
+ -- subunits. We will get the full warnings when we compile the parent,
+ -- but the following is helpful when compiling a subunit by itself.
if Nkind (Unit (Cunit (Main_Unit))) = N_Subunit then
+ if Current_Sem_Unit = Main_Unit then
+ Check_One_Unit (Main_Unit);
+ end if;
+
return;
end if;
projects / gcc.git / commitdiff