[Ada] Change SPARK_Mode into GNATprove_Mode, and avoid expansion

Arnaud Charlet charlet@adacore.com
Mon Jan 20 13:44:00 GMT 2014


The use of SPARK_Mode to refer to GNAT being called in the context of
formal verification was confusing, because of the recent addition of a
new pragma SPARK_Mode with a different meaning. This mode of the frontend
has been renamed GNATprove_Mode, to refer to the tool it is used in.
(This is similar to CodePeer_Mode.)

The default setting of Expander_Active to True in this mode has also
been changed to False, which better reflects the light expansion done in
this mode, which has little in common with the true expansion. This should
facilitate maintenance, as Expander_Active is restored to its meaning
of generating code, and explicit mention of GNATprove_Mode is added each
time some specific action is needed in GNATprove mode.

Tested on x86_64-pc-linux-gnu, committed on trunk

2014-01-20  Yannick Moy  <moy@adacore.com>

	* adabkend.adb, ali-util.adb, errout.adb, exp_ch7.adb,
	* exp_dbug.adb, freeze.adb, lib-xref.adb, restrict.adb,
	* sem_attr.adb, sem_ch4.adb, sem_ch5.adb, sem_ch6.adb, sem_ch8.adb,
	* sem_prag.adb, sem_res.adb, sem_util.adb Rename SPARK_Mode into
	GNATprove_Mode.
	* sem_ch13.adb: Remove blank.
	* exp_spark.adb, exp_spark.ads (Expand_SPARK_Call): Only replace
	subprograms by alias for renamings, not for inherited primitive
	operations.
	* exp_util.adb (Expand_Subtype_From_Expr): Apply the expansion
	in GNATprove mode.
	(Remove_Side_Effects): Apply the removal in
	GNATprove mode, for the full analysis of expressions.
	* expander.adb (Expand): Call the light SPARK expansion in GNATprove
	mode.
	(Expander_Mode_Restore, Expander_Mode_Save_And_Set): Ignore
	save/restore actions for Expander_Active flag in GNATprove mode,
	similar to what is done in ASIS mode.
	* frontend.adb (Frontend): Generic bodies are instantiated in
	GNATprove mode.
	* gnat1drv.adb (Adjust_Global_Switches): Set operating
	mode to Check_Semantics in GNATprove mode, although a light
	expansion is still performed.
	(Gnat1drv): Set Back_End_Mode to
	Declarations_Only in GNATprove mode, and later on special case
	the GNATprove mode to continue analysis anyway.
	* lib-writ.adb (Write_ALI): Always generate ALI files in
	GNATprove mode.
	* opt.adb, opt.ads (Full_Expander_Active): Make it equivalent to
	Expander_Active.
	(SPARK_Mode): Renamed as GNATprove_Mode.
	* sem_aggr.adb (Aggregate_Constraint_Checks): Add checks in the
	tree in GNATprove_Mode.
	* sem_ch12.adb (Analyze_Package_Instantiation): Always instantiate
	body in GNATprove mode.
	(Need_Subprogram_Instance_Body): Always instantiate body in GNATprove
	mode.
	* sem_ch3.adb (Constrain_Index, Process_Range_Expr_In_Decl):
	Make sure side effects are removed in GNATprove mode.

-------------- next part --------------
Index: sem_aggr.adb
===================================================================
--- sem_aggr.adb	(revision 206790)
+++ sem_aggr.adb	(working copy)
@@ -454,10 +454,14 @@
          Check_Unset_Reference (Exp);
       end if;
 
-      --  This is really expansion activity, so make sure that expansion
-      --  is on and is allowed.
+      --  This is really expansion activity, so make sure that expansion is
+      --  on and is allowed. In GNATprove mode, we also want check flags to be
+      --  added in the tree, so that the formal verification can rely on those
+      --  to be present.
 
-      if not Expander_Active or else In_Spec_Expression then
+      if not (Expander_Active or GNATprove_Mode)
+        or In_Spec_Expression
+      then
          return;
       end if;
 
@@ -996,10 +1000,10 @@
       --  frozen so that initialization procedures can properly be called
       --  in the resolution that follows.  The replacement of boxes with
       --  initialization calls is properly an expansion activity but it must
-      --  be done during revolution.
+      --  be done during resolution.
 
       if Expander_Active
-        and then  Present (Component_Associations (N))
+        and then Present (Component_Associations (N))
       then
          declare
             Comp : Node_Id;
Index: sem_ch3.adb
===================================================================
--- sem_ch3.adb	(revision 206790)
+++ sem_ch3.adb	(working copy)
@@ -10084,7 +10084,7 @@
                --  SPARK mode. Since this is legal code with respect to theorem
                --  proving, do not emit the error.
 
-               if SPARK_Mode
+               if GNATprove_Mode
                  and then Nkind (Exp) = N_Function_Call
                  and then Nkind (Parent (Exp)) = N_Object_Declaration
                  and then not Comes_From_Source
@@ -12223,12 +12223,12 @@
          --  needed, since checks may cause duplication of the expressions
          --  which must not be reevaluated.
 
