From patchwork Mon Aug 29 13:21:53 2011 Content-Type: text/plain; charset="utf-8" MIME-Version: 1.0 Content-Transfer-Encoding: 7bit X-Patchwork-Submitter: Arnaud Charlet X-Patchwork-Id: 112047 Return-Path: X-Original-To: incoming@patchwork.ozlabs.org Delivered-To: patchwork-incoming@bilbo.ozlabs.org Received: from sourceware.org (server1.sourceware.org [209.132.180.131]) by ozlabs.org (Postfix) with SMTP id 5A1DFB6F81 for ; Mon, 29 Aug 2011 23:22:12 +1000 (EST) Received: (qmail 9945 invoked by alias); 29 Aug 2011 13:22:10 -0000 Received: (qmail 9932 invoked by uid 22791); 29 Aug 2011 13:22:09 -0000 X-SWARE-Spam-Status: No, hits=-1.7 required=5.0 tests=AWL,BAYES_00,TW_KN X-Spam-Check-By: sourceware.org Received: from rock.gnat.com (HELO rock.gnat.com) (205.232.38.15) by sourceware.org (qpsmtpd/0.43rc1) with ESMTP; Mon, 29 Aug 2011 13:21:53 +0000 Received: from localhost (localhost.localdomain [127.0.0.1]) by filtered-rock.gnat.com (Postfix) with ESMTP id 2A8842BB136; Mon, 29 Aug 2011 09:21:53 -0400 (EDT) Received: from rock.gnat.com ([127.0.0.1]) by localhost (rock.gnat.com [127.0.0.1]) (amavisd-new, port 10024) with LMTP id dBjjZW+w-vO4; Mon, 29 Aug 2011 09:21:53 -0400 (EDT) Received: from kwai.gnat.com (kwai.gnat.com [205.232.38.4]) by rock.gnat.com (Postfix) with ESMTP id 15C1E2BAFEF; Mon, 29 Aug 2011 09:21:53 -0400 (EDT) Received: by kwai.gnat.com (Postfix, from userid 4192) id 0BFAF92A55; Mon, 29 Aug 2011 09:21:53 -0400 (EDT) Date: Mon, 29 Aug 2011 09:21:53 -0400 From: Arnaud Charlet To: gcc-patches@gcc.gnu.org Cc: Yannick Moy Subject: [Ada] Suppress expansion related to tasking and tagged types in Alfa mode Message-ID: <20110829132152.GA8396@adacore.com> MIME-Version: 1.0 Content-Disposition: inline User-Agent: Mutt/1.5.20 (2009-06-14) Mailing-List: contact gcc-patches-help@gcc.gnu.org; run by ezmlm Precedence: bulk List-Id: List-Unsubscribe: List-Archive: List-Post: List-Help: Sender: gcc-patches-owner@gcc.gnu.org Delivered-To: mailing list gcc-patches@gcc.gnu.org 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 * 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. 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),