From patchwork Tue Nov 28 09:38:29 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: 170644 Return-Path: Delivered-To: ouuuleilei@gmail.com Received: by 2002:a59:ce62:0:b0:403:3b70:6f57 with SMTP id o2csp3792245vqx; Tue, 28 Nov 2023 01:39:15 -0800 (PST) X-Google-Smtp-Source: AGHT+IE85FyIyBo3fa1ysmAZomIqX36dJgunrsszQIP8ixt7/jjFrJiFROKyE99KIeoyvlGuX6CE X-Received: by 2002:a05:620a:8d0e:b0:774:2c35:3796 with SMTP id rb14-20020a05620a8d0e00b007742c353796mr14489686qkn.34.1701164355777; Tue, 28 Nov 2023 01:39:15 -0800 (PST) ARC-Seal: i=2; a=rsa-sha256; t=1701164355; cv=pass; d=google.com; s=arc-20160816; b=NQBgzJQ1xHg73UQcwqdKuk6XmCvjiGFyWgSGZLa1LNAX7oeaUu1X/2Ysm3SFqbhoMk 2UHcGbs4uzmr7CntKV4IX+TJUY81Y7cZB/dvtxVQoF9YTFxnmH8LOD0yDjN9LybaCStv MaKB4clTNqD/eQqyPbXgDkQWliTR0Cd66KnCr4h/mZZ04CZsol07gRLEyvjyV1FVmNtH XPlgVscTAptXRRPCl3/qhWWNMlJ2/mt4C8FGi0TENIHP5RdZ8ohvk+JUs8lPB3OH7Nlt SwVx10GEIhtzu5/z0LSPCk+0jMokZFKgwMdyXgH2SHbOd6zen9B+/aSmVeSBdRYlPtkB YDgg== ARC-Message-Signature: i=2; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=errors-to:list-subscribe:list-help:list-post:list-archive :list-unsubscribe:list-id:precedence:content-transfer-encoding :mime-version:message-id:date:subject:cc:to:from:dkim-signature :arc-filter:dmarc-filter:delivered-to; bh=TauflELMEhb4gKyshoeiF1uUQSYF6B091pDolZf5dNA=; fh=xkXw4ZjwHxuTwIHh5BpbVWFYGO+bP8cUYTTqcq/2BVI=; b=w5INckcrFKLt3//ksI7BBnbUqtqiZ3QbF1+O9/rhMp33qD1DquaOb4Vqy8btqwl+7i OFKtFl4AF8fLTwOY0Qt2sRcMgGirpjgHGsbDu8XVb/ZcEl47he6RRARFScfeZc2jufbw IxBcWVbGxAOoOtGR/Xs4+aK2mKazH5kHSlzh3I21qHWUdkTrwsffi6uom8RxdJxNuz7v XQd7iavriJ+5pAkOAvQXmCf/NCta2tWAwBmIVEf+fhB/5TdSRWkZ+YnfxX+BR1sMNQZF Y4ed/jGzJ4A2ABmbcg/9ikSyuEXv8qDvHy7eMFSrNlfpUJaptwOlS2+o+/bNDS+jc6E6 7SsA== ARC-Authentication-Results: i=2; mx.google.com; dkim=pass header.i=@adacore.com header.s=google header.b=JVYmpCPn; arc=pass (i=1); spf=pass (google.com: domain of gcc-patches-bounces+ouuuleilei=gmail.com@gcc.gnu.org designates 2620:52:3:1:0:246e:9693:128c as permitted sender) smtp.mailfrom="gcc-patches-bounces+ouuuleilei=gmail.com@gcc.gnu.org"; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=adacore.com Received: from server2.sourceware.org (server2.sourceware.org. [2620:52:3:1:0:246e:9693:128c]) by mx.google.com with ESMTPS id x20-20020a05620a0ed400b0077dbf723ceesi720563qkm.439.2023.11.28.01.39.15 for (version=TLS1_3 cipher=TLS_AES_256_GCM_SHA384 bits=256/256); Tue, 28 Nov 2023 01:39:15 -0800 (PST) Received-SPF: pass (google.com: domain of gcc-patches-bounces+ouuuleilei=gmail.com@gcc.gnu.org designates 2620:52:3:1:0:246e:9693:128c as permitted sender) client-ip=2620:52:3:1:0:246e:9693:128c; Authentication-Results: mx.google.com; dkim=pass header.i=@adacore.com header.s=google header.b=JVYmpCPn; arc=pass (i=1); spf=pass (google.com: domain of gcc-patches-bounces+ouuuleilei=gmail.com@gcc.gnu.org designates 2620:52:3:1:0:246e:9693:128c as permitted sender) smtp.mailfrom="gcc-patches-bounces+ouuuleilei=gmail.com@gcc.gnu.org"; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=adacore.com Received: from server2.sourceware.org (localhost [IPv6:::1]) by sourceware.org (Postfix) with ESMTP id 8138B394741E for ; Tue, 28 Nov 2023 09:39:08 +0000 (GMT) X-Original-To: gcc-patches@gcc.gnu.org Delivered-To: gcc-patches@gcc.gnu.org Received: from mail-ot1-x32a.google.com (mail-ot1-x32a.google.com [IPv6:2607:f8b0:4864:20::32a]) by sourceware.org (Postfix) with ESMTPS id 69AA0394741B for ; Tue, 28 Nov 2023 09:38:42 +0000 (GMT) DMARC-Filter: OpenDMARC Filter v1.4.2 sourceware.org 69AA0394741B 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 69AA0394741B Authentication-Results: server2.sourceware.org; arc=none smtp.remote-ip=2607:f8b0:4864:20::32a ARC-Seal: i=1; a=rsa-sha256; d=sourceware.org; s=key; t=1701164324; cv=none; b=UNsSw1LRvzpuSDtfFD3TMEYlgp0cvuHcq10fPDIVatZgJHKapCrAf0JjGiXHNpQX/DrynOt7zOdVgelp162JhjAmy2GP2Mxp5XTFuv4py5no09qKpAfxKFQGaPwEoM3F/xV9b9bh0LLwYGvjjtPCcrmEBG1VUZdhC3VSEMsaCtE= ARC-Message-Signature: i=1; a=rsa-sha256; d=sourceware.org; s=key; t=1701164324; c=relaxed/simple; bh=jpXKmr59UHlnfFv2YWGC+GuU8ZaaKyYU3QJaCfl/4Cw=; h=DKIM-Signature:From:To:Subject:Date:Message-ID:MIME-Version; b=Cdgc/tsq5kiBqmtk92feP8O1XRvkWUkGomsx3pw3Q3oB6OarJj649Ex+GLAcK+XmEZWbPspPDrY38D+7pT2mABKxqk8STPUEv5YgkawyFEzj4ISVBc0RwJcsIlSG7BoYYSeP2WDUrw4ApWj17tSXWxYXZWE/VyuKBClvJY698fo= ARC-Authentication-Results: i=1; server2.sourceware.org Received: by mail-ot1-x32a.google.com with SMTP id 46e09a7af769-6d7f3a4bbc6so3028857a34.2 for ; Tue, 28 Nov 2023 01:38:42 -0800 (PST) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=adacore.com; s=google; t=1701164321; x=1701769121; 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=TauflELMEhb4gKyshoeiF1uUQSYF6B091pDolZf5dNA=; b=JVYmpCPnkD8u0kZVE5RjliuIZG6Me+w/u/q58NZh4rX4CVRFAO3UElyqC+uurnDDrj gUDl14pW4w6cnciPOsKKrZTNSxuNJlFLaFAqcGaufLCF/N/DYVwfqIECjMq3pSTtuJyR EXFcVNkpaFE8H9QhCWaFouKNu0wdev99BMat/WXzuNg0RbPLHrGeoiAah3f84bd649vz ogfSdJecsq+Yrubjq67xe00T2+Byj7md85k3BYErqqY91Eyq5MQnITiV2SNstD7ytG1k X1K8PiTxM8WBxIUIxj048Oon+1wmxeonL3zC5d+TwKMVnMligF7ELIa47WWXAYmZO2XL UWLQ== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20230601; t=1701164321; x=1701769121; 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=TauflELMEhb4gKyshoeiF1uUQSYF6B091pDolZf5dNA=; b=J/OcxOGG0hxKG5VAW1OK8Rat6WwYrGlCbSrBUb1SlPQqb15fVf5jrLr7e6cuyJm+rc vDL1ctktSApbdKk+RuVV2tsjlXdvrV5nkshipomVWJDejNgV5zdW9RpANXbyOZtwnGuf Z7gAnJifo9IMLQxPGa90QZQa5lgyzYSXNBcYSo4b7nh8y3cxF2guUWjuRnDJ4forbARe MecVjT2M6wH2DUlz7uyXTSoCwJwlBTejbuZKfWpLuZ14DivdD9bbbgfrwQ1ELZiq+9Ov P227ZXZvQUKC5QyW7cBaBIf3SrBzsJWFefYDmCbb+GkYPrvv9e7iWdsMXP2c5WlJE1ho +WJg== X-Gm-Message-State: AOJu0Yyd/QF9Su28CZtJUM09K2//Q/XoGR/XMTFftfx5eTkOi58VmPnq SPg7RRhbSjuBiQRCLmqgGqoUFxxtcRs/EsIuFmPvjw== X-Received: by 2002:a05:6870:390b:b0:1fa:3e47:5a8e with SMTP id b11-20020a056870390b00b001fa3e475a8emr9295719oap.5.1701164321557; Tue, 28 Nov 2023 01:38:41 -0800 (PST) Received: from localhost.localdomain ([2001:861:3382:1a90:a24b:a65f:9576:c701]) by smtp.gmail.com with ESMTPSA id j7-20020aa78007000000b006900cb919b8sm8383826pfi.53.2023.11.28.01.38.39 (version=TLS1_3 cipher=TLS_AES_256_GCM_SHA384 bits=256/256); Tue, 28 Nov 2023 01:38:41 -0800 (PST) From: =?utf-8?q?Marc_Poulhi=C3=A8s?= To: gcc-patches@gcc.gnu.org Cc: Yannick Moy Subject: [COMMITTED] ada: Remove dependency on System.Val_Bool in System.Img_Bool Date: Tue, 28 Nov 2023 10:38:29 +0100 Message-ID: <20231128093829.2970640-1-poulhies@adacore.com> X-Mailer: git-send-email 2.42.0 MIME-Version: 1.0 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, 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+ouuuleilei=gmail.com@gcc.gnu.org X-getmail-retrieved-from-mailbox: INBOX X-GMAIL-THRID: 1783800115654932224 X-GMAIL-MSGID: 1783800115654932224 From: Yannick Moy In order to facilitate the certification of System.Img_Bool, remove its dependency on unit System.Val_Bool. Modify the definition of ghost function Is_Boolean_Image_Ghost to take the expected boolean value and move it to System.Val_Spec. gcc/ada/ * libgnat/s-imgboo.adb: Remove with_clause now in spec file. * libgnat/s-imgboo.ads: Remove dependency on System.Val_Bool. (Image_Boolean): Replace call to Value_Boolean by passing value V to updated ghost function Is_Boolean_Image_Ghost. * libgnat/s-valboo.ads (Is_Boolean_Image_Ghost): Move to other unit. (Value_Boolean.): Update precondition. * libgnat/s-valspe.ads (Is_Boolean_Image_Ghost): Move here. Add new parameter for expected boolean value. Tested on x86_64-pc-linux-gnu, committed on master. --- gcc/ada/libgnat/s-imgboo.adb | 2 -- gcc/ada/libgnat/s-imgboo.ads | 5 ++--- gcc/ada/libgnat/s-valboo.ads | 34 ++-------------------------------- gcc/ada/libgnat/s-valspe.ads | 36 ++++++++++++++++++++++++++++++++++++ 4 files changed, 40 insertions(+), 37 deletions(-) diff --git a/gcc/ada/libgnat/s-imgboo.adb b/gcc/ada/libgnat/s-imgboo.adb index fb3301a4270..9a6340fc010 100644 --- a/gcc/ada/libgnat/s-imgboo.adb +++ b/gcc/ada/libgnat/s-imgboo.adb @@ -37,8 +37,6 @@ pragma Assertion_Policy (Ghost => Ignore, Loop_Invariant => Ignore, Assert => Ignore); -with System.Val_Spec; - package body System.Img_Bool with SPARK_Mode is diff --git a/gcc/ada/libgnat/s-imgboo.ads b/gcc/ada/libgnat/s-imgboo.ads index d40c0860fac..92cc7c31b57 100644 --- a/gcc/ada/libgnat/s-imgboo.ads +++ b/gcc/ada/libgnat/s-imgboo.ads @@ -42,7 +42,7 @@ pragma Assertion_Policy (Pre => Ignore, Contract_Cases => Ignore, Ghost => Ignore); -with System.Val_Bool; +with System.Val_Spec; package System.Img_Bool with SPARK_Mode, Preelaborate @@ -56,8 +56,7 @@ is Pre => S'First = 1 and then (if V then S'Length >= 4 else S'Length >= 5), Post => (if V then P = 4 else P = 5) - and then System.Val_Bool.Is_Boolean_Image_Ghost (S (1 .. P)) - and then System.Val_Bool.Value_Boolean (S (1 .. P)) = V; + and then System.Val_Spec.Is_Boolean_Image_Ghost (S (1 .. P), V); -- Computes Boolean'Image (V) and stores the result in S (1 .. P) -- setting the resulting value of P. The caller guarantees that S -- is long enough to hold the result, and that S'First is 1. diff --git a/gcc/ada/libgnat/s-valboo.ads b/gcc/ada/libgnat/s-valboo.ads index d48219953a0..6cdc3e559fe 100644 --- a/gcc/ada/libgnat/s-valboo.ads +++ b/gcc/ada/libgnat/s-valboo.ads @@ -47,40 +47,10 @@ package System.Val_Bool is pragma Preelaborate; - function Is_Boolean_Image_Ghost (Str : String) return Boolean is - (not System.Val_Spec.Only_Space_Ghost (Str, Str'First, Str'Last) - and then - (declare - F : constant Positive := System.Val_Spec.First_Non_Space_Ghost - (Str, Str'First, Str'Last); - begin - (F <= Str'Last - 3 - and then Str (F) in 't' | 'T' - and then Str (F + 1) in 'r' | 'R' - and then Str (F + 2) in 'u' | 'U' - and then Str (F + 3) in 'e' | 'E' - and then - (if F + 3 < Str'Last then - System.Val_Spec.Only_Space_Ghost (Str, F + 4, Str'Last))) - or else - (F <= Str'Last - 4 - and then Str (F) in 'f' | 'F' - and then Str (F + 1) in 'a' | 'A' - and then Str (F + 2) in 'l' | 'L' - and then Str (F + 3) in 's' | 'S' - and then Str (F + 4) in 'e' | 'E' - and then - (if F + 4 < Str'Last then - System.Val_Spec.Only_Space_Ghost (Str, F + 5, Str'Last))))) - with - Ghost; - -- Ghost function that returns True iff Str is the image of a boolean, that - -- is "true" or "false" in any capitalization, possibly surounded by space - -- characters. - function Value_Boolean (Str : String) return Boolean with - Pre => Is_Boolean_Image_Ghost (Str), + Pre => System.Val_Spec.Is_Boolean_Image_Ghost (Str, True) + or else System.Val_Spec.Is_Boolean_Image_Ghost (Str, False), Post => Value_Boolean'Result = (Str (System.Val_Spec.First_Non_Space_Ghost diff --git a/gcc/ada/libgnat/s-valspe.ads b/gcc/ada/libgnat/s-valspe.ads index dd861e5029f..6f0ca5317ff 100644 --- a/gcc/ada/libgnat/s-valspe.ads +++ b/gcc/ada/libgnat/s-valspe.ads @@ -72,6 +72,42 @@ is -- Ghost function that returns the index of the first non-space character -- in S, which necessarily exists given the precondition on S. + function Is_Boolean_Image_Ghost + (Str : String; + Val : Boolean) return Boolean + is + (not Only_Space_Ghost (Str, Str'First, Str'Last) + and then + (declare + F : constant Positive := First_Non_Space_Ghost + (Str, Str'First, Str'Last); + begin + (Val + and then F <= Str'Last - 3 + and then Str (F) in 't' | 'T' + and then Str (F + 1) in 'r' | 'R' + and then Str (F + 2) in 'u' | 'U' + and then Str (F + 3) in 'e' | 'E' + and then + (if F + 3 < Str'Last then + Only_Space_Ghost (Str, F + 4, Str'Last))) + or else + (not Val + and then F <= Str'Last - 4 + and then Str (F) in 'f' | 'F' + and then Str (F + 1) in 'a' | 'A' + and then Str (F + 2) in 'l' | 'L' + and then Str (F + 3) in 's' | 'S' + and then Str (F + 4) in 'e' | 'E' + and then + (if F + 4 < Str'Last then + Only_Space_Ghost (Str, F + 5, Str'Last))))) + with + Ghost; + -- Ghost function that returns True iff Str is the image of boolean Val, + -- that is "true" or "false" in any capitalization, possibly surounded by + -- space characters. + function Only_Number_Ghost (Str : String; From, To : Integer) return Boolean is (for all J in From .. To => Str (J) in '0' .. '9' | '_')