-         --  The forced evaluation removes side effects from expressions,
-         --  which should occur also in SPARK mode. Otherwise, we end up with
+         --  The forced evaluation removes side effects from expressions, which
+         --  should occur also in GNATprove mode. Otherwise, we end up with
          --  unexpected insertions of actions at places where this is not
          --  supposed to occur, e.g. on default parameters of a call.
 
-         if Expander_Active then
+         if Expander_Active or GNATprove_Mode then
             Force_Evaluation (Low_Bound (R));
             Force_Evaluation (High_Bound (R));
          end if;
@@ -18865,11 +18865,11 @@
             --  duplication of the expression without forcing evaluation.
 
             --  The forced evaluation removes side effects from expressions,
-            --  which should occur also in SPARK mode. Otherwise, we end up
+            --  which should occur also in GNATprove mode. Otherwise, we end up
             --  with unexpected insertions of actions at places where this is
             --  not supposed to occur, e.g. on default parameters of a call.
 
-            if Expander_Active then
+            if Expander_Active or GNATprove_Mode then
                Force_Evaluation (Lo);
                Force_Evaluation (Hi);
             end if;
@@ -18980,11 +18980,11 @@
       --  Case of other than an explicit N_Range node
 
       --  The forced evaluation removes side effects from expressions, which
-      --  should occur also in SPARK mode. Otherwise, we end up with unexpected
-      --  insertions of actions at places where this is not supposed to occur,
-      --  e.g. on default parameters of a call.
+      --  should occur also in GNATprove mode. Otherwise, we end up with
+      --  unexpected insertions of actions at places where this is not
+      --  supposed to occur, e.g. on default parameters of a call.
 
-      elsif Expander_Active then
+      elsif Expander_Active or GNATprove_Mode then
          Get_Index_Bounds (R, Lo, Hi);
          Force_Evaluation (Lo);
          Force_Evaluation (Hi);
Index: frontend.adb
===================================================================
--- frontend.adb	(revision 206790)
+++ frontend.adb	(working copy)
@@ -362,7 +362,7 @@
 
          if Operating_Mode = Generate_Code
            or else (Operating_Mode = Check_Semantics
-                     and then ASIS_Mode)
+                     and then (ASIS_Mode or GNATprove_Mode))
          then
             Instantiate_Bodies;
          end if;
Index: exp_spark.adb
===================================================================
--- exp_spark.adb	(revision 206790)
+++ exp_spark.adb	(working copy)
@@ -31,7 +31,6 @@
 with Sem_Res;  use Sem_Res;
 with Sem_Util; use Sem_Util;
 with Sinfo;    use Sinfo;
-with Stand;    use Stand;
 
 package body Exp_SPARK is
 
@@ -94,52 +93,29 @@
    -----------------------
 
    procedure Expand_SPARK_Call (N : Node_Id) is
-      Call_Node   : constant Node_Id := N;
-      Parent_Subp : Entity_Id;
-
    begin
-      --  Ignore if previous error
+      --  If the subprogram is a renaming, replace it in the call with the name
+      --  of the actual subprogram being called. We distinguish renamings from
+      --  inherited primitive operations, which both have an Alias component,
+      --  by looking at the parent node of the entity. The entity for a
+      --  renaming has the function or procedure specification node as
+      --  parent, while an inherited primitive operation has the derived
+      --  type declaration as parent.
 
-      if Nkind (Call_Node) in N_Has_Etype
-        and then Etype (Call_Node) = Any_Type
+      if Nkind (Name (N)) in N_Has_Entity
+        and then Present (Entity (Name (N)))
       then
-         return;
+         declare
+            E : constant Entity_Id := Entity (Name (N));
+         begin
+            if Nkind_In (Parent (E), N_Function_Specification,
+                                     N_Procedure_Specification)
+              and then Present (Alias (E))
+            then
+               Set_Entity (Name (N), Ultimate_Alias (E));
+            end if;
+         end;
       end if;
-
-      --  Call using access to subprogram with explicit dereference
-
-      if Nkind (Name (Call_Node)) = N_Explicit_Dereference then
-         Parent_Subp := Empty;
-
-      --  Case of call to simple entry, where the Name is a selected component
-      --  whose prefix is the task, and whose selector name is the entry name
-
-      elsif Nkind (Name (Call_Node)) = N_Selected_Component then
-         Parent_Subp := Empty;
-
-      --  Case of call to member of entry family, where Name is an indexed
-      --  component, with the prefix being a selected component giving the
-      --  task and entry family name, and the index being the entry index.
-
-      elsif Nkind (Name (Call_Node)) = N_Indexed_Component then
-         Parent_Subp := Empty;
-
-      --  Normal case
-
-      else
-         Parent_Subp := Alias (Entity (Name (Call_Node)));
-      end if;
-
-      --  If the subprogram is a renaming, replace it in the call with the name
-      --  of the actual subprogram being called.
-
-      if Present (Parent_Subp) then
-         Parent_Subp := Ultimate_Alias (Parent_Subp);
-
-         --  The below setting of Entity is suspect, see F109-018 discussion???
-
-         Set_Entity (Name (Call_Node), Parent_Subp);
-      end if;
    end Expand_SPARK_Call;
 
    ------------------------------------------------
