]> gcc.gnu.org Git - gcc.git/blobdiff - gcc/ada/sem_ch7.adb
ada: Implement change to SPARK RM rule on state refinement
[gcc.git] / gcc / ada / sem_ch7.adb
index c43686b10ee122734bd765ebc6ccde961a536e8d..284706981d65d2b5a1f339a679ea1b08fb5760e2 100644 (file)
@@ -72,6 +72,7 @@ with Sinfo.Utils;    use Sinfo.Utils;
 with Sinput;         use Sinput;
 with Style;
 with Uintp;          use Uintp;
+with Warnsw;         use Warnsw;
 
 with GNAT.HTable;
 
@@ -304,6 +305,46 @@ package body Sem_Ch7 is
             Decl_Id     : Entity_Id;
             In_Instance : Boolean;
             Spec        : Node_Id;
+            Ignore      : Boolean;
+
+            function Set_Referencer_Of_Non_Subprograms return Boolean;
+            --  Set Has_Referencer_Of_Non_Subprograms and call
+            --  Scan_Subprogram_Refs if relevant.
+            --  Return whether Scan_Subprogram_Refs was called.
+
+            ---------------------------------------
+            -- Set_Referencer_Of_Non_Subprograms --
+            ---------------------------------------
+
+            function Set_Referencer_Of_Non_Subprograms return Boolean is
+            begin
+               --  An inlined subprogram body acts as a referencer
+               --  unless we generate C code since inlining is then
+               --  handled by the C compiler.
+
+               --  Note that we test Has_Pragma_Inline here in addition
+               --  to Is_Inlined. We are doing this for a client, since
+               --  we are computing which entities should be public, and
+               --  it is the client who will decide if actual inlining
+               --  should occur, so we need to catch all cases where the
+               --  subprogram may be inlined by the client.
+
+               if (not CCG_Mode or else Has_Pragma_Inline_Always (Decl_Id))
+                 and then (Is_Inlined (Decl_Id)
+                            or else Has_Pragma_Inline (Decl_Id))
+               then
+                  Has_Referencer_Of_Non_Subprograms := True;
+
+                  --  Inspect the statements of the subprogram body
+                  --  to determine whether the body references other
+                  --  subprograms.
+
+                  Scan_Subprogram_Refs (Decl);
+                  return True;
+               else
+                  return False;
+               end if;
+            end Set_Referencer_Of_Non_Subprograms;
 
          begin
             if No (Decls) then
@@ -398,54 +439,17 @@ package body Sem_Ch7 is
                         return True;
                      end if;
 
-                     --  An inlined subprogram body acts as a referencer
-                     --  unless we generate C code since inlining is then
-                     --  handled by the C compiler.
-
-                     --  Note that we test Has_Pragma_Inline here in addition
-                     --  to Is_Inlined. We are doing this for a client, since
-                     --  we are computing which entities should be public, and
-                     --  it is the client who will decide if actual inlining
-                     --  should occur, so we need to catch all cases where the
-                     --  subprogram may be inlined by the client.
-
-                     if not Generate_C_Code
-                       and then (Is_Inlined (Decl_Id)
-                                  or else Has_Pragma_Inline (Decl_Id))
-                     then
-                        Has_Referencer_Of_Non_Subprograms := True;
-
-                        --  Inspect the statements of the subprogram body
-                        --  to determine whether the body references other
-                        --  subprograms.
-
-                        Scan_Subprogram_Refs (Decl);
-                     end if;
+                     Ignore := Set_Referencer_Of_Non_Subprograms;
 
                   --  Otherwise this is a stand alone subprogram body
 
                   else
                      Decl_Id := Defining_Entity (Decl);
 
-                     --  An inlined subprogram body acts as a referencer
-                     --  unless we generate C code since inlining is then
-                     --  handled by the C compiler.
-
-                     if not Generate_C_Code
-                       and then (Is_Inlined (Decl_Id)
-                                  or else Has_Pragma_Inline (Decl_Id))
+                     if not Set_Referencer_Of_Non_Subprograms
+                       and then not Subprogram_Table.Get (Decl_Id)
                      then
