[Ada] SPARK: fix a bug related to loop exit environment

2018-09-26  Maroua Maalej  <maalej@adacore.com>

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

2 files changed, 58 insertions, 23 deletions

diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog
index 80d119d..c8145cf 100644
--- a/gcc/ada/ChangeLog
+++ b/gcc/ada/ChangeLog
@@ -1,3 +1,10 @@
+2018-09-26  Maroua Maalej  <maalej@adacore.com>
+
+	* 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  <kirtchev@adacore.com>
 
 	* sem_ch12.adb (Instantiate_Package_Body): Capture and restore
diff --git a/gcc/ada/sem_spark.adb b/gcc/ada/sem_spark.adb
index 920c3ff..9a22092 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;