Index: exp_spark.ads
===================================================================
--- exp_spark.ads	(revision 206790)
+++ exp_spark.ads	(working copy)
@@ -23,10 +23,9 @@
 --                                                                          --
 ------------------------------------------------------------------------------
 
---  This package implements a light expansion which is used in formal
---  verification mode (SPARK_Mode = True). Instead of a complete expansion
---  of nodes for code generation, this SPARK expansion targets generation
---  of intermediate code for formal verification.
+--  This package implements a light expansion which is used in GNATprove mode.
+--  Instead of a complete expansion of nodes for code generation, this light
+--  expansion targets generation of intermediate code for formal verification.
 
 --  Expand_SPARK is called directly by Expander.Expand.
 
Index: exp_ch7.adb
===================================================================
--- exp_ch7.adb	(revision 206790)
+++ exp_ch7.adb	(working copy)
@@ -937,7 +937,7 @@
       --  Do not create finalization masters in SPARK mode because they result
       --  in unwanted expansion.
 
-      elsif SPARK_Mode then
+      elsif GNATprove_Mode then
          return;
       end if;
 
@@ -2813,7 +2813,7 @@
       --  Do not perform this expansion in SPARK mode because it is not
       --  necessary.
 
-      if SPARK_Mode then
+      if GNATprove_Mode then
          return;
       end if;
 
@@ -2975,7 +2975,7 @@
       --  Do not perform this expansion in SPARK mode because we do not create
       --  finalizers in the first place.
 
-      if SPARK_Mode then
+      if GNATprove_Mode then
          return;
       end if;
 
@@ -3658,7 +3658,7 @@
       --  this node and enclosed expression are not expanded, so do not apply
       --  any transformations here.
 
-      elsif SPARK_Mode
+      elsif GNATprove_Mode
         and then Nkind (Wrap_Node) = N_Pragma
         and then Get_Pragma_Id (Wrap_Node) = Pragma_Check
       then
Index: sem_ch5.adb
===================================================================
--- sem_ch5.adb	(revision 206790)
+++ sem_ch5.adb	(working copy)
@@ -1712,7 +1712,7 @@
         --  Do not perform this expansion in SPARK mode, since the formal
         --  verification directly deals with the source form of the iterator.
 
-        and then not SPARK_Mode
+        and then not GNATprove_Mode
       then
          declare
             Id   : constant Entity_Id := Make_Temporary (Loc, 'R', Iter_Name);
Index: exp_util.adb
===================================================================
--- exp_util.adb	(revision 206790)
+++ exp_util.adb	(working copy)
@@ -2034,12 +2034,22 @@
       --  may be constants that depend on the bounds of a string literal, both
       --  standard string types and more generally arrays of characters.
 
-      if not Expander_Active
+      --  In GNATprove mode, we also need the more precise subtype to be set.
+
+      if not (Expander_Active or GNATprove_Mode)
         and then (No (Etype (Exp)) or else not Is_String_Type (Etype (Exp)))
       then
          return;
       end if;
 
+      --  In GNATprove mode, Unc_Type might not be complete when analyzing
+      --  a generic unit. As generic units are not analyzed directly in
+      --  GNATprove, return here rather than failing later.
+
+      if GNATprove_Mode and then No (Underlying_Type (Unc_Type)) then
+         return;
+      end if;
+
       if Nkind (Exp) = N_Slice then
          declare
             Slice_Type : constant Entity_Id := Etype (First_Index (Exp_Typ));
@@ -6862,9 +6872,11 @@
    --  Start of processing for Remove_Side_Effects
 
    begin
-      --  Handle cases in which there is nothing to do
+      --  Handle cases in which there is nothing to do. In GNATprove mode,
+      --  removal of side effects is useful for the light expansion of
+      --  renamings.
 
-      if not Expander_Active then
+      if not (Expander_Active or (Full_Analysis and GNATprove_Mode)) then
          return;
       end if;
 
@@ -7074,7 +7086,7 @@
          --  free if the resulting value is captured by a variable or a
          --  constant.
 
-         if SPARK_Mode
+         if GNATprove_Mode
            and then Nkind (Parent (Exp)) = N_Object_Declaration
          then
             goto Leave;
@@ -7119,7 +7131,7 @@
          --  types, use a different approach which ignores the secondary stack
          --  and "copies" the returned object.
 
-         if SPARK_Mode then
+         if GNATprove_Mode then
             Res := New_Reference_To (Def_Id, Loc);
             Ref_Type := Exp_Type;
 
@@ -7156,7 +7168,7 @@
             --  Do not generate a 'reference in SPARK mode since the access
             --  type is not created in the first place.
 
-            if SPARK_Mode then
+            if GNATprove_Mode then
                New_Exp := E;
 
             --  Otherwise generate reference, marking the value as non-null
Index: lib-writ.adb
===================================================================
--- lib-writ.adb	(revision 206790)
+++ lib-writ.adb	(working copy)
@@ -841,7 +841,7 @@
               --  files, which are required to compute frame conditions
               --  of subprograms.
 