-                        Has_Referencer_Of_Non_Subprograms := True;
-
-                        --  Inspect the statements of the subprogram body
-                        --  to determine whether the body references other
-                        --  subprograms.
-
-                        Scan_Subprogram_Refs (Decl);
-
-                     --  Otherwise we can reset Is_Public right away
-
-                     elsif not Subprogram_Table.Get (Decl_Id) then
+                        --  We can reset Is_Public right away
                         Set_Is_Public (Decl_Id, False);
                      end if;
                   end if;
@@ -1239,17 +1243,24 @@ package body Sem_Ch7 is
          Check_Completion;
 
          --  If the package spec does not require an explicit body, then all
-         --  abstract states declared in nested packages cannot possibly get
-         --  a proper refinement (SPARK RM 7.2.2(3)). This check is performed
-         --  only when the compilation unit is the main unit to allow for
-         --  modular SPARK analysis where packages do not necessarily have
-         --  bodies.
+         --  abstract states declared in nested packages cannot possibly get a
+         --  proper refinement (SPARK RM 7.1.4(4) and SPARK RM 7.2.2(3)). This
+         --  check is performed only when the compilation unit is the main
+         --  unit to allow for modular SPARK analysis where packages do not
+         --  necessarily have bodies.
 
          if Is_Comp_Unit then
             Check_State_Refinements
               (Context      => N,
                Is_Main_Unit => Parent (N) = Cunit (Main_Unit));
          end if;
+
+         --  Warn about references to unset objects, which is straightforward
+         --  for packages with no bodies. For packages with bodies this is more
+         --  complicated, because some of the objects might be set between spec
+         --  and body elaboration, in nested or child packages, etc.
+
+         Check_References (Id);
       end if;
 
       --  Set Body_Required indication on the compilation unit node
@@ -1307,11 +1318,10 @@ package body Sem_Ch7 is
       --  private_with_clauses, and remove them at the end of the nested
       --  package.
 
-      procedure Clear_Constants (Id : Entity_Id; FE : Entity_Id);
-      --  Clears constant indications (Never_Set_In_Source, Constant_Value, and
-      --  Is_True_Constant) on all variables that are entities of Id, and on
-      --  the chain whose first element is FE. A recursive call is made for all
-      --  packages and generic packages.
+      procedure Clear_Constants (Id : Entity_Id);
+      --  Clears constant indications (Never_Set_In_Source, Constant_Value,
+      --  and Is_True_Constant) on all variables that are entities of Id.
+      --  A recursive call is made for all packages and generic packages.
 
       procedure Generate_Parent_References;
       --  For a child unit, generate references to parent units, for
@@ -1342,7 +1352,7 @@ package body Sem_Ch7 is
       -- Clear_Constants --
       ---------------------
 
-      procedure Clear_Constants (Id : Entity_Id; FE : Entity_Id) is
+      procedure Clear_Constants (Id : Entity_Id) is
          E : Entity_Id;
 
       begin
@@ -1358,9 +1368,9 @@ package body Sem_Ch7 is
          --  package can contain a renaming declaration to itself, and such
          --  renamings are generated automatically within package instances.
 
-         E := FE;
+         E := First_Entity (Id);
          while Present (E) and then E /= Id loop
-            if Is_Assignable (E) then
+            if Ekind (E) = E_Variable then
                Set_Never_Set_In_Source (E, False);
                Set_Is_True_Constant    (E, False);
                Set_Current_Value       (E, Empty);
@@ -1372,8 +1382,7 @@ package body Sem_Ch7 is
                end if;
 
             elsif Is_Package_Or_Generic_Package (E) then
-               Clear_Constants (E, First_Entity (E));
-               Clear_Constants (E, First_Private_Entity (E));
+               Clear_Constants (E);
             end if;
 
             Next_Entity (E);
@@ -1999,8 +2008,7 @@ package body Sem_Ch7 is
       if Is_Library_Level_Entity (Id)
         or else Is_Generic_Instance (Id)
       then
-         Clear_Constants (Id, First_Entity (Id));
-         Clear_Constants (Id, First_Private_Entity (Id));
+         Clear_Constants (Id);
       end if;
 
       --  Output relevant information as to why the package requires a body.
This page took 0.038035 seconds and 5 git commands to generate.