Patchwork [Ada] Suppress expansion related to tasking and tagged types in Alfa mode

login
register
mail settings
Submitter Arnaud Charlet
Date Aug. 29, 2011, 1:21 p.m.
Message ID <20110829132152.GA8396@adacore.com>
Download mbox | patch
Permalink /patch/112047/
State New
Headers show

Comments

Arnaud Charlet - Aug. 29, 2011, 1:21 p.m.
Alfa mode for formal verification currently does no deal with tasking and
tagged types. Suppress expansion of these features to simplify input to
formal verification back-end.

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

2011-08-29  Yannick Moy  <moy@adacore.com>

	* exp_ch13.adb (Expand_N_Freeze_Entity): Do nothing in Alfa mode.
	* exp_ch9.adb: Do not expand tasking constructs in Alfa mode.
	* gnat1drv.adb (Adjust_Global_Switches): Suppress the expansion of
	tagged types and dispatching calls in Alfa mode.

Patch

Index: exp_ch9.adb
===================================================================
--- exp_ch9.adb	(revision 178195)
+++ exp_ch9.adb	(working copy)
@@ -5290,6 +5290,12 @@ 
       Tasknm : Node_Id;
 
    begin
+      --  Do not expand tasking constructs in formal verification mode
+
+      if ALFA_Mode then
+         return;
+      end if;
+
       Aggr := Make_Aggregate (Loc, Component_Associations => New_List);
       Count := 0;
 
@@ -5421,6 +5427,12 @@ 
    --  Start of processing for Expand_N_Accept_Statement
 
    begin
+      --  Do not expand tasking constructs in formal verification mode
+
+      if ALFA_Mode then
+         return;
+      end if;
+
       --  If accept statement is not part of a list, then its parent must be
       --  an accept alternative, and, as described above, we do not do any
       --  expansion for such accept statements at this level.
@@ -5871,6 +5883,12 @@ 
       T   : Entity_Id;  --  Additional status flag
 
    begin
+      --  Do not expand tasking constructs in formal verification mode
+
+      if ALFA_Mode then
+         return;
+      end if;
+
       Process_Statements_For_Controlled_Objects (Trig);
       Process_Statements_For_Controlled_Objects (Abrt);
 
@@ -6820,6 +6838,12 @@ 
       S : Entity_Id;  --  Primitive operation slot
 
    begin
+      --  Do not expand tasking constructs in formal verification mode
+
+      if ALFA_Mode then
+         return;
+      end if;
+
       Process_Statements_For_Controlled_Objects (N);
 
       if Ada_Version >= Ada_2005
@@ -7136,6 +7160,12 @@ 
    procedure Expand_N_Delay_Relative_Statement (N : Node_Id) is
       Loc : constant Source_Ptr := Sloc (N);
    begin
