diff options
| -rw-r--r-- | gcc/ada/sem_ch4.adb | 10 | ||||
| -rw-r--r-- | gcc/ada/sem_prag.adb | 12 | ||||
| -rw-r--r-- | gcc/ada/sem_res.adb | 100 |
3 files changed, 10 insertions, 112 deletions
diff --git a/gcc/ada/sem_ch4.adb b/gcc/ada/sem_ch4.adb index d506944..64aa9a8 100644 --- a/gcc/ada/sem_ch4.adb +++ b/gcc/ada/sem_ch4.adb @@ -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; diff --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb index 9d66fb7..db20f20 100644 --- a/gcc/ada/sem_prag.adb +++ b/gcc/ada/sem_prag.adb @@ -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; diff --git a/gcc/ada/sem_res.adb b/gcc/ada/sem_res.adb index c684075..d81a5af 100644 --- a/gcc/ada/sem_res.adb +++ b/gcc/ada/sem_res.adb @@ -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. |