(Item_Is_Input : out Boolean;
Item_Is_Output : out Boolean)
is
- -- A constant or IN parameter of access type should be handled
- -- like a variable, as the underlying memory pointed-to can be
- -- modified. Use Adjusted_Kind to do this adjustment.
+ -- A constant or IN parameter of access-to-variable type should be
+ -- handled like a variable, as the underlying memory pointed-to
+ -- can be modified. Use Adjusted_Kind to do this adjustment.
Adjusted_Kind : Entity_Kind := Ekind (Item_Id);
if Ekind (Item_Id) in E_Constant
| E_Generic_In_Parameter
| E_In_Parameter
- and then Is_Access_Type (Etype (Item_Id))
+ and then Is_Access_Variable (Etype (Item_Id))
then
Adjusted_Kind := E_Variable;
end if;
-- clause as this will lead to misleading errors.
if Has_Extra_Parentheses (Deps) then
- return;
+ goto Leave;
end if;
if Present (Component_Associations (Deps)) then
else
Error_Msg_N ("malformed dependency relation", Deps);
- return;
+ goto Leave;
end if;
-- The top level dependency relation is malformed. This is a syntax
Add_To_Config_Boolean_Restrictions (No_Elaboration_Code);
end if;
- -- Special processing for No_Tasking restriction placed in
- -- a configuration pragmas file.
+ -- Special processing for No_Tasking restriction (not just a
+ -- warning) when it appears as a configuration pragma.
- elsif R_Id = No_Tasking and then No (Cunit (Main_Unit)) then
+ elsif R_Id = No_Tasking
+ and then No (Cunit (Main_Unit))
+ and then not Warn
+ then
Set_Global_No_Tasking;
end if;
-- ASSERTION_KIND ::= RM_ASSERTION_KIND | ID_ASSERTION_KIND
- -- RM_ASSERTION_KIND ::= Assert |
- -- Static_Predicate |
- -- Dynamic_Predicate |
- -- Pre |
- -- Pre'Class |
- -- Post |
- -- Post'Class |
- -- Type_Invariant |
- -- Type_Invariant'Class
-
- -- ID_ASSERTION_KIND ::= Assert_And_Cut |
- -- Assume |
- -- Contract_Cases |
- -- Debug |
- -- Default_Initial_Condition |
- -- Ghost |
- -- Initial_Condition |
- -- Loop_Invariant |
- -- Loop_Variant |
- -- Postcondition |
- -- Precondition |
- -- Predicate |
- -- Refined_Post |
- -- Statement_Assertions
+ -- RM_ASSERTION_KIND ::= Assert |
+ -- Static_Predicate |
+ -- Dynamic_Predicate |
+ -- Pre |
+ -- Pre'Class |
+ -- Post |
+ -- Post'Class |
+ -- Type_Invariant |
+ -- Type_Invariant'Class |
+ -- Default_Initial_Condition
+
+ -- ID_ASSERTION_KIND ::= Assert_And_Cut |
+ -- Assume |
+ -- Contract_Cases |
+ -- Debug |
+ -- Ghost |
+ -- Initial_Condition |
+ -- Loop_Invariant |
+ -- Loop_Variant |
+ -- Postcondition |
+ -- Precondition |
+ -- Predicate |
+ -- Refined_Post |
+ -- Statement_Assertions |
+ -- Subprogram_Variant
-- Note: The RM_ASSERTION_KIND list is language-defined, and the
-- ID_ASSERTION_KIND list contains implementation-defined additions
begin
GNAT_Pragma;
Check_No_Identifiers;
- Check_At_Most_N_Arguments (1);
+ Check_At_Most_N_Arguments (2); -- Accounts for implicit type arg
Typ := Empty;
Stmt := Prev (N);
Set_Has_Own_DIC (Typ);
+ -- A type entity argument is appended to facilitate inheriting the
+ -- aspect/pragma from parent types (see Build_DIC_Procedure_Body),
+ -- though that extra argument isn't documented for the pragma.
+
+ if not Present (Arg2) then
+ -- When the pragma has no arguments, create an argument with
+ -- the value Empty, so the type name argument can be appended
+ -- following it (since it's expected as the second argument).
+
+ if not Present (Arg1) then
+ Set_Pragma_Argument_Associations (N, New_List (
+ Make_Pragma_Argument_Association (Sloc (Typ),
+ Expression => Empty)));
+ end if;
+
+ Append_To
+ (Pragma_Argument_Associations (N),
+ Make_Pragma_Argument_Association (Sloc (Typ),
+ Expression => New_Occurrence_Of (Typ, Sloc (Typ))));
+ end if;
+
-- Chain the pragma on the rep item chain for further processing
Discard := Rep_Item_Too_Late (Typ, N, FOnly => True);
-- The pragma defines a type-specific invariant, the type is said
-- to have invariants of its "own".
- Set_Has_Own_Invariants (Typ);
+ Set_Has_Own_Invariants (Base_Type (Typ));
-- If the invariant is class-wide, then it can be inherited by
-- derived or interface implementing types. The type is said to
-- pragma No_Return (procedure_LOCAL_NAME {, procedure_Local_Name});
- when Pragma_No_Return => No_Return : declare
+ when Pragma_No_Return => Prag_No_Return : declare
+
+ function Check_No_Return
+ (E : Entity_Id;
+ N : Node_Id) return Boolean;
+ -- Check rule 6.5.1(4/3) of the Ada RM. If the rule is violated,
+ -- emit an error message and return False, otherwise return True.
+ -- 6.5.1 Nonreturning procedures:
+ -- 4/3 "Aspect No_Return shall not be specified for a null
+ -- procedure nor an instance of a generic unit."
+
+ ---------------------
+ -- Check_No_Return --
+ ---------------------
+
+ function Check_No_Return
+ (E : Entity_Id;
+ N : Node_Id) return Boolean
+ is
+ begin
+ if Ekind (E) = E_Procedure then
+
+ -- If E is a generic instance, marking it with No_Return
+ -- is forbidden, but having it inherit the No_Return of
+ -- the generic is allowed. We check if E is inheriting its
+ -- No_Return flag from the generic by checking if No_Return
+ -- is already set.
+
+ if Is_Generic_Instance (E) and then not No_Return (E) then
+ Error_Msg_NE
+ ("generic instance & is marked as No_Return", N, E);
+ Error_Msg_NE
+ ("\generic procedure & must be marked No_Return",
+ N,
+ Generic_Parent (Parent (E)));
+ return False;
+
+ elsif Null_Present (Subprogram_Specification (E)) then
+ Error_Msg_NE
+ ("null procedure & cannot be marked No_Return", N, E);
+ return False;
+ end if;
+ end if;
+
+ return True;
+ end Check_No_Return;
+
Arg : Node_Id;
E : Entity_Id;
Found : Boolean;
end if;
end if;
- Set_No_Return (E);
+ if Check_No_Return (E, N) then
+ Set_No_Return (E);
+ end if;
-- A pragma that applies to a Ghost entity becomes Ghost
-- for the purposes of legality checks and removal of
-- Set flag on any alias as well
- if Is_Overloadable (E) and then Present (Alias (E)) then
+ if Is_Overloadable (E)
+ and then Present (Alias (E))
+ and then Check_No_Return (Alias (E), N)
+ then
Set_No_Return (Alias (E));
end if;
if not Found then
if Entity (Id) = Current_Scope
and then From_Aspect_Specification (N)
+ and then Check_No_Return (Entity (Id), N)
then
Set_No_Return (Entity (Id));
Next (Arg);
end loop;
- end No_Return;
+ end Prag_No_Return;
-----------------
-- No_Run_Time --
-- body, not in the spec).
when Pragma_Unimplemented_Unit => Unimplemented_Unit : declare
- Cunitent : constant Entity_Id :=
+ Cunitent : constant Entity_Id :=
Cunit_Entity (Get_Source_Unit (Loc));
- Ent_Kind : constant Entity_Kind := Ekind (Cunitent);
begin
GNAT_Pragma;
Check_Arg_Count (0);
if Operating_Mode = Generate_Code
- or else Ent_Kind = E_Generic_Function
- or else Ent_Kind = E_Generic_Procedure
- or else Ent_Kind = E_Generic_Package
+ or else Is_Generic_Unit (Cunitent)
then
Get_Name_String (Chars (Cunitent));
Set_Casing (Mixed_Case);
Constit, Encapsulating_State (Constit_Id));
end if;
- -- The only other source of legal constituents is the body
- -- state space of the related package.
-
else
- if Present (Body_States) then
- State_Elmt := First_Elmt (Body_States);
- while Present (State_Elmt) loop
+ declare
+ Pack_Id : Entity_Id;
+ Placement : State_Space_Kind;
+ begin
+ -- Find where the constituent lives with respect to the
+ -- state space.
- -- Consume a valid constituent to signal that it has
- -- been encountered.
+ Find_Placement_In_State_Space
+ (Item_Id => Constit_Id,
+ Placement => Placement,
+ Pack_Id => Pack_Id);
- if Node (State_Elmt) = Constit_Id then
- Remove_Elmt (Body_States, State_Elmt);
- Collect_Constituent;
- return;
- end if;
+ -- The constituent is part of the visible state of a
+ -- private child package, but lacks a Part_Of indicator.
- Next_Elmt (State_Elmt);
- end loop;
- end if;
+ if Placement = Visible_State_Space
+ and then Is_Child_Unit (Pack_Id)
+ and then not Is_Generic_Unit (Pack_Id)
+ and then Is_Private_Descendant (Pack_Id)
+ then
+ Error_Msg_Name_1 := Chars (State_Id);
+ SPARK_Msg_NE
+ ("& cannot act as constituent of state %",
+ Constit, Constit_Id);
+ Error_Msg_Sloc :=
+ Sloc (Enclosing_Declaration (Constit_Id));
+ SPARK_Msg_NE
+ ("\missing Part_Of indicator # should specify "
+ & "encapsulator &",
+ Constit, State_Id);
- -- At this point it is known that the constituent is not
- -- part of the package hidden state and cannot be used in
- -- a refinement (SPARK RM 7.2.2(9)).
+ -- The only other source of legal constituents is the
+ -- body state space of the related package.
- Error_Msg_Name_1 := Chars (Spec_Id);
- SPARK_Msg_NE
- ("cannot use & in refinement, constituent is not a hidden "
- & "state of package %", Constit, Constit_Id);
+ else
+ if Present (Body_States) then
+ State_Elmt := First_Elmt (Body_States);
+ while Present (State_Elmt) loop
+
+ -- Consume a valid constituent to signal that it
+ -- has been encountered.
+
+ if Node (State_Elmt) = Constit_Id then
+ Remove_Elmt (Body_States, State_Elmt);
+ Collect_Constituent;
+ return;
+ end if;
+
+ Next_Elmt (State_Elmt);
+ end loop;
+ end if;
+
+ -- At this point it is known that the constituent is
+ -- not part of the package hidden state and cannot be
+ -- used in a refinement (SPARK RM 7.2.2(9)).
+
+ Error_Msg_Name_1 := Chars (Spec_Id);
+ SPARK_Msg_NE
+ ("cannot use & in refinement, constituent is not a "
+ & "hidden state of package %", Constit, Constit_Id);
+ end if;
+ end;
end if;
end Match_Constituent;
-- in the refinement clause.
Report_Unused_Constituents (Part_Of_Constits);
+
+ -- Avoid a cascading error reporting a missing refinement by adding a
+ -- dummy constituent.
+
+ if No (Refinement_Constituents (State_Id)) then
+ Set_Refinement_Constituents (State_Id, New_Elmt_List (Any_Id));
+ end if;
+
+ -- At this point the refinement might be dummy, but must be
+ -- well-formed, to prevent cascaded errors.
+
+ pragma Assert (Has_Null_Refinement (State_Id)
+ xor
+ Has_Non_Null_Refinement (State_Id));
end Analyze_Refinement_Clause;
-----------------------------
Formal := First_Entity (Spec_Id);
while Present (Formal) loop
if Ekind (Formal) in E_In_Out_Parameter | E_In_Parameter then
+
+ -- IN parameters can act as output when the related type is
+ -- access-to-variable.
+
+ if Ekind (Formal) = E_In_Parameter
+ and then Is_Access_Variable (Etype (Formal))
+ then
+ Append_New_Elmt (Formal, Subp_Outputs);
+ end if;
+
Append_New_Elmt (Formal, Subp_Inputs);
end if;
if Ekind (Formal) in E_In_Out_Parameter | E_Out_Parameter then
Append_New_Elmt (Formal, Subp_Outputs);
- -- Out parameters can act as inputs when the related type is
+ -- OUT parameters can act as inputs when the related type is
-- tagged, unconstrained array, unconstrained record, or record
-- with unconstrained components.
Global := Get_Pragma (Subp_Id, Pragma_Refined_Global);
-- Subprogram declaration or stand-alone body case, look for pragmas
- -- Depends and Global
+ -- Depends and Global.
else
Depends := Get_Pragma (Spec_Id, Pragma_Depends);
-- RM defined
Name_Assert
- | Name_Assertion_Policy
| Name_Static_Predicate
| Name_Dynamic_Predicate
| Name_Pre
projects / gcc.git / blobdiff