diff options
| -rw-r--r-- | gcc/ada/ChangeLog | 8 | ||||
| -rw-r--r-- | gcc/ada/sem_spark.adb | 63 | ||||
| -rw-r--r-- | gcc/ada/sem_spark.ads | 4 |
3 files changed, 62 insertions, 13 deletions
diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index 0f7cd2d..748f1bf 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -1,5 +1,13 @@ 2019-07-23 Yannick Moy <moy@adacore.com> + * sem_spark.ads (Is_Local_Context): New function. + * sem_spark.adb (Check_Declaration): Issue errors on violations + of SPARK RM 3.10(4) + (Process_Path): Do not issue error on borrow/observe during + elaboration, as these are caught by the new rule. + +2019-07-23 Yannick Moy <moy@adacore.com> + * exp_ch7.adb (Create_Finalizer): Force finalizer not to be Ghost enabled. * exp_dbug.adb (Get_External_Name): Explain special case of diff --git a/gcc/ada/sem_spark.adb b/gcc/ada/sem_spark.adb index 0de51f8..a60a6cb 100644 --- a/gcc/ada/sem_spark.adb +++ b/gcc/ada/sem_spark.adb @@ -1419,9 +1419,37 @@ package body Sem_SPARK is Check_Expression (Subtype_Indication (Decl), Read); when N_Object_Declaration => + Expr := Expression (Decl); + Check_Type (Target_Typ); - Expr := Expression (Decl); + -- A declaration of a stand-alone object of an anonymous access + -- type shall have an explicit initial value and shall occur + -- immediately within a subprogram body, an entry body, or a + -- block statement (SPARK RM 3.10(4)). + + if Is_Anonymous_Access_Type (Target_Typ) then + declare + Scop : constant Entity_Id := Scope (Target); + begin + if not Is_Local_Context (Scop) then + if Emit_Messages then + Error_Msg_N + ("object of anonymous access type must be declared " + & "immediately within a subprogram, entry or block " + & "(SPARK RM 3.10(4))", Decl); + end if; + end if; + end; + + if No (Expr) then + if Emit_Messages then + Error_Msg_N ("object of anonymous access type must be " + & "initialized (SPARK RM 3.10(4))", Decl); + end if; + end if; + end if; + if Present (Expr) then Check_Assignment (Target => Target, Expr => Expr); @@ -2848,9 +2876,14 @@ package body Sem_SPARK is -- independently for R permission. Outputs are checked -- independently to have RW permission on exit. - when Pragma_Contract_Cases + -- Postconditions are checked for correct use of 'Old, but starting + -- from the corresponding declaration, in order to avoid dealing with + -- with contracts on generic subprograms, which are not handled in + -- GNATprove. + + when Pragma_Precondition | Pragma_Postcondition - | Pragma_Precondition + | Pragma_Contract_Cases | Pragma_Refined_Post => null; @@ -3993,6 +4026,16 @@ package body Sem_SPARK is end case; end Is_Deep; + ---------------------- + -- Is_Local_Context -- + ---------------------- + + function Is_Local_Context (Scop : Entity_Id) return Boolean is + begin + return Is_Subprogram_Or_Entry (Scop) + or else Ekind (Scop) = E_Block; + end Is_Local_Context; + ------------------------ -- Is_Path_Expression -- ------------------------ @@ -4863,13 +4906,10 @@ package body Sem_SPARK is when Borrow => - -- Forbidden during elaboration + -- Forbidden during elaboration, an error is already issued in + -- Check_Declaration, just return. if Inside_Elaboration then - if not Inside_Procedure_Call and then Emit_Messages then - Error_Msg_N ("illegal borrow during elaboration", Expr); - end if; - return; end if; @@ -4882,13 +4922,10 @@ package body Sem_SPARK is when Observe => - -- Forbidden during elaboration + -- Forbidden during elaboration, an error is already issued in + -- Check_Declaration, just return. if Inside_Elaboration then - if not Inside_Procedure_Call and then Emit_Messages then - Error_Msg_N ("illegal observe during elaboration", Expr); - end if; - return; end if; diff --git a/gcc/ada/sem_spark.ads b/gcc/ada/sem_spark.ads index 0e8b29b..195e833 100644 --- a/gcc/ada/sem_spark.ads +++ b/gcc/ada/sem_spark.ads @@ -162,4 +162,8 @@ package Sem_SPARK is function Is_Traversal_Function (E : Entity_Id) return Boolean; + function Is_Local_Context (Scop : Entity_Id) return Boolean; + -- Return if a given scope defines a local context where it is legal to + -- declare a variable of anonymous access type. + end Sem_SPARK; |