-              or else SPARK_Mode
+              or else GNATprove_Mode
             then
                Write_Info_Tab (25);
 
@@ -973,9 +973,10 @@
 
       --  If we are not generating code, and there is an up to date ALI file
       --  file accessible, read it, and acquire the compilation arguments from
-      --  this file.
+      --  this file. In GNATprove mode, always generate the ALI file, which
+      --  contains a special section for formal verification.
 
-      if Operating_Mode /= Generate_Code then
+      if Operating_Mode /= Generate_Code and then not GNATprove_Mode then
          if Up_To_Date_ALI_File_Exists then
             Update_Tables_From_ALI_File;
             return;
@@ -1488,7 +1489,7 @@
 
       --  Output SPARK cross-reference information if needed
 
-      if Opt.Xref_Active and then SPARK_Mode then
+      if Opt.Xref_Active and then GNATprove_Mode then
          SPARK_Specific.Collect_SPARK_Xrefs (Sdep_Table => Sdep_Table,
                                              Num_Sdep   => Num_Sdep);
          SPARK_Specific.Output_SPARK_Xrefs;
Index: ali-util.adb
===================================================================
--- ali-util.adb	(revision 206790)
+++ ali-util.adb	(working copy)
@@ -274,11 +274,11 @@
                      Error_Msg ("{ had errors, must be fixed, and recompiled");
                      Set_Name_Table_Info (Afile, Int (No_Unit_Id));
 
-                  --  In formal verification mode, object files are never
-                  --  generated, so No_Object=True is not considered an error.
+                  --  In GNATprove mode, object files are never generated, so
+                  --  No_Object=True is not considered an error.
 
                   elsif ALIs.Table (Idread).No_Object
-                    and then not SPARK_Mode
+                    and then not GNATprove_Mode
                     and then not Ignore_Errors
                   then
                      Error_Msg_File_1 := Withs.Table (W).Sfile;
Index: sem_prag.adb
===================================================================
--- sem_prag.adb	(revision 206790)
+++ sem_prag.adb	(working copy)
@@ -4556,7 +4556,7 @@
             --  N_Contract node.
 
             if Acts_As_Spec (PO)
-              and then (SPARK_Mode or Formal_Extensions)
+              and then (GNATprove_Mode or Formal_Extensions)
             then
                declare
                   Prag : constant Node_Id := New_Copy_Tree (N);
@@ -4596,7 +4596,7 @@
             --  where there is no later point at which the aspect will be
             --  analyzed.
 
-            if SPARK_Mode or else ASIS_Mode then
+            if GNATprove_Mode or else ASIS_Mode then
                Analyze_Pre_Post_Condition_In_Decl_Part
                  (N, Defining_Entity (Unit (Parent (PO))));
             end if;
@@ -8345,7 +8345,9 @@
          --  user code: we want to generate checks for analysis purposes, as
          --  set respectively by -gnatC and -gnatd.F
 
-         if (CodePeer_Mode or SPARK_Mode) and then Comes_From_Source (N) then
+         if (CodePeer_Mode or GNATprove_Mode)
+           and then Comes_From_Source (N)
+         then
             return;
          end if;
 
@@ -13700,7 +13702,7 @@
             --  in these modes.
 
             if not Restriction_Active (No_Initialize_Scalars)
-              and then not (CodePeer_Mode or SPARK_Mode)
+              and then not (CodePeer_Mode or GNATprove_Mode)
             then
                Init_Or_Norm_Scalars := True;
                Initialize_Scalars := True;
@@ -13819,7 +13821,7 @@
             --  Pragma always active unless in CodePeer or SPARK mode, since
             --  this causes walk order issues.
 
-            if not (CodePeer_Mode or SPARK_Mode) then
+            if not (CodePeer_Mode or GNATprove_Mode) then
                Process_Inline (Enabled);
             end if;
 
@@ -15460,7 +15462,7 @@
             --  incorrect negative results in SPARK mode, so ignore this pragma
             --  in these modes.
 
-            if not (CodePeer_Mode or SPARK_Mode) then
+            if not (CodePeer_Mode or GNATprove_Mode) then
                Normalize_Scalars := True;
                Init_Or_Norm_Scalars := True;
             end if;
@@ -15921,7 +15923,7 @@
                   --  complex front-end expansions related to pragma Pack,
                   --  so disable handling of pragma Pack in these cases.
 
-                  if CodePeer_Mode or SPARK_Mode then
+                  if CodePeer_Mode or GNATprove_Mode then
                      null;
 
                   --  Don't attempt any packing for VM targets. We possibly
Index: sem_ch12.adb
===================================================================
--- sem_ch12.adb	(revision 206790)
+++ sem_ch12.adb	(working copy)
@@ -3616,7 +3616,7 @@
 
          --  We instantiate the body if we are generating code, if we are
          --  generating cross-reference information, or if we are building
-         --  trees for ASIS use.
+         --  trees for ASIS use or GNATprove use.
 
          declare
             Enclosing_Body_Present : Boolean := False;
