From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Received: from mail-wm1-x32a.google.com (mail-wm1-x32a.google.com [IPv6:2a00:1450:4864:20::32a]) by sourceware.org (Postfix) with ESMTPS id C6E1D3849AEA for ; Fri, 17 May 2024 08:32:36 +0000 (GMT) DMARC-Filter: OpenDMARC Filter v1.4.2 sourceware.org C6E1D3849AEA Authentication-Results: sourceware.org; dmarc=pass (p=quarantine 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 C6E1D3849AEA Authentication-Results: server2.sourceware.org; arc=none smtp.remote-ip=2a00:1450:4864:20::32a ARC-Seal: i=1; a=rsa-sha256; d=sourceware.org; s=key; t=1715934776; cv=none; b=C5czaYmAgX6ERGqDb6asYpCYQaaPZ+ldrH7Gj7fEBOyVmAjszDy5JZIZ/w+GyOIkQYOXm/79QtOoxpi/ekSmuxZQITw+Vsf7kkHBzVUyT3WXZvqQMfcnoep5/qJ2hpW5jymocZN1bWAzOsONKOd00RLEyJ5ZXy3pOfCBmbUMRBE= ARC-Message-Signature: i=1; a=rsa-sha256; d=sourceware.org; s=key; t=1715934776; c=relaxed/simple; bh=MveXmIpqwEYebTb5T7dVwODj3uHv6oAWiXC2cgOfuN4=; h=DKIM-Signature:From:To:Subject:Date:Message-ID:MIME-Version; b=NySGz8t7vNASbUEMXa2ckbKKknfjkJvZ5kGCM+vguVs/RjBIBvzs5DcLdUKOh1dLifTHxd1c50+aKDJMu1glS/cJ0L4tb0DE9g246Y/vtaZgMX4mOig8Mq3DxAlJqBuuTljuUnI/unJl8qRnuShiAt4QgZi+bvoqiUhLuUAAg4w= ARC-Authentication-Results: i=1; server2.sourceware.org Received: by mail-wm1-x32a.google.com with SMTP id 5b1f17b1804b1-4202cea98daso9809985e9.0 for ; Fri, 17 May 2024 01:32:36 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=adacore.com; s=google; t=1715934755; x=1716539555; darn=gcc.gnu.org; h=content-transfer-encoding:mime-version:references:in-reply-to :message-id:date:subject:cc:to:from:from:to:cc:subject:date :message-id:reply-to; bh=bQZvcUu1vJUYUYyhCJocdbULl1b3f4Mg6hGjh4+MS80=; b=i9GS7Y7IRgAwqUGwdJQm/16aaFftPPWzXUER+u9mgRcastr8Kli/GsyalKJxb1cC5Y 0mjfrKGD0snXOa0x6b53ZfSUuW4Z1dGR7F58jXIdiPjBa+LxIm1TzFrvoIMf2RTgpyHr HnpsAkUupsz9fCIKU/ZcFZfeD4q8r2MZf0jbCEZHNbYozrR1YkL5Q4Odptk+11LG49VB TDIrax/HRGZPWT4JtqDSVUyNYyZCs3GzO+z3N5/WeG2eDFVLdkc0jGl4xS21TjiSTyZK qOjWDDQxWyOPzw3ajurOWGhsHhhd94xep9EM6yzWB88OOEQYyGk5YVa/GmoprlVzAklY LprQ== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20230601; t=1715934755; x=1716539555; h=content-transfer-encoding:mime-version:references:in-reply-to :message-id:date:subject:cc:to:from:x-gm-message-state:from:to:cc :subject:date:message-id:reply-to; bh=bQZvcUu1vJUYUYyhCJocdbULl1b3f4Mg6hGjh4+MS80=; b=qkEOEaHqn8hDIbh5yuNLVhXQDHmkIkiw/B4vFg/HU067L62V/rlDIEq7Vyk91Duj9d yf85fvtHLrQVb37YIRR3nUNSR8i3hItLpAVetyyNpa5kpBfs7pk2gOqe9G7eT+62+JCf zu+CEvqb2t3QFHIru4nJyFe8bRAwfNNG0OTdYTRD8DZ/brSr3Vy+iQpH20RHTczWWZ0k JquccZntiJ7Y8qjOd/3e2BLZz2geMdI4hMiD1h0xEWr/WWiU9CpspaRe6COk/N5xmcCN vasbqWdLdm5emrl2EUdiygWS4M35Xoh3sLDzgCvHKbsShqpA8G6ixtRdogbVeIApl4/q 6ucw== X-Gm-Message-State: AOJu0YyUTFz2Zq74DjKOSePv/uu8ciHEO4/2oAaoU5iEWdLPjLk3zJgG IZ5PMOBODos5deuH4Ot7mRNJ/cXTiFR6Vkry7BHBPT5e+pIJVzLH3Fqv75IPncjyzH0344qBktg = X-Google-Smtp-Source: AGHT+IHksWhW4iqbm5exPR/ttyj+DJtxdsmPQn+ZmAOwG6f2SBk1+O3/9NeVl02spnsCS8PKJVY7cA== X-Received: by 2002:a7b:cbcf:0:b0:416:7470:45ad with SMTP id 5b1f17b1804b1-41feaa43707mr184821565e9.17.1715934755423; Fri, 17 May 2024 01:32:35 -0700 (PDT) Received: from poulhies-Precision-5550.lan ([2001:861:3382:1a90:de37:8b1c:1f33:2610]) by smtp.gmail.com with ESMTPSA id 5b1f17b1804b1-420273cff03sm75197045e9.26.2024.05.17.01.32.34 (version=TLS1_3 cipher=TLS_AES_256_GCM_SHA384 bits=256/256); Fri, 17 May 2024 01:32:35 -0700 (PDT) From: =?UTF-8?q?Marc=20Poulhi=C3=A8s?= To: gcc-patches@gcc.gnu.org Cc: Piotr Trojanek Subject: [COMMITTED 20/35] ada: Expose utility routine for processing of Depends contracts in SPARK Date: Fri, 17 May 2024 10:31:52 +0200 Message-ID: <20240517083207.130391-20-poulhies@adacore.com> X-Mailer: git-send-email 2.43.2 In-Reply-To: <20240517083207.130391-1-poulhies@adacore.com> References: <20240517083207.130391-1-poulhies@adacore.com> MIME-Version: 1.0 Content-Transfer-Encoding: 8bit X-Spam-Status: No, score=-13.7 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 autolearn=ham autolearn_force=no version=3.4.6 X-Spam-Checker-Version: SpamAssassin 3.4.6 (2021-04-09) on server2.sourceware.org List-Id: From: Piotr Trojanek Routine Is_Unconstrained_Or_Tagged_Item is now used both in the GNAT frontend (for checking legality of Depends clauses) and in the GNATprove backend (for representing implicit inputs in flow graphs). gcc/ada/ * sem_prag.adb (Is_Unconstrained_Or_Tagged_Item): Move to Sem_Util, so it can be used from GNATprove. * sem_util.ads (Is_Unconstrained_Or_Tagged_Item): Move from Sem_Prag; spec. * sem_util.adb (Is_Unconstrained_Or_Tagged_Item): Move from Sem_Prag; body. Tested on x86_64-pc-linux-gnu, committed on master. --- gcc/ada/sem_prag.adb | 29 ----------------------------- gcc/ada/sem_util.adb | 23 +++++++++++++++++++++++ gcc/ada/sem_util.ads | 5 +++++ 3 files changed, 28 insertions(+), 29 deletions(-) diff --git a/gcc/ada/sem_prag.adb b/gcc/ada/sem_prag.adb index 02aad4d1caa..f27e40edcbb 100644 --- a/gcc/ada/sem_prag.adb +++ b/gcc/ada/sem_prag.adb @@ -280,12 +280,6 @@ package body Sem_Prag is -- Determine whether dependency clause Clause is surrounded by extra -- parentheses. If this is the case, issue an error message. - function Is_Unconstrained_Or_Tagged_Item (Item : Entity_Id) return Boolean; - -- Subsidiary to Collect_Subprogram_Inputs_Outputs and the analysis of - -- pragma Depends. Determine whether the type of dependency item Item is - -- tagged, unconstrained array, unconstrained private or unconstrained - -- record. - procedure Record_Possible_Body_Reference (State_Id : Entity_Id; Ref : Node_Id); @@ -32959,29 +32953,6 @@ package body Sem_Prag is and then List_Containing (N) = Private_Declarations (Parent (N)); end Is_Private_SPARK_Mode; - ------------------------------------- - -- Is_Unconstrained_Or_Tagged_Item -- - ------------------------------------- - - function Is_Unconstrained_Or_Tagged_Item - (Item : Entity_Id) return Boolean - is - Typ : constant Entity_Id := Etype (Item); - begin - if Is_Tagged_Type (Typ) then - return True; - - elsif Is_Array_Type (Typ) - or else Is_Record_Type (Typ) - or else Is_Private_Type (Typ) - then - return not Is_Constrained (Typ); - - else - return False; - end if; - end Is_Unconstrained_Or_Tagged_Item; - ----------------------------- -- Is_Valid_Assertion_Kind -- ----------------------------- diff --git a/gcc/ada/sem_util.adb b/gcc/ada/sem_util.adb index dd9f868b696..be777d26e46 100644 --- a/gcc/ada/sem_util.adb +++ b/gcc/ada/sem_util.adb @@ -20709,6 +20709,29 @@ package body Sem_Util is return T = Universal_Integer or else T = Universal_Real; end Is_Universal_Numeric_Type; + ------------------------------------- + -- Is_Unconstrained_Or_Tagged_Item -- + ------------------------------------- + + function Is_Unconstrained_Or_Tagged_Item + (Item : Entity_Id) return Boolean + is + Typ : constant Entity_Id := Etype (Item); + begin + if Is_Tagged_Type (Typ) then + return True; + + elsif Is_Array_Type (Typ) + or else Is_Record_Type (Typ) + or else Is_Private_Type (Typ) + then + return not Is_Constrained (Typ); + + else + return False; + end if; + end Is_Unconstrained_Or_Tagged_Item; + ------------------------------ -- Is_User_Defined_Equality -- ------------------------------ diff --git a/gcc/ada/sem_util.ads b/gcc/ada/sem_util.ads index 99c60ddf708..4fef8966380 100644 --- a/gcc/ada/sem_util.ads +++ b/gcc/ada/sem_util.ads @@ -2397,6 +2397,11 @@ package Sem_Util is pragma Inline (Is_Universal_Numeric_Type); -- True if T is Universal_Integer or Universal_Real + function Is_Unconstrained_Or_Tagged_Item (Item : Entity_Id) return Boolean; + -- Subsidiary to Collect_Subprogram_Inputs_Outputs and the analysis of + -- pragma Depends. Determine whether the type of dependency item Item is + -- tagged, unconstrained array or unconstrained record. + function Is_User_Defined_Equality (Id : Entity_Id) return Boolean; -- Determine whether an entity denotes a user-defined equality -- 2.43.2