procedure Check_Declaration (Decl : Node_Id);
+ procedure Check_Declaration_Legality
+ (Decl : Node_Id;
+ Force : Boolean;
+ Legal : in out Boolean);
+ -- Check the legality of declaration Decl regarding rules not related to
+ -- permissions. Update Legal to False if a rule is violated. Issue an
+ -- error message if Force is True and Emit_Messages returns True.
+
procedure Check_Expression (Expr : Node_Id; Mode : Extended_Checking_Mode);
pragma Precondition (Nkind_In (Expr, N_Index_Or_Discriminant_Constraint,
N_Range_Constraint,
procedure Check_Node (N : Node_Id);
-- Main traversal procedure to check safe pointer usage
+ procedure Check_Old_Loop_Entry (N : Node_Id);
+ -- Check SPARK RM 3.10(14) regarding 'Old and 'Loop_Entry
+
procedure Check_Package_Body (Pack : Node_Id);
procedure Check_Package_Spec (Pack : Node_Id);
procedure Check_Statement (Stmt : Node_Id);
- procedure Check_Type (Typ : Entity_Id);
+ procedure Check_Type_Legality
+ (Typ : Entity_Id;
+ Force : Boolean;
+ Legal : in out Boolean);
-- Check that type Typ is either not deep, or that it is an observing or
-- owning type according to SPARK RM 3.10
Expr_Root : Entity_Id;
Perm : Perm_Kind;
Status : Error_Status;
+ Dummy : Boolean := True;
-- Start of processing for Check_Assignment
begin
- Check_Type (Target_Typ);
+ Check_Type_Legality (Target_Typ, Force => True, Legal => Dummy);
if Is_Anonymous_Access_Type (Target_Typ) then
Check_Source_Of_Borrow_Or_Observe (Expr, Status);
Expr_Root := Get_Root_Object (Expr);
- -- SPARK RM 3.10(8): For an assignment statement where
- -- the target is a stand-alone object of an anonymous
- -- access-to-object type
+ -- SPARK RM 3.10(7): For an assignment statement where the target is
+ -- a stand-alone object of an anonymous access-to-object type.
pragma Assert (Present (Target_Root));
- -- If the type of the target is an anonymous
- -- access-to-constant type (an observing access type), the
- -- source shall be an owning access object denoted by a name
- -- that is not in the Moved state, and whose root object
- -- is not in the Moved state and is not declared at a
- -- statically deeper accessibility level than that of
- -- the target object.
+ -- If the type of the target is an anonymous access-to-constant type
+ -- (an observing access type), the source shall be an owning access
+ -- object denoted by a name that is not in the Moved state, and whose
+ -- root object is not in the Moved state and is not declared at a
+ -- statically deeper accessibility level than that of the target
+ -- object.
if Is_Access_Constant (Target_Typ) then
Perm := Get_Perm (Expr);
-- ??? check accessibility level
- -- If the type of the target is an anonymous
- -- access-to-variable type (an owning access type), the
- -- source shall be an owning access object denoted by a
- -- name that is in the Unrestricted state, and whose root
- -- object is the target object itself.
+ -- If the type of the target is an anonymous access-to-variable
+ -- type (an owning access type), the source shall be an owning
+ -- access object denoted by a name that is in the Unrestricted
+ -- state, and whose root object is the target object itself.
Check_Expression (Expr, Observe);
Handle_Observe (Target_Root, Expr, Is_Decl);
Target : constant Entity_Id := Defining_Identifier (Decl);
Target_Typ : constant Node_Id := Etype (Target);
Expr : Node_Id;
+ Dummy : Boolean := True;
begin
+ -- Start with legality rules not related to permissions
+
+ Check_Declaration_Legality (Decl, Force => True, Legal => Dummy);
+
+ -- Now check permission-related legality rules
+
case N_Declaration'(Nkind (Decl)) is
when N_Full_Type_Declaration =>
- Check_Type (Target);
+ null;
-- ??? What about component declarations with defaults.
when N_Object_Declaration =>
Expr := Expression (Decl);
- Check_Type (Target_Typ);
+ if Present (Expr) then
+ Check_Assignment (Target => Target,
+ Expr => Expr);
+ end if;
+
+ if Is_Deep (Target_Typ) then
+ declare
+ Tree : constant Perm_Tree_Access :=
+ new Perm_Tree_Wrapper'
+ (Tree =>
+ (Kind => Entire_Object,
+ Is_Node_Deep => True,
+ Explanation => Decl,
+ Permission => Read_Write,
+ Children_Permission => Read_Write));
+ begin
+ Set (Current_Perm_Env, Target, Tree);
+ end;
+ end if;
+
+ when N_Iterator_Specification =>
+ null;
+
+ when N_Loop_Parameter_Specification =>
+ null;
+
+ -- Checking should not be called directly on these nodes
+
+ when N_Function_Specification
+ | N_Entry_Declaration
+ | N_Procedure_Specification
+ | N_Component_Declaration
+ =>
+ raise Program_Error;
+
+ -- Ignored constructs for pointer checking
+
+ when N_Formal_Object_Declaration
+ | N_Formal_Type_Declaration
+ | N_Incomplete_Type_Declaration
+ | N_Private_Extension_Declaration
+ | N_Private_Type_Declaration
+ | N_Protected_Type_Declaration
+ =>
+ null;
+
+ -- The following nodes are rewritten by semantic analysis
+
+ when N_Expression_Function =>
+ raise Program_Error;
+ end case;
+ end Check_Declaration;
+
+ --------------------------------
+ -- Check_Declaration_Legality --
+ --------------------------------
+
+ procedure Check_Declaration_Legality
+ (Decl : Node_Id;
+ Force : Boolean;
+ Legal : in out Boolean)
+ is
+ function Original_Emit_Messages return Boolean renames Emit_Messages;
+
+ function Emit_Messages return Boolean;
+ -- Local wrapper around generic formal parameter Emit_Messages, to
+ -- check the value of parameter Force before calling the original
+ -- Emit_Messages, and setting Legal to False.
+
+ -------------------
+ -- Emit_Messages --
+ -------------------
+
+ function Emit_Messages return Boolean is
+ begin
+ Legal := False;
+ return Force and then Original_Emit_Messages;
+ end Emit_Messages;
+
+ -- Local variables
+
+ Target : constant Entity_Id := Defining_Identifier (Decl);
+ Target_Typ : constant Node_Id := Etype (Target);
+ Expr : Node_Id;
+
+ -- Start of processing for Check_Declaration_Legality
+
+ begin
+ case N_Declaration'(Nkind (Decl)) is
+ when N_Full_Type_Declaration =>
+ Check_Type_Legality (Target, Force, Legal);
+
+ when N_Subtype_Declaration =>
+ null;
+
+ when N_Object_Declaration =>
+ Expr := Expression (Decl);
+
+ Check_Type_Legality (Target_Typ, Force, Legal);
-- A declaration of a stand-alone object of an anonymous access
-- type shall have an explicit initial value and shall occur
end if;
end if;
- if Present (Expr) then
- Check_Assignment (Target => Target,
- Expr => Expr);
- end if;
-
- if Is_Deep (Target_Typ) then
- declare
- Tree : constant Perm_Tree_Access :=
- new Perm_Tree_Wrapper'
- (Tree =>
- (Kind => Entire_Object,
- Is_Node_Deep => True,
- Explanation => Decl,
- Permission => Read_Write,
- Children_Permission => Read_Write));
- begin
- Set (Current_Perm_Env, Target, Tree);
- end;
- end if;
-
when N_Iterator_Specification =>
null;
when N_Expression_Function =>
raise Program_Error;
end case;
- end Check_Declaration;
+ end Check_Declaration_Legality;
----------------------
-- Check_Expression --
----------------
procedure Check_Node (N : Node_Id) is
+
+ procedure Check_Subprogram_Contract (N : Node_Id);
+ -- Check the postcondition-like contracts for use of 'Old
+
+ -------------------------------
+ -- Check_Subprogram_Contract --
+ -------------------------------
+
+ procedure Check_Subprogram_Contract (N : Node_Id) is
+ begin
+ if Nkind (N) = N_Subprogram_Declaration
+ or else Acts_As_Spec (N)
+ then
+ declare
+ E : constant Entity_Id := Unique_Defining_Entity (N);
+ Post : constant Node_Id :=
+ Get_Pragma (E, Pragma_Postcondition);
+ Cases : constant Node_Id :=
+ Get_Pragma (E, Pragma_Contract_Cases);
+ begin
+ Check_Old_Loop_Entry (Post);
+ Check_Old_Loop_Entry (Cases);
+ end;
+
+ elsif Nkind (N) = N_Subprogram_Body then
+ declare
+ E : constant Entity_Id := Defining_Entity (N);
+ Ref_Post : constant Node_Id :=
+ Get_Pragma (E, Pragma_Refined_Post);
+ begin
+ Check_Old_Loop_Entry (Ref_Post);
+ end;
+ end if;
+ end Check_Subprogram_Contract;
+
+ -- Start of processing for Check_Node
+
begin
case Nkind (N) is
when N_Declaration =>
Check_Package_Body (N);
end if;
- when N_Subprogram_Body
- | N_Entry_Body
- | N_Task_Body
- =>
+ when N_Subprogram_Body =>
if not Is_Generic_Unit (Unique_Defining_Entity (N)) then
+ Check_Subprogram_Contract (N);
Check_Callable_Body (N);
end if;
+ when N_Entry_Body
+ | N_Task_Body
+ =>
+ Check_Callable_Body (N);
+
when N_Protected_Body =>
Check_List (Declarations (N));
when N_Pragma =>
Check_Pragma (N);
+ when N_Subprogram_Declaration =>
+ Check_Subprogram_Contract (N);
+
+ -- Attribute references in statement position are not supported in
+ -- SPARK and will be rejected by GNATprove.
+
+ when N_Attribute_Reference =>
+ null;
+
-- Ignored constructs for pointer checking
when N_Abstract_Subprogram_Declaration
| N_Procedure_Instantiation
| N_Raise_xxx_Error
| N_Record_Representation_Clause
- | N_Subprogram_Declaration
| N_Subprogram_Renaming_Declaration
| N_Task_Type_Declaration
| N_Use_Package_Clause
end case;
end Check_Node;
+ --------------------------
+ -- Check_Old_Loop_Entry --
+ --------------------------
+
+ procedure Check_Old_Loop_Entry (N : Node_Id) is
+
+ function Check_Attribute (N : Node_Id) return Traverse_Result;
+
+ ---------------------
+ -- Check_Attribute --
+ ---------------------
+
+ function Check_Attribute (N : Node_Id) return Traverse_Result is
+ Attr_Id : Attribute_Id;
+ Aname : Name_Id;
+ Pref : Node_Id;
+
+ begin
+ if Nkind (N) = N_Attribute_Reference then
+ Attr_Id := Get_Attribute_Id (Attribute_Name (N));
+ Aname := Attribute_Name (N);
+
+ if Attr_Id = Attribute_Old
+ or else Attr_Id = Attribute_Loop_Entry
+ then
+ Pref := Prefix (N);
+
+ if Is_Deep (Etype (Pref)) then
+ if Nkind (Pref) /= N_Function_Call then
+ if Emit_Messages then
+ Error_Msg_Name_1 := Aname;
+ Error_Msg_N
+ ("prefix of % attribute must be a function call "
+ & "(SPARK RM 3.10(14))", Pref);
+ end if;
+
+ elsif Is_Traversal_Function_Call (Pref) then
+ if Emit_Messages then
+ Error_Msg_Name_1 := Aname;
+ Error_Msg_N
+ ("prefix of % attribute should not call a traversal "
+ & "function (SPARK RM 3.10(14))", Pref);
+ end if;
+ end if;
+ end if;
+ end if;
+ end if;
+
+ return OK;
+ end Check_Attribute;
+
+ procedure Check_All is new Traverse_Proc (Check_Attribute);
+
+ -- Start of processing for Check_Old_Loop_Entry
+
+ begin
+ Check_All (N);
+ end Check_Old_Loop_Entry;
+
------------------------
-- Check_Package_Body --
------------------------
Expr : constant Node_Id := Expression (Arg2);
begin
Check_Expression (Expr, Read);
+
+ -- Prefix of Loop_Entry should be checked inside any assertion
+ -- where it may appear.
+
+ Check_Old_Loop_Entry (Expr);
end;
+ -- Prefix of Loop_Entry should be checked inside a Loop_Variant
+
+ when Pragma_Loop_Variant =>
+ Check_Old_Loop_Entry (Prag);
+
-- There is no need to check contracts, as these can only access
-- inputs and outputs of the subprogram. Inputs are checked
-- independently for R permission. Outputs are checked
when N_Package_Body
| N_Package_Declaration
+ | N_Subprogram_Declaration
| N_Subprogram_Body
=>
declare
end case;
end Check_Statement;
- ----------------
- -- Check_Type --
- ----------------
+ -------------------------
+ -- Check_Type_Legality --
+ -------------------------
+
+ procedure Check_Type_Legality
+ (Typ : Entity_Id;
+ Force : Boolean;
+ Legal : in out Boolean)
+ is
+ function Original_Emit_Messages return Boolean renames Emit_Messages;
+
+ function Emit_Messages return Boolean;
+ -- Local wrapper around generic formal parameter Emit_Messages, to
+ -- check the value of parameter Force before calling the original
+ -- Emit_Messages, and setting Legal to False.
+
+ -------------------
+ -- Emit_Messages --
+ -------------------
+
+ function Emit_Messages return Boolean is
+ begin
+ Legal := False;
+ return Force and then Original_Emit_Messages;
+ end Emit_Messages;
+
+ -- Local variables
- procedure Check_Type (Typ : Entity_Id) is
Check_Typ : constant Entity_Id := Retysp (Typ);
+ -- Start of processing for Check_Type_Legality
+
begin
case Type_Kind'(Ekind (Check_Typ)) is
when Access_Kind =>
=>
null;
when E_Access_Subtype =>
- Check_Type (Base_Type (Check_Typ));
+ Check_Type_Legality (Base_Type (Check_Typ), Force, Legal);
when E_Access_Attribute_Type =>
if Emit_Messages then
Error_Msg_N ("access attribute not allowed in SPARK",
when E_Array_Type
| E_Array_Subtype
=>
- Check_Type (Component_Type (Check_Typ));
+ Check_Type_Legality (Component_Type (Check_Typ), Force, Legal);
when Record_Kind =>
if Is_Deep (Check_Typ)
-- Ignore components which are not visible in SPARK
if Component_Is_Visible_In_SPARK (Comp) then
- Check_Type (Etype (Comp));
+ Check_Type_Legality (Etype (Comp), Force, Legal);
end if;
Next_Component_Or_Discriminant (Comp);
end loop;
=>
null;
end case;
- end Check_Type;
+ end Check_Type_Legality;
--------------
-- Get_Expl --
end case;
end Is_Deep;
+ --------------
+ -- Is_Legal --
+ --------------
+
+ function Is_Legal (N : Node_Id) return Boolean is
+ Legal : Boolean := True;
+
+ begin
+ case Nkind (N) is
+ when N_Declaration =>
+ Check_Declaration_Legality (N, Force => False, Legal => Legal);
+ when others =>
+ null;
+ end case;
+
+ return Legal;
+ end Is_Legal;
+
----------------------
-- Is_Local_Context --
----------------------
is
begin
return Is_Path_Expression (Expr, Is_Traversal)
+
+ or else (Nkind_In (Expr, N_Qualified_Expression,
+ N_Type_Conversion,
+ N_Unchecked_Type_Conversion)
+ and then Is_Subpath_Expression (Expression (Expr)))
+
or else (Nkind (Expr) = N_Attribute_Reference
and then
(Get_Attribute_Id (Attribute_Name (Expr)) =
or else
Get_Attribute_Id (Attribute_Name (Expr)) =
Attribute_Image))
- or else Nkind (Expr) = N_Op_Concat;
+
+ or else Nkind (Expr) = N_Op_Concat;
end Is_Subpath_Expression;
---------------------------
Get_First_Key (Current_Borrowers);
Var : Entity_Id;
Borrowed : Node_Id;
+ B_Pledge : Entity_Id := Empty;
begin
+ -- Search for a call to a pledge function or a global pragma in
+ -- the parents of Expr.
+
+ declare
+ Call : Node_Id := Expr;
+ begin
+ while Present (Call)
+ and then
+ (Nkind (Call) /= N_Function_Call
+ or else not Is_Pledge_Function (Get_Called_Entity (Call)))
+ loop
+ -- Do not check for borrowed objects in global contracts
+ -- ??? However we should keep these objects in the borrowed
+ -- state when verifying the subprogram so that we can make
+ -- sure that they are only read inside pledges.
+ -- ??? There is probably a better way to disable checking of
+ -- borrows inside global contracts.
+
+ if Nkind (Call) = N_Pragma
+ and then Get_Pragma_Id (Pragma_Name (Call)) = Pragma_Global
+ then
+ return;
+ end if;
+
+ Call := Parent (Call);
+ end loop;
+
+ if Present (Call)
+ and then Nkind (First_Actual (Call)) in N_Has_Entity
+ then
+ B_Pledge := Entity (First_Actual (Call));
+ end if;
+ end;
+
while Key.Present loop
Var := Key.K;
Borrowed := Get (Current_Borrowers, Var);
if Is_Prefix_Or_Almost (Pref => Borrowed, Expr => Expr)
+ and then Var /= B_Pledge
and then Emit_Messages
then
Error_Msg_Sloc := Sloc (Borrowed);
projects / thirdparty / gcc.git / blobdiff