From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Received: from mail-ed1-x52a.google.com (mail-ed1-x52a.google.com [IPv6:2a00:1450:4864:20::52a]) by sourceware.org (Postfix) with ESMTPS id BDBCF395443E for ; Thu, 2 Jun 2022 09:08:53 +0000 (GMT) DMARC-Filter: OpenDMARC Filter v1.4.1 sourceware.org BDBCF395443E Received: by mail-ed1-x52a.google.com with SMTP id x62so5419418ede.10 for ; Thu, 02 Jun 2022 02:08:53 -0700 (PDT) X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20210112; h=x-gm-message-state:date:from:to:cc:subject:message-id:mime-version :content-disposition; bh=OPvuI7R+ZudcHxeRhQJzoNKFz/wLE3ASBMOYCrFxfbc=; b=0ZUNpeEmXv6yN+srRUVMH6skS4efgy163hkm7l8cJo/UTzZlN0d8IvEz7/+B4lV9ni cyFvtW2tLR6j+sGTyRdvlpxs3ZkBq40sb70IQ6i92F4Dh6FfgdY8EMFcXaxY6a6Ke8pl dqdttcf8bTVujDAaGJqM/6IjQ6w6fRqfuAQnhPjjv+dwDdbrh2DrxPGkI9GI1KGYLa75 zTXYHuHo4z6O/8DT4+Zg9osjqJl1QqrGbHlttwK70HtSmET91Iz8VZSg3/K0SYC8Wn3e Ylyqj9L5qvbQkaYCSZyiiiOONWm8s/pTIgrYS6GcR42ZVhYKj/pHcobo/EiMO561Kr18 K2bw== X-Gm-Message-State: AOAM531p6IaqBpgCb9B8XSj5t5CkigGXfJAA95V25J9akEL+3kuDbymM VDhhvLqqYg7G5RtPF6ni3f4mV4wdy6QdYg== X-Google-Smtp-Source: ABdhPJwqxw7+ILXX8noh5oBHaqWGZn/5YSOLkc78duZiogF0j8vzjsMHbaEYpUtyWUSdIDsfd3+7JQ== X-Received: by 2002:a05:6402:3899:b0:42d:d79e:acef with SMTP id fd25-20020a056402389900b0042dd79eacefmr4215343edb.12.1654160932582; Thu, 02 Jun 2022 02:08:52 -0700 (PDT) Received: from adacore.com ([45.147.211.82]) by smtp.gmail.com with ESMTPSA id r24-20020a170906549800b006f3ef214db9sm1536176ejo.31.2022.06.02.02.08.51 (version=TLS1_3 cipher=TLS_AES_256_GCM_SHA384 bits=256/256); Thu, 02 Jun 2022 02:08:52 -0700 (PDT) Date: Thu, 2 Jun 2022 09:08:51 +0000 From: Pierre-Marie de Rodat To: gcc-patches@gcc.gnu.org Cc: Joffrey Huguet Subject: [Ada] Complete contracts of Interfaces.C.Strings subprograms Message-ID: <20220602090851.GA1010590@adacore.com> MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="huq684BweRXVnRxX" Content-Disposition: inline X-Spam-Status: No, score=-13.2 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.29 Precedence: list List-Id: Gcc-patches mailing list List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , X-List-Received-Date: Thu, 02 Jun 2022 09:08:55 -0000 --huq684BweRXVnRxX Content-Type: text/plain; charset=us-ascii Content-Disposition: inline This patch adds preconditions to Update procedures, to protect from Update_Error propagations. Tested on x86_64-pc-linux-gnu, committed on trunk gcc/ada/ * libgnat/i-cstrin.ads (Update): Add precondition. --huq684BweRXVnRxX Content-Type: text/x-diff; charset=us-ascii Content-Disposition: attachment; filename="patch.diff" diff --git a/gcc/ada/libgnat/i-cstrin.ads b/gcc/ada/libgnat/i-cstrin.ads --- a/gcc/ada/libgnat/i-cstrin.ads +++ b/gcc/ada/libgnat/i-cstrin.ads @@ -36,7 +36,8 @@ -- Preconditions in this unit are meant for analysis only, not for run-time -- checking, so that the expected exceptions are raised. This is enforced by -- setting the corresponding assertion policy to Ignore. These preconditions --- do not protect against Storage_Error. +-- protect from Dereference_Error and Update_Error, but not from +-- Storage_Error. pragma Assertion_Policy (Pre => Ignore); @@ -117,7 +118,9 @@ is Chars : char_array; Check : Boolean := True) with - Pre => Item /= Null_Ptr, + Pre => + Item /= Null_Ptr + and then (if Check then Offset <= Strlen (Item) - Chars'Length), Global => (In_Out => C_Memory); procedure Update @@ -126,7 +129,9 @@ is Str : String; Check : Boolean := True) with - Pre => Item /= Null_Ptr, + Pre => + Item /= Null_Ptr + and then (if Check then Offset <= Strlen (Item) - Str'Length), Global => (In_Out => C_Memory); Update_Error : exception; --huq684BweRXVnRxX--