@@ -3724,7 +3724,7 @@
                 and then not Inline_Now
                 and then (Operating_Mode = Generate_Code
                            or else (Operating_Mode = Check_Semantics
-                                     and then ASIS_Mode));
+                                     and then (ASIS_Mode or GNATprove_Mode)));
 
             --  If front_end_inlining is enabled, do not instantiate body if
             --  within a generic context.
@@ -4390,17 +4390,18 @@
            or else Is_Inlined (Subp)
            or else Is_Inlined (Alias (Subp)))
 
-        --  Must be generating code or analyzing code in ASIS mode
+        --  Must be generating code or analyzing code in ASIS mode or GNATprove
+        --  mode.
 
         and then (Operating_Mode = Generate_Code
                    or else (Operating_Mode = Check_Semantics
-                             and then ASIS_Mode))
+                             and then (ASIS_Mode or GNATprove_Mode)))
 
         --  The body is needed when generating code (full expansion), in ASIS
-        --  mode for other tools, and in SPARK mode (special expansion) for
+        --  mode for other tools, and in GNATprove mode (special expansion) for
         --  formal verification of the body itself.
 
-        and then (Expander_Active or ASIS_Mode)
+        and then (Expander_Active or ASIS_Mode or GNATprove_Mode)
 
         --  No point in inlining if ABE is inevitable
 
Index: freeze.adb
===================================================================
--- freeze.adb	(revision 206790)
+++ freeze.adb	(working copy)
@@ -3280,7 +3280,7 @@
            --  general, neither CodePeer not GNATprove care about the
            --  internal representation of objects.
 
-           and then not (CodePeer_Mode or SPARK_Mode)
+           and then not (CodePeer_Mode or GNATprove_Mode)
          then
             --  If implicit packing enabled, do it
 
@@ -4230,7 +4230,7 @@
                     and then not Is_Limited_Composite (E)
                     and then not Is_Packed (Root_Type (E))
                     and then not Has_Component_Size_Clause (Root_Type (E))
-                    and then not (CodePeer_Mode or SPARK_Mode)
+                    and then not (CodePeer_Mode or GNATprove_Mode)
                   then
                      --  Compute number of elements in array
 
Index: sem_util.adb
===================================================================
--- sem_util.adb	(revision 206790)
+++ sem_util.adb	(working copy)
@@ -12802,7 +12802,7 @@
                --  In formal verification mode, keep track of all reads and
                --  writes through explicit dereferences.
 
-               if SPARK_Mode then
+               if GNATprove_Mode then
                   SPARK_Specific.Generate_Dereference (N, 'm');
                end if;
 
@@ -12897,11 +12897,12 @@
 
                --  Generate a reference only if the assignment comes from
                --  source. This excludes, for example, calls to a dispatching
-               --  assignment operation when the left-hand side is tagged.
+               --  assignment operation when the left-hand side is tagged. In
+               --  GNATprove mode, we need those references also on generated
+               --  code, as these are used to compute the local effects of
+               --  subprograms.
 
-               --  Why is SPARK mode different here ???
-
-               if Modification_Comes_From_Source or SPARK_Mode then
+               if Modification_Comes_From_Source or GNATprove_Mode then
                   Generate_Reference (Ent, Exp, 'm');
 
                   --  If the target of the assignment is the bound variable
Index: sem_res.adb
===================================================================
--- sem_res.adb	(revision 206790)
+++ sem_res.adb	(working copy)
@@ -1693,7 +1693,7 @@
       --  case of Ada 2012 constructs such as quantified expressions, which are
       --  expanded in two separate steps.
 
-      if SPARK_Mode then
+      if GNATprove_Mode then
          Analyze_And_Resolve (N, T);
       else
          Analyze_And_Resolve (N, T, Suppress => All_Checks);
@@ -4206,7 +4206,7 @@
               --  in scope at the point of reference, so the reference should
               --  be ignored for computing effects of subprograms.
 
-              and then not SPARK_Mode
+              and then not GNATprove_Mode
             then
                Set_Entity (Selector_Name (Parent (A)), F);
                Generate_Reference (F, Selector_Name (Parent (A)));
Index: expander.adb
===================================================================
--- expander.adb	(revision 206790)
+++ expander.adb	(working copy)
@@ -88,8 +88,9 @@
       --  The first is when are not generating code. In this mode the
       --  Full_Analysis flag indicates whether we are performing a complete
       --  analysis, in which case Full_Analysis = True or a pre-analysis in
-      --  which case Full_Analysis = False. See the spec of Sem for more
-      --  info on this.
+      --  which case Full_Analysis = False. See the spec of Sem for more info
+      --  on this. Additionally, the GNATprove_Mode flag indicates that a light
+      --  expansion for formal verification should be used.
       --
       --  The second reason for the Expander_Active flag to be False is that
       --  we are performing a pre-analysis. During pre-analysis all expansion
@@ -107,7 +108,7 @@
       --  given that the expansion actions that would normally process it will
       --  not take place. This prevents cascaded errors due to stack mismatch.
 
