From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Received: from mail-lf1-x133.google.com (mail-lf1-x133.google.com [IPv6:2a00:1450:4864:20::133]) by sourceware.org (Postfix) with ESMTPS id EA8C3385841F for ; Tue, 5 Oct 2021 08:26:38 +0000 (GMT) DMARC-Filter: OpenDMARC Filter v1.4.1 sourceware.org EA8C3385841F Received: by mail-lf1-x133.google.com with SMTP id y23so43560355lfb.0 for ; Tue, 05 Oct 2021 01:26:38 -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=+F8Tqf0KQgYcBO+PRqWhHajiL8w8G+rCrM7tEPJj09o=; b=YJOoavtIHF4xLyV9MoLkuPnDbp3XGf6kZEIIF+PJTfMSfOGx2p1hDrHTh7VrjzHs1u 5n1Zr6M2RyxhQEIOBkYgJiu6AhZztnE/Hr6Nh4jDQ4YTmfUXkYXywrluxYHP79RFThe/ 3sdCYJrfxtJDgSURLM8hRgO43FE/qfJ72xoYf0B9YEQpCS6UrMHyVeQg3Tv41eNLTt26 9q3kAA2fXlW2yAQusS+EwA4EzNfThEncVzYUT0fcaQ4dyPNv/j0+F9FliADbBUdqS2CT jfLfczo0365hZmZ26hrVq7PZnr1waJAK8+kJvKqoisqsqT51vNeOh58t0anPKqfAtkqj c65g== X-Gm-Message-State: AOAM533Q0SsY3oIeJoIP8bwyAH2gBwGIwImiJgGFqwVhKm9j5IgfHpXu dsXB/df5jg277k76pJqDhH5sg3g3JCiQ4w== X-Google-Smtp-Source: ABdhPJxBnAemqbR6FyUKJZya58aopTjvanmt13bS41KosHyoKsNf6m6hZe4eoT/Z9RXGQPp0toS/IQ== X-Received: by 2002:ac2:420d:: with SMTP id y13mr2060107lfh.527.1633422397868; Tue, 05 Oct 2021 01:26:37 -0700 (PDT) Received: from adacore.com ([2a02:2ab8:224:2ce:72b5:e8ff:feef:ee60]) by smtp.gmail.com with ESMTPSA id j18sm1874051lfu.84.2021.10.05.01.26.36 (version=TLS1_3 cipher=TLS_AES_256_GCM_SHA384 bits=256/256); Tue, 05 Oct 2021 01:26:37 -0700 (PDT) Date: Tue, 5 Oct 2021 08:26:36 +0000 From: Pierre-Marie de Rodat To: gcc-patches@gcc.gnu.org Cc: Joffrey Huguet Subject: [Ada] Add Default_Initial_Condition to type Unbounded_String Message-ID: <20211005082636.GA2693574@adacore.com> MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="0OAP2g/MAC+5xKAE" Content-Disposition: inline X-Spam-Status: No, score=-13.0 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 autolearn=ham autolearn_force=no version=3.4.4 X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) 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: Tue, 05 Oct 2021 08:26:40 -0000 --0OAP2g/MAC+5xKAE Content-Type: text/plain; charset=us-ascii Content-Disposition: inline SPARK emitted spurious checks on Unbounded_String variables that were not initialized. This patch adds a default initial condition to the type Unbounded_String so that they disappear. Tested on x86_64-pc-linux-gnu, committed on trunk gcc/ada/ * libgnat/a-strunb.ads, libgnat/a-strunb__shared.ads: Add Default_Initial_Condition to Unbounded_String. --0OAP2g/MAC+5xKAE Content-Type: text/x-diff; charset=us-ascii Content-Disposition: attachment; filename="patch.diff" diff --git a/gcc/ada/libgnat/a-strunb.ads b/gcc/ada/libgnat/a-strunb.ads --- a/gcc/ada/libgnat/a-strunb.ads +++ b/gcc/ada/libgnat/a-strunb.ads @@ -58,7 +58,8 @@ package Ada.Strings.Unbounded with is pragma Preelaborate; - type Unbounded_String is private; + type Unbounded_String is private with + Default_Initial_Condition => Length (Unbounded_String) = 0; pragma Preelaborable_Initialization (Unbounded_String); Null_Unbounded_String : constant Unbounded_String; diff --git a/gcc/ada/libgnat/a-strunb__shared.ads b/gcc/ada/libgnat/a-strunb__shared.ads --- a/gcc/ada/libgnat/a-strunb__shared.ads +++ b/gcc/ada/libgnat/a-strunb__shared.ads @@ -85,7 +85,8 @@ package Ada.Strings.Unbounded with is pragma Preelaborate; - type Unbounded_String is private; + type Unbounded_String is private with + Default_Initial_Condition => Length (Unbounded_String) = 0; pragma Preelaborable_Initialization (Unbounded_String); Null_Unbounded_String : constant Unbounded_String; --0OAP2g/MAC+5xKAE--