From patchwork Thu Nov 30 10:19:16 2023 Content-Type: text/plain; charset="utf-8" MIME-Version: 1.0 Content-Transfer-Encoding: 7bit X-Patchwork-Submitter: =?utf-8?q?Marc_Poulhi=C3=A8s?= X-Patchwork-Id: 81019 Return-Path: X-Original-To: patchwork@sourceware.org Delivered-To: patchwork@sourceware.org Received: from server2.sourceware.org (localhost [IPv6:::1]) by sourceware.org (Postfix) with ESMTP id 315E9383CA80 for ; Thu, 30 Nov 2023 10:21:29 +0000 (GMT) X-Original-To: gcc-patches@gcc.gnu.org Delivered-To: gcc-patches@gcc.gnu.org Received: from mail-wr1-x430.google.com (mail-wr1-x430.google.com [IPv6:2a00:1450:4864:20::430]) by sourceware.org (Postfix) with ESMTPS id 185913861882 for ; Thu, 30 Nov 2023 10:19:19 +0000 (GMT) DMARC-Filter: OpenDMARC Filter v1.4.2 sourceware.org 185913861882 Authentication-Results: sourceware.org; dmarc=pass (p=none dis=none) header.from=adacore.com Authentication-Results: sourceware.org; spf=pass smtp.mailfrom=adacore.com ARC-Filter: OpenARC Filter v1.0.0 sourceware.org 185913861882 Authentication-Results: server2.sourceware.org; arc=none smtp.remote-ip=2a00:1450:4864:20::430 ARC-Seal: i=1; a=rsa-sha256; d=sourceware.org; s=key; t=1701339563; cv=none; b=GZFwtqh6+LJ1Y2p3TDHq+j2p0PN1cnb86JoSXVkn88jb/l5z6aY5WIF6R/CRpznMXK1YyOCReR7ON3Y532lEgzoZDXeCxzWFZeh51CS7MI2rxbAopVSjWcmwYg8d4XV4vMg0Zn23thVfDq8GYsxTlJKLEMGf/EpKWAFaMMpzsus= ARC-Message-Signature: i=1; a=rsa-sha256; d=sourceware.org; s=key; t=1701339563; c=relaxed/simple; bh=ar0grNkE47686yAZ3u+rroxkOraF+hrkfhsu+vxOcPM=; h=DKIM-Signature:From:To:Subject:Date:Message-ID:MIME-Version; b=oyRMPfY2cJVYz35AJTXKUD93rqTDHKUIECFJReVqyINimYj8A9WhopPuEF4UXgI0MoMLNhJ04XYwP46HjbGAIp/0OS+OawkO32JyvE1TvfDAmNQWiHjqNWLKEgb3/B3VlLYpGma0DmOFm3ZjR4AC8SH3yAG+r0tpzt+ZH1oKCys= ARC-Authentication-Results: i=1; server2.sourceware.org Received: by mail-wr1-x430.google.com with SMTP id ffacd0b85a97d-332f90a375eso500107f8f.3 for ; Thu, 30 Nov 2023 02:19:19 -0800 (PST) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=adacore.com; s=google; t=1701339558; x=1701944358; darn=gcc.gnu.org; h=content-transfer-encoding:mime-version:message-id:date:subject:cc :to:from:from:to:cc:subject:date:message-id:reply-to; bh=ZfOhA38iNifQC2bvmSpv3YJ3gqWhdJt1qYpaKjwQkUg=; b=ckwJmy8ydVluVWDyjibmVG6urq94iU4RvI6lZlBv2bYnrVb2P50E24e0zWf2e3XiVu c9zTyQUQegf524FnKZ/KVxDGE5EejI/SKbsG5TvaVxNrfryQ/0Tum2J6NFOp3S4s8PUj I7UXfx6t16jyqfmqht4wTufm/maj6jmwQxUc3T7oxHhrgT/U7jViC8vaBirBWTnkIQ9f MW/pYgbeZSZiHf8iQA4vv1RtsV688ae5T/eDIUPjfCsBwexsr5AlRqLPNhLCGiVJVSXG wulxvW33Y0KJV/LG8uAV09sCXzdp1d0KCMAeSSJSoO0ErvUbARRWGsLpsGEj/ST0cGTD OTQQ== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20230601; t=1701339558; x=1701944358; h=content-transfer-encoding:mime-version:message-id:date:subject:cc :to:from:x-gm-message-state:from:to:cc:subject:date:message-id :reply-to; bh=ZfOhA38iNifQC2bvmSpv3YJ3gqWhdJt1qYpaKjwQkUg=; b=jmB5Q0BOZgb2q6X4InQlXoMJNd6MvGqEr+CnQLI8B0G+rKCfPQdw05xi/9nVmWQ5uD 9NzTZntpjYUlYQFpRvfv9OQpMgwVn3FCwdLj9FKLk9Gv29o2iQ4JtYUJy2Fd3GDBCioe YGH/u/LbtfDZS4VMDQkbX3q1KdJ0DsaylbOOIV4gc5wNcFuG9g6/jJ7Pt7j2snYDANeu gUnqC7xbr1Yx1RYmF2+YysbFGXy2Ril4nLnVotw+LTRCmGyerq7uCMI7h9TZOg9hibwb MythbqOqZMxyxU4bClPKYW7PliR4dFpE3Ba6XLj7PGPgK191AjNOwik4CG7enVJVvJr3 Wm8Q== X-Gm-Message-State: AOJu0YyolIqL/Yn1smK5bMjwvcAXlmEuBgtOOzxnYmbDUTPn01nQVLFq IyYHfw48L+kknFhKX4675ultxOf3HxddcOeBSDOwwg== X-Google-Smtp-Source: AGHT+IFrzx4W0piBf10hpUfVk1UFwSmGJJoUJ9qCMxb6BPeQ+4JmlYPMgo0KHU0vhzPdpGe8B1B08w== X-Received: by 2002:a5d:52cc:0:b0:332:fa7e:a8a6 with SMTP id r12-20020a5d52cc000000b00332fa7ea8a6mr9538840wrv.38.1701339557500; Thu, 30 Nov 2023 02:19:17 -0800 (PST) Received: from poulhies-Precision-5550.telnowedge.local (lmontsouris-659-1-24-67.w81-250.abo.wanadoo.fr. [81.250.175.67]) by smtp.gmail.com with ESMTPSA id r4-20020adff104000000b003313e4dddecsm1112920wro.108.2023.11.30.02.19.16 (version=TLS1_3 cipher=TLS_AES_256_GCM_SHA384 bits=256/256); Thu, 30 Nov 2023 02:19:16 -0800 (PST) From: =?utf-8?q?Marc_Poulhi=C3=A8s?= To: gcc-patches@gcc.gnu.org Cc: Yannick Moy Subject: [COMMITTED] ada: Remove SPARK legality checks Date: Thu, 30 Nov 2023 11:19:16 +0100 Message-ID: <20231130101916.3094439-1-poulhies@adacore.com> X-Mailer: git-send-email 2.42.0 MIME-Version: 1.0 X-Spam-Status: No, score=-13.3 required=5.0 tests=BAYES_00, DKIM_SIGNED, DKIM_VALID, DKIM_VALID_AU, DKIM_VALID_EF, GIT_PATCH_0, KAM_ASCII_DIVIDERS, RCVD_IN_DNSWL_NONE, SPF_HELO_NONE, SPF_PASS, TXREP, T_SCC_BODY_TEXT_LINE autolearn=ham autolearn_force=no version=3.4.6 X-Spam-Checker-Version: SpamAssassin 3.4.6 (2021-04-09) on server2.sourceware.org X-BeenThere: gcc-patches@gcc.gnu.org X-Mailman-Version: 2.1.30 Precedence: list List-Id: Gcc-patches mailing list List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , Errors-To: gcc-patches-bounces+patchwork=sourceware.org@gcc.gnu.org From: Yannick Moy SPARK legality checks apply only to code with SPARK_Mode On, and are performed again in GNATprove for detecting SPARK-compatible declarations in code with SPARK_Mode Auto. Remove this duplication, to only perform SPARK legality checking in GNATprove. After this patch, only a few special SPARK legality checks are performed in the frontend, which could be moved to GNATprove later. gcc/ada/ * contracts.adb (Analyze_Entry_Or_Subprogram_Body_Contract): Remove checking on volatility. Remove handling of SPARK_Mode, not needed anymore. (Analyze_Entry_Or_Subprogram_Contract): Remove checking on volatility. (Check_Type_Or_Object_External_Properties): Same. (Analyze_Object_Contract): Same. * freeze.adb (Freeze_Record_Type): Same. Also remove checking on synchronized types and ghost types. * sem_ch12.adb (Instantiate_Object): Remove checking on volatility. (Instantiate_Type): Same. * sem_ch3.adb (Access_Type_Declaration): Same. (Derived_Type_Declaration): Remove checking related to untagged partial view. (Process_Discriminants): Remove checking on volatility. * sem_ch5.adb (Analyze_Loop_Parameter_Specification): Same. * sem_ch6.adb (Analyze_Procedure_Call): Fix use of SPARK_Mode where GNATprove_Mode was intended. * sem_disp.adb (Inherited_Subprograms): Protect against Empty node. * sem_prag.adb (Analyze_Global_In_Decl_Part): Remove checking on volatility. (Analyze_Pragma): Same. * sem_res.adb (Flag_Effectively_Volatile_Objects): Remove. (Resolve_Actuals): Remove checking on volatility. (Resolve_Entity_Name): Same. * sem_util.adb (Check_Nonvolatile_Function_Profile): Remove. (Check_Volatility_Compatibility): Remove. * sem_util.ads: Same. Tested on x86_64-pc-linux-gnu, committed on master. --- gcc/ada/contracts.adb | 163 ++---------------------------------------- gcc/ada/freeze.adb | 71 ------------------ gcc/ada/sem_ch12.adb | 37 ---------- gcc/ada/sem_ch3.adb | 56 --------------- gcc/ada/sem_ch5.adb | 8 --- gcc/ada/sem_ch6.adb | 4 +- gcc/ada/sem_disp.adb | 1 + gcc/ada/sem_prag.adb | 80 --------------------- gcc/ada/sem_res.adb | 95 ------------------------ gcc/ada/sem_util.adb | 124 +------------------------------- gcc/ada/sem_util.ads | 19 +---- 11 files changed, 13 insertions(+), 645 deletions(-) diff --git a/gcc/ada/contracts.adb b/gcc/ada/contracts.adb index b6e756fbf77..fa0d59a246a 100644 --- a/gcc/ada/contracts.adb +++ b/gcc/ada/contracts.adb @@ -590,10 +590,6 @@ package body Contracts is Items : constant Node_Id := Contract (Body_Id); Spec_Id : constant Entity_Id := Unique_Defining_Entity (Body_Decl); - Saved_SM : constant SPARK_Mode_Type := SPARK_Mode; - Saved_SMP : constant Node_Id := SPARK_Mode_Pragma; - -- Save the SPARK_Mode-related data to restore on exit - begin -- When a subprogram body declaration is illegal, its defining entity is -- left unanalyzed. There is nothing left to do in this case because the @@ -628,39 +624,11 @@ package body Contracts is Analyze_Entry_Or_Subprogram_Contract (Corresponding_Spec (Body_Decl)); end if; - -- Due to the timing of contract analysis, delayed pragmas may be - -- subject to the wrong SPARK_Mode, usually that of the enclosing - -- context. To remedy this, restore the original SPARK_Mode of the - -- related subprogram body. - - Set_SPARK_Mode (Body_Id); - -- Ensure that the contract cases or postconditions mention 'Result or -- define a post-state. Check_Result_And_Post_State (Body_Id); - -- A stand-alone nonvolatile function body cannot have an effectively - -- volatile formal parameter or return type (SPARK RM 7.1.3(9)). This - -- check is relevant only when SPARK_Mode is on, as it is not a standard - -- legality rule. The check is performed here because Volatile_Function - -- is processed after the analysis of the related subprogram body. The - -- check only applies to source subprograms and not to generated TSS - -- subprograms. - - if SPARK_Mode = On - and then Ekind (Body_Id) in E_Function | E_Generic_Function - and then Comes_From_Source (Spec_Id) - and then not Is_Volatile_Function (Body_Id) - then - Check_Nonvolatile_Function_Profile (Body_Id); - end if; - - -- Restore the SPARK_Mode of the enclosing context after all delayed - -- pragmas have been analyzed. - - Restore_SPARK_Mode (Saved_SM, Saved_SMP); - -- Capture all global references in a generic subprogram body now that -- the contract has been analyzed. @@ -865,20 +833,6 @@ package body Contracts is Check_Result_And_Post_State (Subp_Id); end if; - -- A nonvolatile function cannot have an effectively volatile formal - -- parameter or return type (SPARK RM 7.1.3(9)). This check is relevant - -- only when SPARK_Mode is on, as it is not a standard legality rule. - -- The check is performed here because pragma Volatile_Function is - -- processed after the analysis of the related subprogram declaration. - - if SPARK_Mode = On - and then Ekind (Subp_Id) in E_Function | E_Generic_Function - and then Comes_From_Source (Subp_Id) - and then not Is_Volatile_Function (Subp_Id) - then - Check_Nonvolatile_Function_Profile (Subp_Id); - end if; - -- Restore the SPARK_Mode of the enclosing context after all delayed -- pragmas have been analyzed. @@ -902,19 +856,16 @@ package body Contracts is (Type_Or_Obj_Id : Entity_Id) is Is_Type_Id : constant Boolean := Is_Type (Type_Or_Obj_Id); - Decl_Kind : constant String := - (if Is_Type_Id then "type" else "object"); -- Local variables - AR_Val : Boolean := False; - AW_Val : Boolean := False; - ER_Val : Boolean := False; - EW_Val : Boolean := False; - NC_Val : Boolean; - Seen : Boolean := False; - Prag : Node_Id; - Obj_Typ : Entity_Id; + AR_Val : Boolean := False; + AW_Val : Boolean := False; + ER_Val : Boolean := False; + EW_Val : Boolean := False; + NC_Val : Boolean; + Seen : Boolean := False; + Prag : Node_Id; -- Start of processing for Check_Type_Or_Object_External_Properties @@ -922,8 +873,6 @@ package body Contracts is -- Analyze all external properties if Is_Type_Id then - Obj_Typ := Type_Or_Obj_Id; - -- If the parent type of a derived type is volatile -- then the derived type inherits volatility-related flags. @@ -940,8 +889,6 @@ package body Contracts is end if; end; end if; - else - Obj_Typ := Etype (Type_Or_Obj_Id); end if; Prag := Get_Pragma (Type_Or_Obj_Id, Pragma_Async_Readers); @@ -1027,96 +974,6 @@ package body Contracts is if Present (Prag) then Analyze_External_Property_In_Decl_Part (Prag, NC_Val); end if; - - -- The following checks are relevant only when SPARK_Mode is on, as - -- they are not standard Ada legality rules. Internally generated - -- temporaries are ignored, as well as return objects. - - if SPARK_Mode = On - and then Comes_From_Source (Type_Or_Obj_Id) - and then not Is_Return_Object (Type_Or_Obj_Id) - then - if Is_Effectively_Volatile (Type_Or_Obj_Id) then - - -- The declaration of an effectively volatile object or type must - -- appear at the library level (SPARK RM 7.1.3(3), C.6(6)). - - if not Is_Library_Level_Entity (Type_Or_Obj_Id) then - Error_Msg_Code := GEC_Volatile_At_Library_Level; - Error_Msg_N - ("effectively volatile " - & Decl_Kind - & " & must be declared at library level '[[]']", - Type_Or_Obj_Id); - - -- An object of a discriminated type cannot be effectively - -- volatile except for protected objects (SPARK RM 7.1.3(5)). - - elsif Has_Discriminants (Obj_Typ) - and then not Is_Protected_Type (Obj_Typ) - then - Error_Msg_N - ("discriminated " & Decl_Kind & " & cannot be volatile", - Type_Or_Obj_Id); - end if; - - -- An object decl shall be compatible with respect to volatility - -- with its type (SPARK RM 7.1.3(2)). - - if not Is_Type_Id then - if Is_Effectively_Volatile (Obj_Typ) then - Check_Volatility_Compatibility - (Type_Or_Obj_Id, Obj_Typ, - "volatile object", "its type", - Srcpos_Bearer => Type_Or_Obj_Id); - end if; - - -- A component of a composite type (in this case, the composite - -- type is an array type) shall be compatible with respect to - -- volatility with the composite type (SPARK RM 7.1.3(6)). - - elsif Is_Array_Type (Obj_Typ) then - Check_Volatility_Compatibility - (Component_Type (Obj_Typ), Obj_Typ, - "component type", "its enclosing array type", - Srcpos_Bearer => Obj_Typ); - - -- A component of a composite type (in this case, the composite - -- type is a record type) shall be compatible with respect to - -- volatility with the composite type (SPARK RM 7.1.3(6)). - - elsif Is_Record_Type (Obj_Typ) then - declare - Comp : Entity_Id := First_Component (Obj_Typ); - begin - while Present (Comp) loop - Check_Volatility_Compatibility - (Etype (Comp), Obj_Typ, - "record component " & Get_Name_String (Chars (Comp)), - "its enclosing record type", - Srcpos_Bearer => Comp); - Next_Component (Comp); - end loop; - end; - end if; - - -- The type or object is not effectively volatile - - else - -- A non-effectively volatile type cannot have effectively - -- volatile components (SPARK RM 7.1.3(6)). - - if Is_Type_Id - and then not Is_Effectively_Volatile (Type_Or_Obj_Id) - and then Has_Effectively_Volatile_Component (Type_Or_Obj_Id) - then - Error_Msg_N - ("non-volatile type & cannot have effectively volatile" - & " components", - Type_Or_Obj_Id); - end if; - end if; - end if; end Check_Type_Or_Object_External_Properties; ----------------------------- @@ -1263,12 +1120,6 @@ package body Contracts is if Yields_Synchronized_Object (Obj_Typ) then Error_Msg_N ("ghost object & cannot be synchronized", Obj_Id); - -- A Ghost object cannot be effectively volatile (SPARK RM 6.9(7) and - -- SPARK RM 6.9(19)). - - elsif SPARK_Mode = On and then Is_Effectively_Volatile (Obj_Id) then - Error_Msg_N ("ghost object & cannot be volatile", Obj_Id); - -- A Ghost object cannot be imported or exported (SPARK RM 6.9(7)). -- One exception to this is the object that represents the dispatch -- table of a Ghost tagged type, as the symbol needs to be exported. diff --git a/gcc/ada/freeze.adb b/gcc/ada/freeze.adb index 4a5dd5311bb..26b5589a020 100644 --- a/gcc/ada/freeze.adb +++ b/gcc/ada/freeze.adb @@ -5689,77 +5689,6 @@ package body Freeze is end if; end if; - -- The following checks are relevant only when SPARK_Mode is on as - -- they are not standard Ada legality rules. - - if SPARK_Mode = On then - - -- A discriminated type cannot be effectively volatile - -- (SPARK RM 7.1.3(5)). - - if Is_Effectively_Volatile (Rec) then - if Has_Discriminants (Rec) then - Error_Msg_N ("discriminated type & cannot be volatile", Rec); - end if; - - -- A non-effectively volatile record type cannot contain - -- effectively volatile components (SPARK RM 7.1.3(6)). - - else - Comp := First_Component (Rec); - while Present (Comp) loop - if Comes_From_Source (Comp) - and then Is_Effectively_Volatile (Etype (Comp)) - then - Error_Msg_Name_1 := Chars (Rec); - Error_Msg_N - ("component & of non-volatile type % cannot be " - & "volatile", Comp); - end if; - - Next_Component (Comp); - end loop; - end if; - - -- A type which does not yield a synchronized object cannot have - -- a component that yields a synchronized object (SPARK RM 9.5). - - if not Yields_Synchronized_Object (Rec) then - Comp := First_Component (Rec); - while Present (Comp) loop - if Comes_From_Source (Comp) - and then Yields_Synchronized_Object (Etype (Comp)) - then - Error_Msg_Name_1 := Chars (Rec); - Error_Msg_N - ("component & of non-synchronized type % cannot be " - & "synchronized", Comp); - end if; - - Next_Component (Comp); - end loop; - end if; - - -- A Ghost type cannot have a component of protected or task type - -- (SPARK RM 6.9(19)). - - if Is_Ghost_Entity (Rec) then - Comp := First_Component (Rec); - while Present (Comp) loop - if Comes_From_Source (Comp) - and then Is_Concurrent_Type (Etype (Comp)) - then - Error_Msg_Name_1 := Chars (Rec); - Error_Msg_N - ("component & of ghost type % cannot be concurrent", - Comp); - end if; - - Next_Component (Comp); - end loop; - end if; - end if; - -- Make sure that if we have an iterator aspect, then we have -- either Constant_Indexing or Variable_Indexing. diff --git a/gcc/ada/sem_ch12.adb b/gcc/ada/sem_ch12.adb index ea85e88d753..5db9754f81d 100644 --- a/gcc/ada/sem_ch12.adb +++ b/gcc/ada/sem_ch12.adb @@ -11526,19 +11526,6 @@ package body Sem_Ch12 is Actual); end if; - -- Check actual/formal compatibility with respect to the four - -- volatility refinement aspects. - - declare - Actual_Obj : constant Entity_Id := - Get_Enclosing_Deep_Object (Actual); - begin - Check_Volatility_Compatibility - (Actual_Obj, A_Gen_Obj, "actual object", - "its corresponding formal object of mode in out", - Srcpos_Bearer => Actual); - end; - -- The actual for a ghost generic formal IN OUT parameter should be a -- ghost object (SPARK RM 6.9(14)). @@ -11746,22 +11733,6 @@ package body Sem_Ch12 is ("actual must exclude null to match generic formal#", Actual); end if; - -- An effectively volatile object cannot be used as an actual in a - -- generic instantiation (SPARK RM 7.1.3(7)). The following check is - -- relevant only when SPARK_Mode is on as it is not a standard Ada - -- legality rule, and also verifies that the actual is an object. - - if SPARK_Mode = On - and then Present (Actual) - and then Is_Object_Reference (Actual) - and then Is_Effectively_Volatile_Object (Actual) - and then not Is_Effectively_Volatile (A_Gen_Obj) - then - Error_Msg_N - ("volatile object cannot act as actual in generic instantiation", - Actual); - end if; - return List; end Instantiate_Object; @@ -12944,14 +12915,6 @@ package body Sem_Ch12 is ("actual for& must have Independent_Components specified", Actual, A_Gen_T); end if; - - -- Check actual/formal compatibility with respect to the four - -- volatility refinement aspects. - - Check_Volatility_Compatibility - (Act_T, A_Gen_T, - "actual type", "its corresponding formal type", - Srcpos_Bearer => Actual); end if; end Check_Shared_Variable_Control_Aspects; diff --git a/gcc/ada/sem_ch3.adb b/gcc/ada/sem_ch3.adb index aed7828752b..96fd16dc171 100644 --- a/gcc/ada/sem_ch3.adb +++ b/gcc/ada/sem_ch3.adb @@ -1442,26 +1442,6 @@ package body Sem_Ch3 is end if; Set_Etype (T, T); - - -- For SPARK, check that the designated type is compatible with - -- respect to volatility with the access type. - - if SPARK_Mode /= Off - and then Comes_From_Source (T) - then - -- ??? UNIMPLEMENTED - -- In the case where the designated type is incomplete at this - -- point, performing this check here is harmless but the check - -- will need to be repeated when the designated type is complete. - - -- The preceding call to Comes_From_Source is needed because the - -- FE sometimes introduces implicitly declared access types. See, - -- for example, the expansion of nested_po.ads in OA28-015. - - Check_Volatility_Compatibility - (Full_Desig, T, "designated type", "access type", - Srcpos_Bearer => T); - end if; end if; -- If the type has appeared already in a with_type clause, it is frozen @@ -17337,29 +17317,6 @@ package body Sem_Ch3 is begin Parent_Type := Find_Type_Of_Subtype_Indic (Indic); - if SPARK_Mode = On - and then Is_Tagged_Type (Parent_Type) - then - declare - Partial_View : constant Entity_Id := - Incomplete_Or_Partial_View (Parent_Type); - - begin - -- If the partial view was not found then the parent type is not - -- a private type. Otherwise check if the partial view is a tagged - -- private type. - - if Present (Partial_View) - and then Is_Private_Type (Partial_View) - and then not Is_Tagged_Type (Partial_View) - then - Error_Msg_NE - ("cannot derive from & declared as untagged private " - & "(SPARK RM 3.4(1))", N, Partial_View); - end if; - end; - end if; - -- Ada 2005 (AI-251): In case of interface derivation check that the -- parent is also an interface. @@ -21014,19 +20971,6 @@ package body Sem_Ch3 is end if; end if; - -- A discriminant cannot be effectively volatile (SPARK RM 7.1.3(4)). - -- This check is relevant only when SPARK_Mode is on as it is not a - -- standard Ada legality rule. The only way for a discriminant to be - -- effectively volatile is to have an effectively volatile type, so - -- we check this directly, because the Ekind of Discr might not be - -- set yet (to help preventing cascaded errors on derived types). - - if SPARK_Mode = On - and then Is_Effectively_Volatile (Discr_Type) - then - Error_Msg_N ("discriminant cannot be volatile", Discr); - end if; - Next (Discr); end loop; diff --git a/gcc/ada/sem_ch5.adb b/gcc/ada/sem_ch5.adb index de38ddf4fa8..43dee2b2b6f 100644 --- a/gcc/ada/sem_ch5.adb +++ b/gcc/ada/sem_ch5.adb @@ -3452,14 +3452,6 @@ package body Sem_Ch5 is if Present (Iterator_Filter (N)) then Preanalyze_And_Resolve (Iterator_Filter (N), Standard_Boolean); end if; - - -- A loop parameter cannot be effectively volatile (SPARK RM 7.1.3(4)). - -- This check is relevant only when SPARK_Mode is on as it is not a - -- standard Ada legality check. - - if SPARK_Mode = On and then Is_Effectively_Volatile (Id) then - Error_Msg_N ("loop parameter cannot be volatile", Id); - end if; end Analyze_Loop_Parameter_Specification; ---------------------------- diff --git a/gcc/ada/sem_ch6.adb b/gcc/ada/sem_ch6.adb index 8ee75783d48..da6f6c40c92 100644 --- a/gcc/ada/sem_ch6.adb +++ b/gcc/ada/sem_ch6.adb @@ -1753,11 +1753,11 @@ package body Sem_Ch6 is and then Ekind (Entity (Selector_Name (P))) in E_Entry | E_Function | E_Procedure then - -- When front-end inlining is enabled, as with SPARK_Mode, a call + -- When front-end inlining is enabled, as with GNATprove mode, a call -- in prefix notation may still be missing its controlling argument, -- so perform the transformation now. - if SPARK_Mode = On and then In_Inlined_Body then + if GNATprove_Mode and then In_Inlined_Body then declare Subp : constant Entity_Id := Entity (Selector_Name (P)); Typ : constant Entity_Id := Etype (Prefix (P)); diff --git a/gcc/ada/sem_disp.adb b/gcc/ada/sem_disp.adb index ab7bc40978a..6975f4a4afa 100644 --- a/gcc/ada/sem_disp.adb +++ b/gcc/ada/sem_disp.adb @@ -2581,6 +2581,7 @@ package body Sem_Disp is loop Parent_Op := Overridden_Operation (Parent_Op); exit when No (Parent_Op) + or else No (Find_DT (Parent_Op)) or else (No_Interfaces and then Is_Interface (Find_DT (Parent_Op))); diff --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb index bd1d9d3d59b..9d66fb71a06 100644 --- a/gcc/ada/sem_prag.adb +++ b/gcc/ada/sem_prag.adb @@ -2827,21 +2827,6 @@ package body Sem_Prag is SPARK_Msg_N ("\use its constituents instead", Item); return; - -- An external state which has Async_Writers or - -- Effective_Reads enabled cannot appear as a global item - -- of a nonvolatile function (SPARK RM 7.1.3(8)). - - elsif Is_External_State (Item_Id) - and then (Async_Writers_Enabled (Item_Id) - or else Effective_Reads_Enabled (Item_Id)) - and then Ekind (Spec_Id) in E_Function | E_Generic_Function - and then not Is_Volatile_Function (Spec_Id) - then - SPARK_Msg_NE - ("external state & cannot act as global item of " - & "nonvolatile function", Item, Item_Id); - return; - -- If the reference to the abstract state appears in an -- enclosing package body that will eventually refine the -- state, record the reference for future checks. @@ -2894,50 +2879,6 @@ package body Sem_Prag is Item, Item_Id); return; end if; - - -- Variable related checks. These are only relevant when - -- SPARK_Mode is on as they are not standard Ada legality - -- rules. - - elsif SPARK_Mode = On - and then Ekind (Item_Id) = E_Variable - and then Is_Effectively_Volatile_For_Reading (Item_Id) - then - -- The current instance of a protected unit is not an - -- effectively volatile object, unless the protected unit - -- is already volatile for another reason (SPARK RM 7.1.2). - - if Is_Single_Protected_Object (Item_Id) - and then Is_CCT_Instance (Etype (Item_Id), Spec_Id) - and then not Is_Effectively_Volatile_For_Reading - (Item_Id, Ignore_Protected => True) - then - null; - - -- An effectively volatile object for reading cannot appear - -- as a global item of a nonvolatile function (SPARK RM - -- 7.1.3(8)). - - elsif Ekind (Spec_Id) in E_Function | E_Generic_Function - and then not Is_Volatile_Function (Spec_Id) - then - Error_Msg_NE - ("volatile object & cannot act as global item of a " - & "function", Item, Item_Id); - return; - - -- An effectively volatile object with external property - -- Effective_Reads set to True must have mode Output or - -- In_Out (SPARK RM 7.1.3(10)). - - elsif Effective_Reads_Enabled (Item_Id) - and then Global_Mode = Name_Input - then - Error_Msg_NE - ("volatile object & with property Effective_Reads must " - & "have mode In_Out or Output", Item, Item_Id); - return; - end if; end if; -- When the item renames an entire object, replace the item @@ -8128,27 +8069,6 @@ package body Sem_Prag is Check_Full_Access_Only (E); end if; - -- The following check is only relevant when SPARK_Mode is on as - -- this is not a standard Ada legality rule. Pragma Volatile can - -- only apply to a full type declaration or an object declaration - -- (SPARK RM 7.1.3(2)). Original_Node is necessary to account for - -- untagged derived types that are rewritten as subtypes of their - -- respective root types. - - if SPARK_Mode = On - and then Prag_Id = Pragma_Volatile - and then Nkind (Original_Node (Decl)) not in - N_Full_Type_Declaration | - N_Formal_Type_Declaration | - N_Object_Declaration | - N_Single_Protected_Declaration | - N_Single_Task_Declaration - then - Error_Pragma_Arg - ("argument of pragma % must denote a full type or object " - & "declaration", Arg1); - end if; - -- Deal with the case where the pragma/attribute is applied to a type if Is_Type (E) then diff --git a/gcc/ada/sem_res.adb b/gcc/ada/sem_res.adb index 70a84176054..8e5d351141d 100644 --- a/gcc/ada/sem_res.adb +++ b/gcc/ada/sem_res.adb @@ -3620,10 +3620,6 @@ package body Sem_Res is -- interpretation, but the form of the actual can only be determined -- once the primitive operation is identified. - procedure Flag_Effectively_Volatile_Objects (Expr : Node_Id); - -- Emit an error concerning the illegal usage of an effectively volatile - -- object for reading in interfering context (SPARK RM 7.1.3(10)). - procedure Insert_Default; -- If the actual is missing in a call, insert in the actuals list -- an instance of the default expression. The insertion is always @@ -3874,68 +3870,6 @@ package body Sem_Res is end if; end Check_Prefixed_Call; - --------------------------------------- - -- Flag_Effectively_Volatile_Objects -- - --------------------------------------- - - procedure Flag_Effectively_Volatile_Objects (Expr : Node_Id) is - function Flag_Object (N : Node_Id) return Traverse_Result; - -- Determine whether arbitrary node N denotes an effectively volatile - -- object for reading and if it does, emit an error. - - ----------------- - -- Flag_Object -- - ----------------- - - function Flag_Object (N : Node_Id) return Traverse_Result is - Id : Entity_Id; - - begin - case Nkind (N) is - -- Do not consider nested function calls because they have - -- already been processed during their own resolution. - - when N_Function_Call => - return Skip; - - when N_Identifier | N_Expanded_Name => - Id := Entity (N); - - -- Identifiers of components and discriminants are not names - -- in the sense of Ada RM 4.1. They can only occur as a - -- selector_name in selected_component or as a choice in - -- component_association. - - if Present (Id) - and then Is_Object (Id) - and then Ekind (Id) not in E_Component | E_Discriminant - and then Is_Effectively_Volatile_For_Reading (Id) - and then - not Is_OK_Volatile_Context (Context => Parent (N), - Obj_Ref => N, - Check_Actuals => True) - then - Error_Msg_Code := GEC_Volatile_Non_Interfering_Context; - Error_Msg_N - ("volatile object cannot appear in this context '[[]']", - N); - end if; - - return Skip; - - when others => - return OK; - end case; - end Flag_Object; - - procedure Flag_Objects is new Traverse_Proc (Flag_Object); - - -- Start of processing for Flag_Effectively_Volatile_Objects - - begin - Flag_Objects (Expr); - end Flag_Effectively_Volatile_Objects; - -------------------- -- Insert_Default -- -------------------- @@ -5128,22 +5062,6 @@ package body Sem_Res is Check_Unset_Reference (A); end if; - -- The following checks are only relevant when SPARK_Mode is on as - -- they are not standard Ada legality rule. Internally generated - -- temporaries are ignored. - - if SPARK_Mode = On and then Comes_From_Source (A) then - - -- Inspect the expression and flag each effectively volatile - -- object for reading as illegal because it appears within - -- an interfering context. Note that this is usually done - -- in Resolve_Entity_Name, but when the effectively volatile - -- object for reading appears as an actual in a call, the call - -- must be resolved first. - - Flag_Effectively_Volatile_Objects (A); - end if; - -- A formal parameter of a specific tagged type whose related -- subprogram is subject to pragma Extensions_Visible with value -- "False" cannot act as an actual in a subprogram with value @@ -8130,19 +8048,6 @@ package body Sem_Res is if SPARK_Mode = On then - -- An effectively volatile object for reading must appear in - -- non-interfering context (SPARK RM 7.1.3(10)). - - if Is_Object (E) - and then Is_Effectively_Volatile_For_Reading (E) - and then - not Is_OK_Volatile_Context (Par, N, Check_Actuals => False) - then - Error_Msg_Code := GEC_Volatile_Non_Interfering_Context; - SPARK_Msg_N - ("volatile object cannot appear in this context '[[]']", N); - end if; - -- Parameters of modes OUT or IN OUT of the subprogram shall not -- occur in the consequences of an exceptional contract unless -- they are either passed by reference or occur in the prefix diff --git a/gcc/ada/sem_util.adb b/gcc/ada/sem_util.adb index 9215fc7da6c..909f93da040 100644 --- a/gcc/ada/sem_util.adb +++ b/gcc/ada/sem_util.adb @@ -3795,36 +3795,6 @@ package body Sem_Util is end loop; end Check_Inherited_Nonoverridable_Aspects; - ---------------------------------------- - -- Check_Nonvolatile_Function_Profile -- - ---------------------------------------- - - procedure Check_Nonvolatile_Function_Profile (Func_Id : Entity_Id) is - Formal : Entity_Id; - - begin - -- Inspect all formal parameters - - Formal := First_Formal (Func_Id); - while Present (Formal) loop - if Is_Effectively_Volatile_For_Reading (Etype (Formal)) then - Error_Msg_NE - ("nonvolatile function & cannot have a volatile parameter", - Formal, Func_Id); - end if; - - Next_Formal (Formal); - end loop; - - -- Inspect the return type - - if Is_Effectively_Volatile_For_Reading (Etype (Func_Id)) then - Error_Msg_NE - ("nonvolatile function & cannot have a volatile return type", - Result_Definition (Parent (Func_Id)), Func_Id); - end if; - end Check_Nonvolatile_Function_Profile; - ------------------- -- Check_Parents -- ------------------- @@ -5153,96 +5123,6 @@ package body Sem_Util is end if; end Check_Unused_Body_States; - ------------------------------------ - -- Check_Volatility_Compatibility -- - ------------------------------------ - - procedure Check_Volatility_Compatibility - (Id1, Id2 : Entity_Id; - Description_1, Description_2 : String; - Srcpos_Bearer : Node_Id) is - - begin - if SPARK_Mode /= On then - return; - end if; - - declare - AR1 : constant Boolean := Async_Readers_Enabled (Id1); - AW1 : constant Boolean := Async_Writers_Enabled (Id1); - ER1 : constant Boolean := Effective_Reads_Enabled (Id1); - EW1 : constant Boolean := Effective_Writes_Enabled (Id1); - AR2 : constant Boolean := Async_Readers_Enabled (Id2); - AW2 : constant Boolean := Async_Writers_Enabled (Id2); - ER2 : constant Boolean := Effective_Reads_Enabled (Id2); - EW2 : constant Boolean := Effective_Writes_Enabled (Id2); - - AR_Check_Failed : constant Boolean := AR1 and not AR2; - AW_Check_Failed : constant Boolean := AW1 and not AW2; - ER_Check_Failed : constant Boolean := ER1 and not ER2; - EW_Check_Failed : constant Boolean := EW1 and not EW2; - - package Failure_Description is - procedure Note_If_Failure - (Failed : Boolean; Aspect_Name : String); - -- If Failed is False, do nothing. - -- If Failed is True, add Aspect_Name to the failure description. - - function Failure_Text return String; - -- returns accumulated list of failing aspects - end Failure_Description; - - package body Failure_Description is - Description_Buffer : Bounded_String; - - --------------------- - -- Note_If_Failure -- - --------------------- - - procedure Note_If_Failure - (Failed : Boolean; Aspect_Name : String) is - begin - if Failed then - if Description_Buffer.Length /= 0 then - Append (Description_Buffer, ", "); - end if; - Append (Description_Buffer, Aspect_Name); - end if; - end Note_If_Failure; - - ------------------ - -- Failure_Text -- - ------------------ - - function Failure_Text return String is - begin - return +Description_Buffer; - end Failure_Text; - end Failure_Description; - - use Failure_Description; - begin - if AR_Check_Failed - or AW_Check_Failed - or ER_Check_Failed - or EW_Check_Failed - then - Note_If_Failure (AR_Check_Failed, "Async_Readers"); - Note_If_Failure (AW_Check_Failed, "Async_Writers"); - Note_If_Failure (ER_Check_Failed, "Effective_Reads"); - Note_If_Failure (EW_Check_Failed, "Effective_Writes"); - - Error_Msg_N - (Description_1 - & " and " - & Description_2 - & " are not compatible with respect to volatility due to " - & Failure_Text, - Srcpos_Bearer); - end if; - end; - end Check_Volatility_Compatibility; - ----------------- -- Choice_List -- ----------------- @@ -19326,7 +19206,7 @@ package body Sem_Util is -- An effectively volatile object may act as an actual when the -- corresponding formal is of a non-scalar effectively volatile - -- type (SPARK RM 7.1.3(10)). + -- type (SPARK RM 7.1.3(9)). if not Is_Scalar_Type (Etype (Formal)) and then Is_Effectively_Volatile_For_Reading (Etype (Formal)) @@ -19335,7 +19215,7 @@ package body Sem_Util is -- An effectively volatile object may act as an actual in a -- call to an instance of Unchecked_Conversion. (SPARK RM - -- 7.1.3(10)). + -- 7.1.3(9)). elsif Is_Unchecked_Conversion_Instance (Subp) then return True; diff --git a/gcc/ada/sem_util.ads b/gcc/ada/sem_util.ads index 2fae35b6bc4..081217a455a 100644 --- a/gcc/ada/sem_util.ads +++ b/gcc/ada/sem_util.ads @@ -415,10 +415,6 @@ package Sem_Util is -- In the error case, error message is associate with Inheritor; -- Inheritor parameter is otherwise unused. - procedure Check_Nonvolatile_Function_Profile (Func_Id : Entity_Id); - -- Verify that the profile of nonvolatile function Func_Id does not contain - -- effectively volatile parameters or return type for reading. - function Check_Parents (N : Node_Id; List : Elist_Id) return Boolean; -- Return True if all the occurrences of subtree N referencing entities in -- the given List have the right value in their Parent field. @@ -467,19 +463,6 @@ package Sem_Util is -- and the context is external to the protected operation, to warn against -- a possible unlocked access to data. - procedure Check_Volatility_Compatibility - (Id1, Id2 : Entity_Id; - Description_1, Description_2 : String; - Srcpos_Bearer : Node_Id); - -- Id1 and Id2 should each be the entity of a state abstraction, a - -- variable, or a type (i.e., something suitable for passing to - -- Async_Readers_Enabled and similar functions). - -- Does nothing if SPARK_Mode /= On. Otherwise, flags a legality violation - -- if one or more of the four volatility-related aspects is False for Id1 - -- and True for Id2. The two descriptions are included in the error message - -- text; the source position for the generated message is determined by - -- Srcpos_Bearer. - function Choice_List (N : Node_Id) return List_Id; -- Utility to retrieve the choices of a Component_Association or the -- Discrete_Choices of an Iterated_Component_Association. For various @@ -2199,7 +2182,7 @@ package Sem_Util is Obj_Ref : Node_Id; Check_Actuals : Boolean) return Boolean; -- Determine whether node Context denotes a "non-interfering context" (as - -- defined in SPARK RM 7.1.3(10)) where volatile reference Obj_Ref can + -- defined in SPARK RM 7.1.3(9)) where volatile reference Obj_Ref can -- safely reside. When examining references that might be located within -- actual parameters of a subprogram call that has not been resolved yet, -- Check_Actuals should be False; such references will be assumed to be