-      if not Expander_Active then
+      if not (Expander_Active or (Full_Analysis and GNATprove_Mode)) then
          Set_Analyzed (N, Full_Analysis);
 
          if Serious_Errors_Detected > 0
@@ -127,10 +128,11 @@
          Debug_A_Entry ("expanding  ", N);
 
          begin
-            --  In SPARK mode we only need a very limited subset of the usual
-            --  expansions. This limited subset is implemented in Expand_SPARK.
+            --  In GNATprove mode we only need a very limited subset of
+            --  the usual expansions. This limited subset is implemented
+            --  in Expand_SPARK.
 
-            if SPARK_Mode then
+            if GNATprove_Mode then
                Expand_SPARK (N);
 
             --  Here for normal non-SPARK mode
@@ -503,10 +505,10 @@
 
    procedure Expander_Mode_Restore is
    begin
-      --  Not active (has no effect) in ASIS mode (see comments in spec of
-      --  Expander_Mode_Save_And_Set).
+      --  Not active (has no effect) in ASIS and GNATprove modes (see comments
+      --  in spec of Expander_Mode_Save_And_Set).
 
-      if ASIS_Mode then
+      if ASIS_Mode or GNATprove_Mode then
          return;
       end if;
 
@@ -530,10 +532,10 @@
 
    procedure Expander_Mode_Save_And_Set (Status : Boolean) is
    begin
-      --  Not active (has no effect) in ASIS mode (see comments in spec of
-      --  Expander_Mode_Save_And_Set).
+      --  Not active (has no effect) in ASIS and GNATprove modes (see comments
+      --  in spec of Expander_Mode_Save_And_Set).
 
-      if ASIS_Mode then
+      if ASIS_Mode or GNATprove_Mode then
          return;
       end if;
 
Index: expander.ads
===================================================================
--- expander.ads	(revision 206790)
+++ expander.ads	(working copy)
@@ -6,7 +6,7 @@
 --                                                                          --
 --                                 S p e c                                  --
 --                                                                          --
---          Copyright (C) 1992-2008, Free Software Foundation, Inc.         --
+--          Copyright (C) 1992-2013, Free Software Foundation, Inc.         --
 --                                                                          --
 -- GNAT is free software;  you can  redistribute it  and/or modify it under --
 -- terms of the  GNU General Public License as published  by the Free Soft- --
@@ -150,18 +150,20 @@
    --  Saves the current setting of the Expander_Active flag on an internal
    --  stack and then sets the flag to the given value.
    --
-   --  Note: this routine has no effect in ASIS_Mode. In ASIS_Mode, all
-   --  expansion activity is always off, since we want the original semantic
-   --  tree for ASIS purposes without any expansion. This is achieved by
-   --  setting Expander_Active False in ASIS_Mode. In situations such as
-   --  the call to Instantiate_Bodies in Frontend, Expander_Mode_Save_And_Set
-   --  may be called to temporarily turn the expander on, but this will have
-   --  no effect in ASIS mode.
+   --  Note: this routine has no effect in ASIS and GNATprove modes. In ASIS
+   --  mode, all expansion activity is always off, since we want the original
+   --  semantic tree for ASIS purposes without any expansion. In GNATprove
+   --  mode, a very light expansion is performed on specific nodes. Both are
+   --  achieved by setting Expander_Active False in ASIS and GNATprove modes.
+   --  In situations such as the call to Instantiate_Bodies in Frontend,
+   --  Expander_Mode_Save_And_Set may be called to temporarily turn the
+   --  expander on, but this will have no effect in ASIS and GNATprove modes.
 
    procedure Expander_Mode_Restore;
    --  Restores the setting of the Expander_Active flag using the top entry
    --  pushed onto the stack by Expander_Mode_Save_And_Reset, popping the
-   --  stack, except that if any errors have been detected, then the state
-   --  of the flag is left set to False. Disabled for ASIS_Mode (see above).
+   --  stack, except that if any errors have been detected, then the state of
+   --  the flag is left set to False. Disabled for ASIS and GNATprove modes
+   --  (see above).
 
 end Expander;
Index: sem_attr.adb
===================================================================
--- sem_attr.adb	(revision 206790)
+++ sem_attr.adb	(working copy)
@@ -4499,7 +4499,7 @@
          --  not suffer from the out-of-order issue described above. Thus, this
          --  expansion is skipped in SPARK mode.
 
-         if not Is_Entity_Name (P) and then not SPARK_Mode then
+         if not Is_Entity_Name (P) and then not GNATprove_Mode then
             P_Type := Base_Type (P_Type);
             Set_Etype (N, P_Type);
             Set_Etype (P, P_Type);
Index: exp_dbug.adb
===================================================================
--- exp_dbug.adb	(revision 206790)
+++ exp_dbug.adb	(working copy)
@@ -1314,7 +1314,7 @@
       --  name as being qualified, as Qualify_Entity_Name may be called more
       --  than once on the same entity.
 
-      elsif SPARK_Mode then
+      elsif GNATprove_Mode then
          if Has_Homonym (Ent) then
             Get_Name_String (Chars (Ent));
             Append_Homonym_Number (Ent);
