diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index 472a6fdcd2df2837a724ecc6fb2eeb0fd3df4049..95c898b3768d0163ec73cd776df841294f936a6e 100644
--- a/gcc/ada/ChangeLog
+++ b/gcc/ada/ChangeLog
@@ -1,3 +1,38 @@
+2019-07-11 Claire Dross <dross@adacore.com>
+
+ * gnat1drv.adb: SPARK checking rules for pointer aliasing are
+ moved to GNATprove backend.
+ * sem_spark.ads, sem_spark.adb (Sem_SPARK): Is now a generic
+ unit. Takes as parameters:
+ - Retysp which is used to query the most underlying type
+ visible in SPARK. We do not introduce aliasing checks for
+ types which are not visibly deep.
+ - Component_Is_Visible_In_SPARK is used to avoid doing pointer
+ aliasing checks on components which are not visible in SPARK.
+ - Emit_Messages returns True in the second phase of SPARK
+ analysis. Error messages for failed aliasing checks are only
+ output in this case.
+ Additionally, errors on constructs not supported in SPARK are
+ removed as duplicates of marking errors. Components are stored
+ in the permission map using their original component to avoid
+ inconsistencies between components of different views of the
+ same type.
+ (Check_Expression): Handle delta constraints.
+ (Is_Deep): Exported so that we can check for SPARK restrictions
+ on deep types inside SPARK semantic checkings.
+ (Is_Traversal_Function): Exported so that we can check for SPARK
+ restrictions on traversal functions inside SPARK semantic
+ checkings.
+ (Check_Call_Statement, Read_Indexes): Check wether we are
+ dealing with a subprogram pointer type before querying called
+ entity.
+ (Is_Subpath_Expression): Image attribute can appear inside a
+ path.
+ (Check_Loop_Statement): Correct order of statements in the loop.
+ (Check_Node): Ignore raise nodes.
+ (Check_Statement): Use Last_Non_Pragma to get the object
+ declaration in an extended return statement.
+
2019-07-11 Patrick Bernardi <bernardi@adacore.com>
* bindgen.adb (Gen_Main): Do not generate a reference to
diff --git a/gcc/ada/gnat1drv.adb b/gcc/ada/gnat1drv.adb
index 55a57ddc7e8c641f35a5611ceeb335fa518feaea..ecb3ccdd39917639f32a6e632f1d0d773f9381d4 100644
--- a/gcc/ada/gnat1drv.adb
+++ b/gcc/ada/gnat1drv.adb
@@ -63,7 +63,6 @@ with Sem_Ch13;
with Sem_Elim;
with Sem_Eval;
with Sem_Prag;
-with Sem_SPARK; use Sem_SPARK;
with Sem_Type;
with Set_Targ;
with Sinfo; use Sinfo;
@@ -1586,13 +1585,6 @@ begin
if GNATprove_Mode then
- -- Perform the new SPARK checking rules for pointer aliasing. This is
- -- only activated in GNATprove mode and on SPARK code.
-
- if Debug_Flag_FF then
- Check_Safe_Pointers (Main_Unit_Node);
- end if;
-
-- In GNATprove mode we're writing the ALI much earlier than usual
-- as flow analysis needs the file present in order to append its
-- own globals to it.
diff --git a/gcc/ada/sem_spark.adb b/gcc/ada/sem_spark.adb
index 10c82fffc73cd703833b742ef0ee6f1759b19cea..67aa4537c1d4dbe77355e4080ee7598e138cfaa5 100644
--- a/gcc/ada/sem_spark.adb
+++ b/gcc/ada/sem_spark.adb
@@ -641,7 +641,8 @@ package body Sem_SPARK is
pragma Precondition (Nkind_In (Expr, N_Index_Or_Discriminant_Constraint,
N_Range_Constraint,
N_Subtype_Indication,
- N_Digits_Constraint)
+ N_Digits_Constraint,
+ N_Delta_Constraint)
or else Nkind (Expr) in N_Subexpr);
procedure Check_Globals (Subp : Entity_Id);
@@ -744,10 +745,6 @@ package body Sem_SPARK is
-- A procedure that is called when deep globals or aliased globals are used
-- without any global aspect.
- function Is_Deep (Typ : Entity_Id) return Boolean;
- -- A function that can tell if a type is deep or not. Returns true if the
- -- type passed as argument is deep.
-
function Is_Path_Expression (Expr : Node_Id) return Boolean;
-- Return whether Expr corresponds to a path
@@ -759,8 +756,6 @@ package body Sem_SPARK is
-- a prefix, in the sense that they could still refer to overlapping memory
-- locations.
- function Is_Traversal_Function (E : Entity_Id) return Boolean;
-
function Is_Traversal_Function_Call (Expr : Node_Id) return Boolean;
function Loop_Of_Exit (N : Node_Id) return Entity_Id;
@@ -959,7 +954,7 @@ package body Sem_SPARK is
null;
else
Handle_Parameter_Or_Global (Expr => Item,
- Formal_Typ => Etype (Item),
+ Formal_Typ => Retysp (Etype (Item)),
Param_Mode => Kind,
Subp => Subp,
Global_Var => True);
@@ -1076,9 +1071,12 @@ package body Sem_SPARK is
and then (Is_Traversal_Function_Call (Expr)
or else Get_Root_Object (Borrowed) /= Var)
then
- Error_Msg_NE
- ("source of assignment must have & as root (SPARK RM 3.10(8)))",
- Expr, Var);
+ if Emit_Messages then
+ Error_Msg_NE
+ ("source of assignment must have & as root" &
+ " (SPARK RM 3.10(8)))",
+ Expr, Var);
+ end if;
return;
end if;
@@ -1105,9 +1103,12 @@ package body Sem_SPARK is
and then (Is_Traversal_Function_Call (Expr)
or else Get_Root_Object (Observed) /= Var)
then
- Error_Msg_NE
- ("source of assignment must have & as root (SPARK RM 3.10(8)))",
- Expr, Var);
+ if Emit_Messages then
+ Error_Msg_NE
+ ("source of assignment must have & as root" &
+ " (SPARK RM 3.10(8)))",
+ Expr, Var);
+ end if;
return;
end if;
@@ -1197,15 +1198,19 @@ package body Sem_SPARK is
if not Is_Decl then
if not Is_Entity_Name (Target) then
- Error_Msg_N
- ("target of borrow must be stand-alone variable",
- Target);
+ if Emit_Messages then
+ Error_Msg_N
+ ("target of borrow must be stand-alone variable",
+ Target);
+ end if;
return;
elsif Target_Root /= Expr_Root then
- Error_Msg_NE
- ("source of borrow must be variable &",
- Expr, Target);
+ if Emit_Messages then
+ Error_Msg_NE
+ ("source of borrow must be variable &",
+ Expr, Target);
+ end if;
return;
end if;
end if;
@@ -1220,7 +1225,9 @@ package body Sem_SPARK is
Check_Expression (Expr, Move);
else
- Error_Msg_N ("expression not allowed as source of move", Expr);
+ if Emit_Messages then
+ Error_Msg_N ("expression not allowed as source of move", Expr);
+ end if;
return;
end if;
@@ -1253,7 +1260,7 @@ package body Sem_SPARK is
begin
Check_Parameter_Or_Global
(Expr => Actual,
- Typ => Underlying_Type (Etype (Formal)),
+ Typ => Retysp (Etype (Formal)),
Kind => Ekind (Formal),
Subp => Subp,
Global_Var => False);
@@ -1287,7 +1294,15 @@ package body Sem_SPARK is
begin
Inside_Procedure_Call := True;
Check_Params (Call);
- Check_Globals (Get_Called_Entity (Call));
+ if Ekind (Get_Called_Entity (Call)) = E_Subprogram_Type then
+ if Emit_Messages then
+ Error_Msg_N
+ ("call through access to subprogram is not allowed in SPARK",
+ Call);
+ end if;
+ else
+ Check_Globals (Get_Called_Entity (Call));
+ end if;
Inside_Procedure_Call := False;
Update_Params (Call);
@@ -1322,8 +1337,10 @@ package body Sem_SPARK is
and then Is_Anonymous_Access_Type (Etype (Spec_Id))
and then not Is_Traversal_Function (Spec_Id)
then
- Error_Msg_N ("anonymous access type for result only allowed for "
- & "traveral functions", Spec_Id);
+ if Emit_Messages then
+ Error_Msg_N ("anonymous access type for result only allowed for "
+ & "traversal functions", Spec_Id);
+ end if;
return;
end if;
@@ -1585,7 +1602,10 @@ package body Sem_SPARK is
begin
if not Is_Subpath_Expression (Expr) then
- Error_Msg_N ("name expected here for move/borrow/observe", Expr);
+ if Emit_Messages then
+ Error_Msg_N
+ ("name expected here for move/borrow/observe", Expr);
+ end if;
return;
end if;
@@ -1617,7 +1637,15 @@ package body Sem_SPARK is
when N_Function_Call =>
Read_Params (Expr);
- Check_Globals (Get_Called_Entity (Expr));
+ if Ekind (Get_Called_Entity (Expr)) = E_Subprogram_Type then
+ if Emit_Messages then
+ Error_Msg_N
+ ("call through access to subprogram is not allowed in "
+ & "SPARK", Expr);
+ end if;
+ else
+ Check_Globals (Get_Called_Entity (Expr));
+ end if;
when N_Op_Concat =>
Read_Expression (Left_Opnd (Expr));
@@ -1664,9 +1692,10 @@ package body Sem_SPARK is
-- There can be only one element for a value of deep type
-- in order to avoid aliasing.
- if not (Box_Present (Assoc))
+ if not Box_Present (Assoc)
and then Is_Deep (Etype (Expression (Assoc)))
and then not Is_Singleton_Choice (CL)
+ and then Emit_Messages
then
Error_Msg_F
("singleton choice required to prevent aliasing",
@@ -1725,11 +1754,16 @@ package body Sem_SPARK is
(Get_Attribute_Id (Attribute_Name (Expr)) =
Attribute_Loop_Entry
or else
- Get_Attribute_Id (Attribute_Name (Expr)) = Attribute_Update);
+ Get_Attribute_Id (Attribute_Name (Expr)) = Attribute_Update
+ or else
+ Get_Attribute_Id (Attribute_Name (Expr)) = Attribute_Image);
Read_Expression (Prefix (Expr));
if Get_Attribute_Id (Attribute_Name (Expr)) = Attribute_Update
+ or else (Get_Attribute_Id (Attribute_Name (Expr)) =
+ Attribute_Image
+ and then Is_Type_Name (Prefix (Expr)))
then
Read_Expression_List (Expressions (Expr));
end if;
@@ -1761,7 +1795,9 @@ package body Sem_SPARK is
-- Read mode.
if Mode /= Read then
- Error_Msg_N ("name expected here for move/borrow/observe", Expr);
+ if Emit_Messages then
+ Error_Msg_N ("name expected here for move/borrow/observe", Expr);
+ end if;
return;
end if;
@@ -1804,6 +1840,13 @@ package body Sem_SPARK is
end if;
return;
+ when N_Delta_Constraint =>
+ Read_Expression (Delta_Expression (Expr));
+ if Present (Range_Constraint (Expr)) then
+ Read_Expression (Range_Constraint (Expr));
+ end if;
+ return;
+
when others =>
null;
end case;
@@ -1934,8 +1977,7 @@ package body Sem_SPARK is
raise Program_Error;
when others =>
- Error_Msg_Name_1 := Aname;
- Error_Msg_N ("attribute % not allowed in SPARK", Expr);
+ null;
end case;
end;
@@ -1999,7 +2041,7 @@ package body Sem_SPARK is
when N_Delta_Aggregate
| N_Target_Name
=>
- Error_Msg_N ("unsupported construct in SPARK", Expr);
+ null;
-- Procedure calls are handled in Check_Node
@@ -2330,16 +2372,16 @@ package body Sem_SPARK is
KeyO := Perm_Tree_Maps.Get_First_Key
(Component (Orig_Tree));
while KeyO.Present loop
+ CompN := Perm_Tree_Maps.Get
+ (Component (New_Tree), KeyO.K);
+ CompO := Perm_Tree_Maps.Get
+ (Component (Orig_Tree), KeyO.K);
pragma Assert (CompO /= null);
Check_Is_Less_Restrictive_Tree (CompN, CompO, E);
KeyO := Perm_Tree_Maps.Get_Next_Key
(Component (Orig_Tree));
- CompN := Perm_Tree_Maps.Get
- (Component (New_Tree), KeyO.K);
- CompO := Perm_Tree_Maps.Get
- (Component (Orig_Tree), KeyO.K);
end loop;
end;
@@ -2362,12 +2404,15 @@ package body Sem_SPARK is
Expl : Node_Id)
is
begin
- Error_Msg_Node_2 := Loop_Id;
- Error_Msg_N ("insufficient permission for & when exiting loop &", E);
- Perm_Mismatch (Exp_Perm => Perm,
- Act_Perm => Found_Perm,
- N => Loop_Id,
- Expl => Expl);
+ if Emit_Messages then
+ Error_Msg_Node_2 := Loop_Id;
+ Error_Msg_N
+ ("insufficient permission for & when exiting loop &", E);
+ Perm_Mismatch (Exp_Perm => Perm,
+ Act_Perm => Found_Perm,
+ N => Loop_Id,
+ Expl => Expl);
+ end if;
end Perm_Error_Loop_Exit;
-- Local variables
@@ -2543,6 +2588,7 @@ package body Sem_SPARK is
| N_Package_Instantiation
| N_Package_Renaming_Declaration
| N_Procedure_Instantiation
+ | N_Raise_xxx_Error
| N_Record_Representation_Clause
| N_Subprogram_Declaration
| N_Subprogram_Renaming_Declaration
@@ -2745,7 +2791,7 @@ package body Sem_SPARK is
Prag_Id : constant Pragma_Id := Get_Pragma_Id (Prag);
Arg1 : constant Node_Id :=
First (Pragma_Argument_Associations (Prag));
- Arg2 : Node_Id;
+ Arg2 : Node_Id := Empty;
begin
if Present (Arg1) then
@@ -2903,17 +2949,20 @@ package body Sem_SPARK is
-- function.
if No (Root) then
- if Nkind (Expr) = N_Function_Call then
- Error_Msg_N
- ("incorrect borrow or observe (SPARK RM 3.10(3))", Expr);
- Error_Msg_N
- ("\function called must be a traversal function", Expr);
- else
- Error_Msg_N
- ("incorrect borrow or observe (SPARK RM 3.10(3))", Expr);
- Error_Msg_N
- ("\expression must be part of stand-alone object or parameter",
- Expr);
+ if Emit_Messages then
+ if Nkind (Expr) = N_Function_Call then
+ Error_Msg_N
+ ("incorrect borrow or observe (SPARK RM 3.10(3))", Expr);
+ Error_Msg_N
+ ("\function called must be a traversal function", Expr);
+ else
+ Error_Msg_N
+ ("incorrect borrow or observe (SPARK RM 3.10(3))", Expr);
+ Error_Msg_N
+ ("\expression must be part of stand-alone object or " &
+ "parameter",
+ Expr);
+ end if;
end if;
Status := Error;
@@ -2958,7 +3007,9 @@ package body Sem_SPARK is
if No (Get_Root_Object
(Target, Through_Traversal => False))
then
- Error_Msg_N ("illegal target for assignment", Target);
+ if Emit_Messages then
+ Error_Msg_N ("illegal target for assignment", Target);
+ end if;
return;
end if;
@@ -3064,7 +3115,7 @@ package body Sem_SPARK is
if Is_Anonymous_Access_Type (Return_Typ) then
pragma Assert (Is_Traversal_Function (Subp));
- if Nkind (Expr) /= N_Null then
+ if Nkind (Expr) /= N_Null and then Emit_Messages then
declare
Expr_Root : constant Entity_Id :=
Get_Root_Object (Expr);
@@ -3089,9 +3140,11 @@ package body Sem_SPARK is
Check_Expression (Expr, Move);
else
- Error_Msg_N
- ("expression not allowed as source of move",
- Expr);
+ if Emit_Messages then
+ Error_Msg_N
+ ("expression not allowed as source of move",
+ Expr);
+ end if;
return;
end if;
@@ -3114,14 +3167,14 @@ package body Sem_SPARK is
Subp : constant Entity_Id :=
Return_Applies_To (Return_Statement_Entity (Stmt));
Decls : constant List_Id := Return_Object_Declarations (Stmt);
- Decl : constant Node_Id := Last (Decls);
+ Decl : constant Node_Id := Last_Non_Pragma (Decls);
Obj : constant Entity_Id := Defining_Identifier (Decl);
Perm : Perm_Kind;
begin
-- SPARK RM 3.10(5): return statement of traversal function
- if Is_Traversal_Function (Subp) then
+ if Is_Traversal_Function (Subp) and then Emit_Messages then
Error_Msg_N
("extended return cannot apply to a traversal function",
Stmt);
@@ -3254,7 +3307,7 @@ package body Sem_SPARK is
| N_Selective_Accept
| N_Timed_Entry_Call
=>
- Error_Msg_N ("unsupported construct in SPARK", Stmt);
+ null;
-- The following nodes are never generated in GNATprove mode
@@ -3270,12 +3323,12 @@ package body Sem_SPARK is
----------------
procedure Check_Type (Typ : Entity_Id) is
- Check_Typ : constant Entity_Id := Underlying_Type (Typ);
+ Check_Typ : constant Entity_Id := Retysp (Typ);
begin
case Type_Kind'(Ekind (Check_Typ)) is
when Access_Kind =>
- case Access_Kind'(Ekind (Underlying_Type (Check_Typ))) is
+ case Access_Kind'(Ekind (Check_Typ)) is
when E_Access_Type
| E_Anonymous_Access_Type
=>
@@ -3283,18 +3336,26 @@ package body Sem_SPARK is
when E_Access_Subtype =>
Check_Type (Base_Type (Check_Typ));
when E_Access_Attribute_Type =>
- Error_Msg_N ("access attribute not allowed in SPARK",
- Check_Typ);
+ if Emit_Messages then
+ Error_Msg_N ("access attribute not allowed in SPARK",
+ Check_Typ);
+ end if;
when E_Allocator_Type =>
- Error_Msg_N ("missing type resolution", Check_Typ);
+ if Emit_Messages then
+ Error_Msg_N ("missing type resolution", Check_Typ);
+ end if;
when E_General_Access_Type =>
- Error_Msg_NE
- ("general access type & not allowed in SPARK",
- Check_Typ, Check_Typ);
+ if Emit_Messages then
+ Error_Msg_NE
+ ("general access type & not allowed in SPARK",
+ Check_Typ, Check_Typ);
+ end if;
when Access_Subprogram_Kind =>
- Error_Msg_NE
- ("access to subprogram type & not allowed in SPARK",
- Check_Typ, Check_Typ);
+ if Emit_Messages then
+ Error_Msg_NE
+ ("access to subprogram type & not allowed in SPARK",
+ Check_Typ, Check_Typ);
+ end if;
end case;
when E_Array_Type
@@ -3307,9 +3368,11 @@ package body Sem_SPARK is
and then (Is_Tagged_Type (Check_Typ)
or else Is_Class_Wide_Type (Check_Typ))
then
- Error_Msg_NE
- ("tagged type & cannot be owning in SPARK",
- Check_Typ, Check_Typ);
+ if Emit_Messages then
+ Error_Msg_NE
+ ("tagged type & cannot be owning in SPARK",
+ Check_Typ, Check_Typ);
+ end if;
else
declare
@@ -3317,7 +3380,12 @@ package body Sem_SPARK is
begin
Comp := First_Component_Or_Discriminant (Check_Typ);
while Present (Comp) loop
- Check_Type (Etype (Comp));
+
+ -- Ignore components which are not visible in SPARK
+
+ if Component_Is_Visible_In_SPARK (Comp) then
+ Check_Type (Etype (Comp));
+ end if;
Next_Component_Or_Discriminant (Comp);
end loop;
end;
@@ -3333,14 +3401,14 @@ package body Sem_SPARK is
=>
null;
- -- The following should not arise as underlying types
+ -- Do not check type whose full view is not SPARK
when E_Private_Type
| E_Private_Subtype
| E_Limited_Private_Type
| E_Limited_Private_Subtype
=>
- raise Program_Error;
+ null;
end case;
end Check_Type;
@@ -3526,7 +3594,8 @@ package body Sem_SPARK is
pragma Assert (Nkind (N) = N_Selected_Component);
declare
Comp : constant Entity_Id :=
- Entity (Selector_Name (N));
+ Original_Record_Component
+ (Entity (Selector_Name (N)));
D : constant Perm_Tree_Access :=
Perm_Tree_Maps.Get
(Component (C.Tree_Access), Comp);
@@ -3577,7 +3646,9 @@ package body Sem_SPARK is
is
begin
if not Is_Subpath_Expression (Expr) then
- Error_Msg_N ("name expected here for path", Expr);
+ if Emit_Messages then
+ Error_Msg_N ("name expected here for path", Expr);
+ end if;
return Empty;
end if;
@@ -3630,7 +3701,9 @@ package body Sem_SPARK is
Attribute_Loop_Entry
or else
Get_Attribute_Id (Attribute_Name (Expr)) =
- Attribute_Update);
+ Attribute_Update
+ or else Get_Attribute_Id (Attribute_Name (Expr)) =
+ Attribute_Image);
return Empty;
when others =>
@@ -3750,22 +3823,27 @@ package body Sem_SPARK is
function Is_Deep (Typ : Entity_Id) return Boolean is
begin
- case Type_Kind'(Ekind (Underlying_Type (Typ))) is
+ case Type_Kind'(Ekind (Retysp (Typ))) is
when Access_Kind =>
return True;
when E_Array_Type
| E_Array_Subtype
=>
- return Is_Deep (Component_Type (Underlying_Type (Typ)));
+ return Is_Deep (Component_Type (Retysp (Typ)));
when Record_Kind =>
declare
Comp : Entity_Id;
begin
- Comp := First_Component_Or_Discriminant (Typ);
+ Comp := First_Component_Or_Discriminant (Retysp (Typ));
while Present (Comp) loop
- if Is_Deep (Etype (Comp)) then
+
+ -- Ignore components not visible in SPARK
+
+ if Component_Is_Visible_In_SPARK (Comp)
+ and then Is_Deep (Etype (Comp))
+ then
return True;
end if;
Next_Component_Or_Discriminant (Comp);
@@ -3783,14 +3861,14 @@ package body Sem_SPARK is
=>
return False;
- -- The following should not arise as underlying types
+ -- Ignore full view of types if it is not in SPARK
when E_Private_Type
| E_Private_Subtype
| E_Limited_Private_Type
| E_Limited_Private_Subtype
=>
- raise Program_Error;
+ return False;
end case;
end Is_Deep;
@@ -3910,8 +3988,10 @@ package body Sem_SPARK is
when N_Selected_Component =>
if Nkind (Expr_Elt) /= N_Selected_Component
- or else Entity (Selector_Name (Prefix_Elt))
- /= Entity (Selector_Name (Expr_Elt))
+ or else Original_Record_Component
+ (Entity (Selector_Name (Prefix_Elt)))
+ /= Original_Record_Component
+ (Entity (Selector_Name (Expr_Elt)))
then
return False;
end if;
@@ -3962,7 +4042,10 @@ package body Sem_SPARK is
Attribute_Update
or else
Get_Attribute_Id (Attribute_Name (Expr)) =
- Attribute_Loop_Entry))
+ Attribute_Loop_Entry
+ or else
+ Get_Attribute_Id (Attribute_Name (Expr)) =
+ Attribute_Image))
or else Nkind (Expr) = N_Op_Concat;
end Is_Subpath_Expression;
@@ -3985,7 +4068,7 @@ package body Sem_SPARK is
-- and the function's first parameter is of an access type.
- and then Is_Access_Type (Etype (First_Formal (E)));
+ and then Is_Access_Type (Retysp (Etype (First_Formal (E))));
end Is_Traversal_Function;
--------------------------------
@@ -4363,14 +4446,16 @@ package body Sem_SPARK is
begin
Set_Root_Object (N, Root, Is_Deref);
- if Is_Deref then
- Error_Msg_NE
- ("insufficient permission on dereference from &", N, Root);
- else
- Error_Msg_NE ("insufficient permission for &", N, Root);
- end if;
+ if Emit_Messages then
+ if Is_Deref then
+ Error_Msg_NE
+ ("insufficient permission on dereference from &", N, Root);
+ else
+ Error_Msg_NE ("insufficient permission for &", N, Root);
+ end if;
- Perm_Mismatch (N, Perm, Found_Perm, Expl, Forbidden_Perm);
+ Perm_Mismatch (N, Perm, Found_Perm, Expl, Forbidden_Perm);
+ end if;
end Perm_Error;
-------------------------------
@@ -4385,10 +4470,12 @@ package body Sem_SPARK is
Expl : Node_Id)
is
begin
- Error_Msg_Node_2 := Subp;
- Error_Msg_NE ("insufficient permission for & when returning from &",
- Subp, E);
- Perm_Mismatch (Subp, Perm, Found_Perm, Expl);
+ if Emit_Messages then
+ Error_Msg_Node_2 := Subp;
+ Error_Msg_NE ("insufficient permission for & when returning from &",
+ Subp, E);
+ Perm_Mismatch (Subp, Perm, Found_Perm, Expl);
+ end if;
end Perm_Error_Subprogram_End;
------------------
@@ -4429,7 +4516,9 @@ package body Sem_SPARK is
Var := Key.K;
Borrowed := Get (Current_Borrowers, Var);
- if Is_Prefix_Or_Almost (Pref => Borrowed, Expr => Expr) then
+ if Is_Prefix_Or_Almost (Pref => Borrowed, Expr => Expr)
+ and then Emit_Messages
+ then
Error_Msg_Sloc := Sloc (Borrowed);
Error_Msg_N ("object was borrowed #", Expr);
end if;
@@ -4465,7 +4554,9 @@ package body Sem_SPARK is
Var := Key.K;
Observed := Get (Current_Observers, Var);
- if Is_Prefix_Or_Almost (Pref => Observed, Expr => Expr) then
+ if Is_Prefix_Or_Almost (Pref => Observed, Expr => Expr)
+ and then Emit_Messages
+ then
Error_Msg_Sloc := Sloc (Observed);
Error_Msg_N ("object was observed #", Expr);
end if;
@@ -4543,6 +4634,7 @@ package body Sem_SPARK is
if Is_Deep (Expr_Type)
and then not Inside_Procedure_Call
and then Present (Get_Root_Object (Expr))
+ and then Emit_Messages
then
Error_Msg_N ("illegal move during elaboration", Expr);
end if;
@@ -4587,7 +4679,7 @@ package body Sem_SPARK is
-- Forbidden during elaboration
if Inside_Elaboration then
- if not Inside_Procedure_Call then
+ if not Inside_Procedure_Call and then Emit_Messages then
Error_Msg_N ("illegal borrow during elaboration", Expr);
end if;
@@ -4606,7 +4698,7 @@ package body Sem_SPARK is
-- Forbidden during elaboration
if Inside_Elaboration then
- if not Inside_Procedure_Call then
+ if not Inside_Procedure_Call and then Emit_Messages then
Error_Msg_N ("illegal observe during elaboration", Expr);
end if;
@@ -4803,7 +4895,7 @@ package body Sem_SPARK is
while Present (Formal) loop
Return_Parameter_Or_Global
(Id => Formal,
- Typ => Underlying_Type (Etype (Formal)),
+ Typ => Retysp (Etype (Formal)),
Kind => Ekind (Formal),
Subp => Subp,
Global_Var => False);
@@ -4876,6 +4968,7 @@ package body Sem_SPARK is
E : Entity_Id;
Expl : Node_Id)
is
+ Check_Ty : constant Entity_Id := Retysp (E);
begin
-- Shallow extensions are set to RW
@@ -4894,7 +4987,7 @@ package body Sem_SPARK is
-- precision.
when Entire_Object =>
- case Ekind (E) is
+ case Ekind (Check_Ty) is
when E_Array_Type
| E_Array_Subtype
=>
@@ -4908,7 +5001,8 @@ package body Sem_SPARK is
Permission => Read_Write,
Children_Permission => Read_Write));
begin
- Set_Perm_Extensions_Move (C, Component_Type (E), Expl);
+ Set_Perm_Extensions_Move
+ (C, Component_Type (Check_Ty), Expl);
T.all.Tree := (Kind => Array_Component,
Is_Node_Deep => Is_Node_Deep (T),
Explanation => Expl,
@@ -4923,17 +5017,36 @@ package body Sem_SPARK is
Hashtbl : Perm_Tree_Maps.Instance;
begin
- Comp := First_Component_Or_Discriminant (E);
+ Comp := First_Component_Or_Discriminant (Check_Ty);
while Present (Comp) loop
- C := new Perm_Tree_Wrapper'
- (Tree =>
- (Kind => Entire_Object,
- Is_Node_Deep => Is_Deep (Etype (Comp)),
- Explanation => Expl,
- Permission => Read_Write,
- Children_Permission => Read_Write));
- Set_Perm_Extensions_Move (C, Etype (Comp), Expl);
- Perm_Tree_Maps.Set (Hashtbl, Comp, C);
+
+ -- Unfold components which are visible in SPARK
+
+ if Component_Is_Visible_In_SPARK (Comp) then
+ C := new Perm_Tree_Wrapper'
+ (Tree =>
+ (Kind => Entire_Object,
+ Is_Node_Deep => Is_Deep (Etype (Comp)),
+ Explanation => Expl,
+ Permission => Read_Write,
+ Children_Permission => Read_Write));
+ Set_Perm_Extensions_Move (C, Etype (Comp), Expl);
+
+ -- Hidden components are never deep
+
+ else
+ C := new Perm_Tree_Wrapper'
+ (Tree =>
+ (Kind => Entire_Object,
+ Is_Node_Deep => False,
+ Explanation => Expl,
+ Permission => Read_Write,
+ Children_Permission => Read_Write));
+ Set_Perm_Extensions (C, Read_Write, Expl => Expl);
+ end if;
+
+ Perm_Tree_Maps.Set
+ (Hashtbl, Original_Record_Component (Comp), C);
Next_Component_Or_Discriminant (Comp);
end loop;
@@ -4955,7 +5068,8 @@ package body Sem_SPARK is
Set_Perm_Extensions (T, No_Access, Expl);
when Array_Component =>
- Set_Perm_Extensions_Move (Get_Elem (T), Component_Type (E), Expl);
+ Set_Perm_Extensions_Move
+ (Get_Elem (T), Component_Type (Check_Ty), Expl);
when Record_Component =>
declare
@@ -4963,11 +5077,23 @@ package body Sem_SPARK is
Comp : Entity_Id;
begin
- Comp := First_Component_Or_Discriminant (E);
+ Comp := First_Component_Or_Discriminant (Check_Ty);
while Present (Comp) loop
- C := Perm_Tree_Maps.Get (Component (T), Comp);
+ C := Perm_Tree_Maps.Get
+ (Component (T), Original_Record_Component (Comp));
pragma Assert (C /= null);
- Set_Perm_Extensions_Move (C, Etype (Comp), Expl);
+
+ -- Move visible components
+
+ if Component_Is_Visible_In_SPARK (Comp) then
+ Set_Perm_Extensions_Move (C, Etype (Comp), Expl);
+
+ -- Hidden components are never deep
+
+ else
+ Set_Perm_Extensions (C, Read_Write, Expl => Expl);
+ end if;
+
Next_Component_Or_Discriminant (Comp);
end loop;
end;
@@ -5073,7 +5199,9 @@ package body Sem_SPARK is
if Kind (C) = Record_Component then
declare
- Comp : constant Entity_Id := Entity (Selector_Name (N));
+ Comp : constant Entity_Id :=
+ Original_Record_Component
+ (Entity (Selector_Name (N)));
D : constant Perm_Tree_Access :=
Perm_Tree_Maps.Get (Component (C), Comp);
pragma Assert (D /= null);
@@ -5102,11 +5230,14 @@ package body Sem_SPARK is
begin
Comp :=
- First_Component_Or_Discriminant (Etype (Prefix (N)));
+ First_Component_Or_Discriminant
+ (Retysp (Etype (Prefix (N))));
while Present (Comp) loop
if Perm /= None
- and then Comp = Entity (Selector_Name (N))
+ and then Original_Record_Component (Comp) =
+ Original_Record_Component
+ (Entity (Selector_Name (N)))
then
P := Perm;
else
@@ -5116,15 +5247,22 @@ package body Sem_SPARK is
D := new Perm_Tree_Wrapper'
(Tree =>
(Kind => Entire_Object,
- Is_Node_Deep => Is_Deep (Etype (Comp)),
+ Is_Node_Deep =>
+ -- Hidden components are never deep
+ Component_Is_Visible_In_SPARK (Comp)
+ and then Is_Deep (Etype (Comp)),
Explanation => Expl,
Permission => P,
Children_Permission => Child_P));
- Perm_Tree_Maps.Set (Hashtbl, Comp, D);
+ Perm_Tree_Maps.Set
+ (Hashtbl, Original_Record_Component (Comp), D);
-- Store the tree to return for this component
- if Comp = Entity (Selector_Name (N)) then
+ if Original_Record_Component (Comp) =
+ Original_Record_Component
+ (Entity (Selector_Name (N)))
+ then
D_This := D;
end if;
@@ -5380,14 +5518,6 @@ package body Sem_SPARK is
-- Functions cannot have outputs in SPARK
elsif Ekind (Subp) = E_Function then
- if Kind = E_Out_Parameter then
- Error_Msg_N ("function with OUT parameter is not "
- & "allowed in SPARK", Id);
- else
- Error_Msg_N ("function with `IN OUT` parameter is not "
- & "allowed in SPARK", Id);
- end if;
-
return;
-- Deep types define a borrow or a move
@@ -5424,7 +5554,7 @@ package body Sem_SPARK is
while Present (Formal) loop
Setup_Parameter_Or_Global
(Id => Formal,
- Typ => Underlying_Type (Etype (Formal)),
+ Typ => Retysp (Etype (Formal)),
Kind => Ekind (Formal),
Subp => Subp,
Global_Var => False,
@@ -5457,11 +5587,12 @@ package body Sem_SPARK is
while Present (Comp) loop
Setup_Parameter_Or_Global
(Id => Comp,
- Typ => Underlying_Type (Etype (Comp)),
+ Typ => Retysp (Etype (Comp)),
Kind => Kind,
Subp => Subp,
Global_Var => False,
Expl => Comp);
+
Next_Component_Or_Discriminant (Comp);
end loop;
end Setup_Protected_Components;
diff --git a/gcc/ada/sem_spark.ads b/gcc/ada/sem_spark.ads
index ee4126acc5df63628a69d9e0d402b4685fb4c16d..0e8b29b41f7bf2176a9d98549fa00fe0f7d2607b 100644
--- a/gcc/ada/sem_spark.ads
+++ b/gcc/ada/sem_spark.ads
@@ -132,12 +132,34 @@
-- get read-write permission, which can be specified using the node's
-- Children_Permission field.
+-- The implementation is done as a generic, so that GNATprove can instantiate
+-- it with suitable formal arguments that depend on the SPARK_Mode boundary
+-- as well as the two-phase architecture of GNATprove (which runs the GNAT
+-- front end twice, once for global generation and once for analysis).
+
with Types; use Types;
+generic
+ with function Retysp (X : Entity_Id) return Entity_Id;
+ -- Return the representative type in SPARK for a type.
+
+ with function Component_Is_Visible_In_SPARK (C : Entity_Id) return Boolean;
+ -- Return whether a component is visible in SPARK. No aliasing check is
+ -- performed for a component that is visible.
+
+ with function Emit_Messages return Boolean;
+ -- Return True when error messages should be emitted.
+
package Sem_SPARK is
procedure Check_Safe_Pointers (N : Node_Id);
-- The entry point of this package. It analyzes a node and reports errors
-- when there are violations of ownership rules.
+ function Is_Deep (Typ : Entity_Id) return Boolean;
+ -- A function that can tell whether a type is deep. Returns True if the
+ -- type passed as argument is deep.
+
+ function Is_Traversal_Function (E : Entity_Id) return Boolean;
+
end Sem_SPARK;