+      --  Do not expand tasking constructs in formal verification mode
+
+      if ALFA_Mode then
+         return;
+      end if;
+
       Rewrite (N,
         Make_Procedure_Call_Statement (Loc,
           Name => New_Reference_To (RTE (RO_CA_Delay_For), Loc),
@@ -7155,6 +7185,12 @@ 
       Typ : Entity_Id;
 
    begin
+      --  Do not expand tasking constructs in formal verification mode
+
+      if ALFA_Mode then
+         return;
+      end if;
+
       if Is_RTE (Base_Type (Etype (Expression (N))), RO_CA_Time) then
          Typ := RTE (RO_CA_Delay_Until);
       else
@@ -7175,6 +7211,12 @@ 
 
    procedure Expand_N_Entry_Body (N : Node_Id) is
    begin
+      --  Do not expand tasking constructs in formal verification mode
+
+      if ALFA_Mode then
+         return;
+      end if;
+
       --  Associate discriminals with the next protected operation body to be
       --  expanded.
 
@@ -7196,6 +7238,12 @@ 
       Index   : Node_Id;
 
    begin
+      --  Do not expand tasking constructs in formal verification mode
+
+      if ALFA_Mode then
+         return;
+      end if;
+
       if No_Run_Time_Mode then
          Error_Msg_CRT ("entry call", N);
          return;
@@ -7252,6 +7300,12 @@ 
       Acc_Ent    : Entity_Id;
 
    begin
+      --  Do not expand tasking constructs in formal verification mode
+
+      if ALFA_Mode then
+         return;
+      end if;
+
       Formal := First_Formal (Entry_Ent);
       Last_Decl := N;
 
@@ -7520,6 +7574,12 @@ 
    --  Start of processing for Expand_N_Protected_Body
 
    begin
+      --  Do not expand tasking constructs in formal verification mode
+
+      if ALFA_Mode then
+         return;
+      end if;
+
       if No_Run_Time_Mode then
          Error_Msg_CRT ("protected body", N);
          return;
@@ -7870,6 +7930,12 @@ 
    --  Start of processing for Expand_N_Protected_Type_Declaration
 
    begin
+      --  Do not expand tasking constructs in formal verification mode
+
+      if ALFA_Mode then
+         return;
+      end if;
+
       if Present (Corresponding_Record_Type (Prot_Typ)) then
          return;
       else
@@ -9072,6 +9138,12 @@ 
    --  Start of processing for Expand_N_Requeue_Statement
 
    begin
+      --  Do not expand tasking constructs in formal verification mode
+
+      if ALFA_Mode then
+         return;
+      end if;
+
       --  Extract the components of the entry call
 
       Extract_Entry (N, Concval, Ename, Index);
@@ -9658,6 +9730,12 @@ 
    --  Start of processing for Expand_N_Selective_Accept
 
    begin
+      --  Do not expand tasking constructs in formal verification mode
+
+      if ALFA_Mode then
+         return;
+      end if;
+
       Process_Statements_For_Controlled_Objects (N);
 
       --  First insert some declarations before the select. The first is:
@@ -10288,6 +10366,12 @@ 
       --  Used to determine the proper location of wrapper body insertions
 
    begin
+      --  Do not expand tasking constructs in formal verification mode
+
+      if ALFA_Mode then
+         return;
+      end if;
+
       --  Add renaming declarations for discriminals and a declaration for the
       --  entry family index (if applicable).
 
@@ -10493,6 +10577,12 @@ 
       Decl_Stack : Node_Id;
 
    begin
+      --  Do not expand tasking constructs in formal verification mode
+
+      if ALFA_Mode then
+         return;
+      end if;
+
       --  If already expanded, nothing to do
 
       if Present (Corresponding_Record_Type (Tasktyp)) then
@@ -11034,6 +11124,12 @@ 
       S : Entity_Id;  --  Primitive operation slot
 
    begin
+      --  Do not expand tasking constructs in formal verification mode
+
+      if ALFA_Mode then
+         return;
+      end if;
+
       --  Under the Ravenscar profile, timed entry calls are excluded. An error
       --  was already reported on spec, so do not attempt to expand the call.
 
Index: gnat1drv.adb
===================================================================
--- gnat1drv.adb	(revision 178186)
+++ gnat1drv.adb	(working copy)
@@ -455,14 +455,18 @@ 
 
          Reset_Style_Check_Options;
 
-         --  Suppress compiler warnings, since what we are
-         --  interested in here is what formal verification can find out.
+         --  Suppress compiler warnings, since what we are interested in here
+         --  is what formal verification can find out.
 
          Warning_Mode := Suppress;
 
          --  Suppress the generation of name tables for enumerations
 
          Global_Discard_Names := True;
+
+         --  Suppress the expansion of tagged types and dispatching calls
+
+         Tagged_Type_Expansion := False;
       end if;
    end Adjust_Global_Switches;
 
Index: exp_ch13.adb
===================================================================
--- exp_ch13.adb	(revision 178183)
+++ exp_ch13.adb	(working copy)
@@ -307,6 +307,13 @@ 
       Delete         : Boolean := False;
 
    begin
+      --  In formal verification mode, do not generate useless and confusing
+      --  expansion for freeze nodes.
+
+      if ALFA_Mode then
+         return;
+      end if;
+
       --  If there are delayed aspect specifications, we insert them just
       --  before the freeze node. They are already analyzed so we don't need
       --  to reanalyze them (they were analyzed before the type was frozen),