Index: gnat1drv.adb
===================================================================
--- gnat1drv.adb	(revision 206790)
+++ gnat1drv.adb	(working copy)
@@ -299,15 +299,16 @@
          Formal_Extensions := True;
       end if;
 
-      --  Enable SPARK_Mode when using -gnatd.F switch
+      --  Enable GNATprove_Mode when using -gnatd.F switch
 
       if Debug_Flag_Dot_FF then
-         SPARK_Mode := True;
+         GNATprove_Mode := True;
       end if;
 
-      --  SPARK_Mode is also activated by default in the gnat2why executable
+      --  GNATprove_Mode is also activated by default in the gnat2why
+      --  executable.
 
-      if SPARK_Mode then
+      if GNATprove_Mode then
 
          --  Set strict standard interpretation of compiler permissions
 
@@ -384,11 +385,10 @@
 
          Polling_Required := False;
 
-         --  Set operating mode to Generate_Code, but full front-end expansion
-         --  is not desirable in SPARK mode, so a light expansion is performed
-         --  instead.
+         --  Set operating mode to Check_Semantics, but a light front-end
+         --  expansion is still performed.
 
-         Operating_Mode := Generate_Code;
+         Operating_Mode := Check_Semantics;
 
          --  Skip call to gigi
 
@@ -1054,17 +1054,13 @@
       elsif CodePeer_Mode then
          Back_End_Mode := Generate_Object;
 
-      --  It is not an error to analyze in SPARK mode a spec which requires a
-      --  body, when the body is not available. During frame condition
+      --  It is not an error to analyze in GNATprove mode a spec which requires
+      --  a body, when the body is not available. During frame condition
       --  generation, the corresponding ALI file is generated. During
       --  translation to Why, Why code is generated for the spec.
 
-      elsif SPARK_Mode then
-         if Frame_Condition_Mode then
-            Back_End_Mode := Declarations_Only;
-         else
-            Back_End_Mode := Generate_Object;
-         end if;
+      elsif GNATprove_Mode then
+         Back_End_Mode := Declarations_Only;
 
       --  In all other cases (specs which have bodies, generics, and bodies
       --  where subunits are missing), we cannot generate code and we generate
@@ -1168,10 +1164,11 @@
       --  since representations are largely symbolic there.
 
       if Back_End_Mode = Declarations_Only
-        and then (not (Back_Annotate_Rep_Info or Generate_SCIL)
-                   or else Main_Kind = N_Subunit
-                   or else Targparm.Frontend_Layout_On_Target
-                   or else Targparm.VM_Target /= No_VM)
+           and then
+         (not (Back_Annotate_Rep_Info or Generate_SCIL or GNATprove_Mode)
+           or else Main_Kind = N_Subunit
+           or else Targparm.Frontend_Layout_On_Target
+           or else Targparm.VM_Target /= No_VM)
       then
          Sem_Ch13.Validate_Unchecked_Conversions;
          Sem_Ch13.Validate_Address_Clauses;
Index: errout.adb
===================================================================
--- errout.adb	(revision 206790)
+++ errout.adb	(working copy)
@@ -239,7 +239,7 @@
       --  an error status. These errors are handled in the driver of the
       --  verification process instead.
 
-      elsif SPARK_Mode and not Frame_Condition_Mode then
+      elsif GNATprove_Mode and not Frame_Condition_Mode then
          return False;
 
       else
@@ -2970,7 +2970,7 @@
          --  Suppress "size too small" errors in CodePeer mode and SPARK mode,
          --  since pragma Pack is also ignored in these configurations.
 
-         if CodePeer_Mode or SPARK_Mode then
+         if CodePeer_Mode or GNATprove_Mode then
             return True;
 
          --  When a size is wrong for a frozen type there is no explicit size
Index: sem_ch4.adb
===================================================================
--- sem_ch4.adb	(revision 206790)
+++ sem_ch4.adb	(working copy)
@@ -1823,7 +1823,7 @@
       --  In formal verification mode, keep track of all reads and writes
       --  through explicit dereferences.
 
-      if SPARK_Mode then
+      if GNATprove_Mode then
          SPARK_Specific.Generate_Dereference (N);
       end if;
 
@@ -4613,7 +4613,7 @@
                      --  In SPARK mode, this is made into an error to simplify
                      --  the processing of the formal verification backend.
 
