[COMMITTED] ada: Cleanup SPARK legality checking
Checks
Commit Message
From: Yannick Moy <moy@adacore.com>
Move one SPARK legality check from GNAT to GNATprove, and cleanup
other uses of SPARK_Mode for legality checking.
gcc/ada/
* sem_ch4.adb (Analyze_Selected_Component): Check correct mode
variable for GNATprove.
* sem_prag.adb (Refined_State): Call SPARK_Msg_NE which checks
value of SPARK_Mode before issuing a message.
* sem_res.adb (Resolve_Entity_Name): Remove legality check for
SPARK RM 6.1.9(1), moved to GNATprove.
Tested on x86_64-pc-linux-gnu, committed on master.
---
gcc/ada/sem_ch4.adb | 10 ++---
gcc/ada/sem_prag.adb | 12 +++---
gcc/ada/sem_res.adb | 100 -------------------------------------------
3 files changed, 10 insertions(+), 112 deletions(-)
@@ -6025,17 +6025,17 @@ package body Sem_Ch4 is
-- Emit appropriate message. The node will be replaced
-- by an appropriate raise statement.
- -- Note that in SPARK mode, as with all calls to apply a
- -- compile time constraint error, this will be made into
- -- an error to simplify the processing of the formal
- -- verification backend.
+ -- Note that in GNATprove mode, as with all calls to
+ -- apply a compile time constraint error, this will be
+ -- made into an error to simplify the processing of the
+ -- formal verification backend.
Apply_Compile_Time_Constraint_Error
(N, "component not present in }??",
CE_Discriminant_Check_Failed,
Ent => Prefix_Type,
Emit_Message =>
- SPARK_Mode = On or not In_Instance_Not_Visible);
+ GNATprove_Mode or not In_Instance_Not_Visible);
return;
end if;
@@ -23375,15 +23375,13 @@ package body Sem_Prag is
Analyze_If_Present (Pragma_SPARK_Mode);
-- State refinement is allowed only when the corresponding package
- -- declaration has non-null pragma Abstract_State. Refinement not
- -- enforced when SPARK checks are suppressed (SPARK RM 7.2.2(3)).
+ -- declaration has non-null pragma Abstract_State (SPARK RM
+ -- 7.2.2(3)).
- if SPARK_Mode /= Off
- and then
- (No (Abstract_States (Spec_Id))
- or else Has_Null_Abstract_State (Spec_Id))
+ if No (Abstract_States (Spec_Id))
+ or else Has_Null_Abstract_State (Spec_Id)
then
- Error_Msg_NE
+ SPARK_Msg_NE
("useless refinement, package & does not define abstract "
& "states", N, Spec_Id);
return;
@@ -7787,14 +7787,6 @@ package body Sem_Res is
-- Determine whether Expr is part of an N_Attribute_Reference
-- expression.
- function In_Attribute_Old (Expr : Node_Id) return Boolean;
- -- Determine whether Expr is in attribute Old
-
- function Within_Exceptional_Cases_Consequence
- (Expr : Node_Id)
- return Boolean;
- -- Determine whether Expr is part of an Exceptional_Cases consequence
-
----------------------------------------
-- Is_Assignment_Or_Object_Expression --
----------------------------------------
@@ -7836,31 +7828,6 @@ package body Sem_Res is
end if;
end Is_Assignment_Or_Object_Expression;
- ----------------------
- -- In_Attribute_Old --
- ----------------------
-
- function In_Attribute_Old (Expr : Node_Id) return Boolean is
- N : Node_Id := Expr;
- begin
- while Present (N) loop
- if Nkind (N) = N_Attribute_Reference
- and then Attribute_Name (N) = Name_Old
- then
- return True;
-
- -- Prevent the search from going too far
-
- elsif Is_Body_Or_Package_Declaration (N) then
- return False;
- end if;
-
- N := Parent (N);
- end loop;
-
- return False;
- end In_Attribute_Old;
-
-----------------------------
-- Is_Attribute_Expression --
-----------------------------
@@ -7884,39 +7851,6 @@ package body Sem_Res is
return False;
end Is_Attribute_Expression;
- ------------------------------------------
- -- Within_Exceptional_Cases_Consequence --
- ------------------------------------------
-
- function Within_Exceptional_Cases_Consequence
- (Expr : Node_Id)
- return Boolean
- is
- Context : Node_Id := Parent (Expr);
- begin
- while Present (Context) loop
- if Nkind (Context) = N_Pragma then
-
- -- In Exceptional_Cases references to formal parameters are
- -- only allowed within consequences, so it is enough to
- -- recognize the pragma itself.
-
- if Get_Pragma_Id (Context) = Pragma_Exceptional_Cases then
- return True;
- end if;
-
- -- Prevent the search from going too far
-
- elsif Is_Body_Or_Package_Declaration (Context) then
- return False;
- end if;
-
- Context := Parent (Context);
- end loop;
-
- return False;
- end Within_Exceptional_Cases_Consequence;
-
-- Local variables
E : constant Entity_Id := Entity (N);
@@ -8048,40 +7982,6 @@ package body Sem_Res is
if SPARK_Mode = On then
- -- Parameters of modes OUT or IN OUT of the subprogram shall not
- -- occur in the consequences of an exceptional contract unless
- -- they are either passed by reference or occur in the prefix
- -- of a reference to the 'Old attribute. For convenience, we also
- -- allow them as prefixes of attributes that do not actually read
- -- data from the object.
-
- if Ekind (E) in E_Out_Parameter | E_In_Out_Parameter
- and then Scope (E) = Current_Scope_No_Loops
- and then Within_Exceptional_Cases_Consequence (N)
- and then not In_Attribute_Old (N)
- and then not (Nkind (Parent (N)) = N_Attribute_Reference
- and then
- Attribute_Name (Parent (N)) in Name_Constrained
- | Name_First
- | Name_Last
- | Name_Length
- | Name_Range)
- and then not Is_By_Reference_Type (Etype (E))
- and then not Is_Aliased (E)
- then
- if Ekind (E) = E_Out_Parameter then
- Error_Msg_N
- ("formal parameter of mode `OUT` cannot appear " &
- "in consequence of Exceptional_Cases", N);
- else
- Error_Msg_N
- ("formal parameter of mode `IN OUT` cannot appear " &
- "in consequence of Exceptional_Cases", N);
- end if;
- Error_Msg_N
- ("\only parameters passed by reference are allowed", N);
- end if;
-
-- Check for possible elaboration issues with respect to reads of
-- variables. The act of renaming the variable is not considered a
-- read as it simply establishes an alias.