From 2d9a8c0ba10d03608aa2add8cf9f33053ab8c421 Mon Sep 17 00:00:00 2001 From: Maroua Maalej Date: Wed, 26 Sep 2018 09:19:33 +0000 Subject: [PATCH] [Ada] SPARK: fix a bug related to loop exit environment 2018-09-26 Maroua Maalej gcc/ada/ * sem_spark.adb (Check_Loop_Statement): Fix a bug related to loop exit environment. (Check_Statement): fixing a bug when comparing the source and target in an assignment statement. From-SVN: r264631 --- gcc/ada/ChangeLog | 7 ++++ gcc/ada/sem_spark.adb | 74 +++++++++++++++++++++++++++++-------------- 2 files changed, 58 insertions(+), 23 deletions(-) diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index 80d119d87c7..c8145cfb141 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -1,3 +1,10 @@ +2018-09-26 Maroua Maalej + + * sem_spark.adb (Check_Loop_Statement): Fix a bug related to + loop exit environment. + (Check_Statement): fixing a bug when comparing the source and + target in an assignment statement. + 2018-09-26 Hristian Kirtchev * sem_ch12.adb (Instantiate_Package_Body): Capture and restore diff --git a/gcc/ada/sem_spark.adb b/gcc/ada/sem_spark.adb index 920c3ff210c..9a2209233b1 100644 --- a/gcc/ada/sem_spark.adb +++ b/gcc/ada/sem_spark.adb @@ -866,8 +866,17 @@ package body Sem_SPARK is Target_Ent : constant Entity_Id := Defining_Identifier (Decl); Target_Typ : Node_Id renames Etype (Target_Ent); - Check : Boolean := True; + + Target_View_Typ : Entity_Id; + + Check : Boolean := True; begin + if Present (Full_View (Target_Typ)) then + Target_View_Typ := Full_View (Target_Typ); + else + Target_View_Typ := Target_Typ; + end if; + case N_Declaration'(Nkind (Decl)) is when N_Full_Type_Declaration => if not Has_Ownership_Aspect_True (Target_Ent, "type declaration") @@ -878,7 +887,7 @@ package body Sem_SPARK is -- ??? What about component declarations with defaults. when N_Object_Declaration => - if (Is_Access_Type (Target_Typ) + if (Is_Access_Type (Target_View_Typ) or else Is_Deep (Target_Typ)) and then not Has_Ownership_Aspect_True (Target_Ent, "Object declaration ") @@ -886,7 +895,7 @@ package body Sem_SPARK is Check := False; end if; - if Is_Anonymous_Access_Type (Target_Typ) + if Is_Anonymous_Access_Type (Target_View_Typ) and then not Present (Expression (Decl)) then @@ -905,7 +914,7 @@ package body Sem_SPARK is -- Initializing object, access type - if Is_Access_Type (Target_Typ) then + if Is_Access_Type (Target_View_Typ) then -- Initializing object, constant access type @@ -913,7 +922,7 @@ package body Sem_SPARK is -- Initializing object, constant access to variable type - if not Is_Access_Constant (Target_Typ) then + if not Is_Access_Constant (Target_View_Typ) then Current_Checking_Mode := Borrow; -- Initializing object, constant access to constant type @@ -921,7 +930,7 @@ package body Sem_SPARK is -- Initializing object, -- constant access to constant anonymous type. - elsif Is_Anonymous_Access_Type (Target_Typ) then + elsif Is_Anonymous_Access_Type (Target_View_Typ) then -- This is an object declaration so the target -- of the assignement is a stand-alone object. @@ -943,12 +952,12 @@ package body Sem_SPARK is else -- Initializing object, variable access to variable type - if not Is_Access_Constant (Target_Typ) then + if not Is_Access_Constant (Target_View_Typ) then -- Initializing object, variable named access to -- variable type. - if not Is_Anonymous_Access_Type (Target_Typ) then + if not Is_Anonymous_Access_Type (Target_View_Typ) then Current_Checking_Mode := Move; -- Initializing object, variable anonymous access to @@ -968,7 +977,7 @@ package body Sem_SPARK is -- Initializing object, -- variable named access to constant type. - if not Is_Anonymous_Access_Type (Target_Typ) then + if not Is_Anonymous_Access_Type (Target_View_Typ) then Error_Msg_N ("assignment not allowed, Ownership " & "Aspect False (Anonymous Access " & "Object)", Decl); @@ -1201,6 +1210,7 @@ package body Sem_SPARK is Check_Node (Right_Opnd (Expr)); -- Forbid all deep expressions for Attribute ??? + -- What about generics? (formal parameters). when N_Attribute_Reference => case Attribute_Name (Expr) is @@ -1690,12 +1700,12 @@ package body Sem_SPARK is if Exit_Env /= null then Copy_Env (From => Exit_Env.all, To => Current_Perm_Env); + Free_Env (Loop_Env.all); + Free_Env (Exit_Env.all); else Copy_Env (From => Loop_Env.all, To => Current_Perm_Env); + Free_Env (Loop_Env.all); end if; - - Free_Env (Loop_Env.all); - Free_Env (Exit_Env.all); end; end Check_Loop_Statement; @@ -2247,7 +2257,8 @@ package body Sem_SPARK is -- Target /= source root if Nkind_In (Expression (Stmt), N_Allocator, N_Null) - or else St_Name /= Get_Root (Expression (Stmt)) + or else Entity (St_Name) /= + Entity (Get_Root (Expression (Stmt))) then Error_Msg_N ("assignment not allowed, anonymous " & "access Object with Different Root", @@ -2307,7 +2318,10 @@ package body Sem_SPARK is -- Assigning to composite (deep) type. elsif Is_Deep (Ty_St_Name) then - if Ekind (Ty_St_Name) = E_Record_Type then + if Ekind_In (Ty_St_Name, + E_Record_Type, + E_Record_Subtype) + then declare Elmt : Entity_Id := First_Component_Or_Discriminant (Ty_St_Name); @@ -2333,6 +2347,13 @@ package body Sem_SPARK is if Check then Current_Checking_Mode := Move; end if; + + elsif Ekind_In (Ty_St_Name, + E_Array_Type, + E_Array_Subtype) + and then Check + then + Current_Checking_Mode := Move; end if; -- Now handle legality rules of using a borrowed, observed, @@ -3399,7 +3420,7 @@ package body Sem_SPARK is if State_N = Moved then Error_Msg_N ("?the source or one of its extensions has" - & " already been moved", N); + & " already been moved", N); end if; declare @@ -4451,9 +4472,16 @@ package body Sem_SPARK is Mode : Formal_Kind; Global_Var : Boolean) is - Elem : Perm_Tree_Access; + Elem : Perm_Tree_Access; + View_Typ : Entity_Id; begin + if Present (Full_View (Etype (Id))) then + View_Typ := Full_View (Etype (Id)); + else + View_Typ := Etype (Id); + end if; + Elem := new Perm_Tree_Wrapper' (Tree => (Kind => Entire_Object, @@ -4481,16 +4509,16 @@ package body Sem_SPARK is -- a function, and a borrow operation for a procedure. if not Global_Var then - if (Is_Access_Type (Etype (Id)) - and then Is_Access_Constant (Etype (Id)) - and then Is_Anonymous_Access_Type (Etype (Id))) + if (Is_Access_Type (View_Typ) + and then Is_Access_Constant (View_Typ) + and then Is_Anonymous_Access_Type (View_Typ)) or else - (Is_Access_Type (Etype (Id)) + (Is_Access_Type (View_Typ) and then Ekind (Scope (Id)) = E_Function) or else - (not Is_Access_Type (Etype (Id)) - and then Is_Deep (Etype (Id)) - and then not Is_Anonymous_Access_Type (Etype (Id))) + (not Is_Access_Type (View_Typ) + and then Is_Deep (View_Typ) + and then not Is_Anonymous_Access_Type (View_Typ)) then Elem.all.Tree.Permission := Observed; Elem.all.Tree.Children_Permission := Observed; -- 2.30.2