-                     if SPARK_Mode then
+                     if GNATprove_Mode then
                         Apply_Compile_Time_Constraint_Error
                           (N, "component not present in }",
                            CE_Discriminant_Check_Failed,
Index: restrict.adb
===================================================================
--- restrict.adb	(revision 206790)
+++ restrict.adb	(working copy)
@@ -538,7 +538,7 @@
       --  set in gnat1drv.adb so that we have consistency between each
       --  compilation.
 
-      if CodePeer_Mode or SPARK_Mode then
+      if CodePeer_Mode or GNATprove_Mode then
          return;
       end if;
 
Index: sem_ch6.adb
===================================================================
--- sem_ch6.adb	(revision 206790)
+++ sem_ch6.adb	(working copy)
@@ -1151,7 +1151,7 @@
          --  prepares the contract assertions for generic subprograms or for
          --  ASIS. Do not generate contract checks in SPARK mode.
 
-         if not SPARK_Mode then
+         if not GNATprove_Mode then
             Expand_Subprogram_Contract (N, Gen_Id, Body_Id);
          end if;
 
@@ -3188,7 +3188,7 @@
       --  prepares the contract assertions for generic subprograms or for ASIS.
       --  Do not generate contract checks in SPARK mode.
 
-      if not SPARK_Mode then
+      if not GNATprove_Mode then
          Expand_Subprogram_Contract (N, Spec_Id, Body_Id);
       end if;
 
Index: sem_ch8.adb
===================================================================
--- sem_ch8.adb	(revision 206790)
+++ sem_ch8.adb	(working copy)
@@ -5079,7 +5079,7 @@
 
             if Is_Object (E)
               and then Present (Renamed_Object (E))
-              and then not SPARK_Mode
+              and then not GNATprove_Mode
             then
                Generate_Reference (E, N);
 
Index: opt.adb
===================================================================
--- opt.adb	(revision 206790)
+++ opt.adb	(working copy)
@@ -44,7 +44,7 @@
 
    function Full_Expander_Active return Boolean is
    begin
-      return Expander_Active and not SPARK_Mode;
+      return Expander_Active;
    end Full_Expander_Active;
 
    ----------------------------------
Index: opt.ads
===================================================================
--- opt.ads	(revision 206790)
+++ opt.ads	(working copy)
@@ -1996,7 +1996,7 @@
    -----------------------------------
 
    Frame_Condition_Mode : Boolean := False;
-   --  Specific mode to be used in combination with SPARK_Mode. If set to
+   --  Specific mode to be used in combination with GNATprove_Mode. If set to
    --  true, ALI files containing the frame conditions (global effects) are
    --  generated, and Why files are *not* generated. If not true, Why files
    --  are generated. Set by debug flag -gnatd.G.
@@ -2010,7 +2010,7 @@
    --  The mode applicable to the whole compilation. The global mode can be set
    --  in a configuration file such as gnat.adc.
 
-   SPARK_Mode : Boolean := False;
+   GNATprove_Mode : Boolean := False;
    --  Specific compiling mode targeting formal verification through the
    --  generation of Why code for those parts of the input code that belong to
    --  the SPARK 2014 subset of Ada. Set True by the gnat2why executable or by
Index: adabkend.adb
===================================================================
--- adabkend.adb	(revision 206790)
+++ adabkend.adb	(working copy)
@@ -235,12 +235,12 @@
                if Is_Switch (Argv) then
                   Fail ("Object file name missing after -gnatO");
 
-               --  In SPARK_Mode, such an object file is never written, and the
-               --  call to Set_Output_Object_File_Name may fail (e.g. when the
-               --  object file name does not have the expected suffix). So we
-               --  skip that call when SPARK_Mode is set.
+               --  In GNATprove_Mode, such an object file is never written, and
+               --  the call to Set_Output_Object_File_Name may fail (e.g. when
+               --  the object file name does not have the expected suffix). So
+               --  we skip that call when GNATprove_Mode is set.
 
-               elsif SPARK_Mode then
+               elsif GNATprove_Mode then
                   Output_File_Name_Seen := True;
 
                else
Index: sem_ch13.adb
===================================================================
--- sem_ch13.adb	(revision 206790)
+++ sem_ch13.adb	(working copy)
@@ -2718,7 +2718,7 @@
                      Prepend (Aitem,
                        Visible_Declarations (Specification (N)));
 
-                  elsif Nkind (N) =  N_Package_Instantiation then
+                  elsif Nkind (N) = N_Package_Instantiation then
                      declare
                         Spec : constant Node_Id :=
                                  Specification (Instance_Spec (N));
Index: lib-xref.adb
===================================================================
--- lib-xref.adb	(revision 206790)
+++ lib-xref.adb	(working copy)
@@ -644,7 +644,7 @@
             --  in SPARK mode when the related context comes from an instance.
 
            or else
-             (SPARK_Mode
+             (GNATprove_Mode
                 and then In_Extended_Main_Code_Unit (N)
                 and then (Typ = 'm' or else Typ = 'r' or else Typ = 's'))
          then
@@ -899,7 +899,7 @@
          and then
            (Instantiation_Location (Sloc (N)) = No_Location
              or else Typ = 'i'
-             or else SPARK_Mode)
+             or else GNATprove_Mode)
 
         --  Ignore dummy references
 
@@ -986,7 +986,7 @@
          --  the renaming, which is needed to compute a valid set of effects
          --  (reads, writes) for the enclosing subprogram.
 
-         if SPARK_Mode then
+         if GNATprove_Mode then
             Ent := Get_Through_Renamings (Ent);
 
             --  If no enclosing object, then it could be a reference to any
@@ -1015,7 +1015,7 @@
             Actual_Typ := 'P';
          end if;
 
-         if SPARK_Mode then
+         if GNATprove_Mode then
             Ref := Sloc (Nod);
             Def := Sloc (Ent);
 


More information about the Gcc-patches mailing list