From patchwork Sat Aug 10 20:03:41 2024 Content-Type: text/plain; charset="utf-8" MIME-Version: 1.0 Content-Transfer-Encoding: 8bit X-Patchwork-Submitter: Gerald Pfeifer X-Patchwork-Id: 1971175 Return-Path: X-Original-To: incoming@patchwork.ozlabs.org Delivered-To: patchwork-incoming@legolas.ozlabs.org Authentication-Results: legolas.ozlabs.org; dkim=pass (2048-bit key; unprotected) header.d=pfeifer.com header.i=@pfeifer.com header.a=rsa-sha256 header.s=pair-202402271039 header.b=qtou3nWS; dkim-atps=neutral Authentication-Results: legolas.ozlabs.org; spf=pass (sender SPF authorized) smtp.mailfrom=gcc.gnu.org (client-ip=2620:52:3:1:0:246e:9693:128c; helo=server2.sourceware.org; envelope-from=gcc-patches-bounces~incoming=patchwork.ozlabs.org@gcc.gnu.org; receiver=patchwork.ozlabs.org) Received: from server2.sourceware.org (server2.sourceware.org [IPv6:2620:52:3:1:0:246e:9693:128c]) (using TLSv1.3 with cipher TLS_AES_256_GCM_SHA384 (256/256 bits) key-exchange X25519 server-signature ECDSA (secp384r1) server-digest SHA384) (No client certificate requested) by legolas.ozlabs.org (Postfix) with ESMTPS id 4WhBZ26ZKvz1yXl for ; Sun, 11 Aug 2024 06:04:08 +1000 (AEST) Received: from server2.sourceware.org (localhost [IPv6:::1]) by sourceware.org (Postfix) with ESMTP id 5B62D3858CDB for ; Sat, 10 Aug 2024 20:04:06 +0000 (GMT) X-Original-To: gcc-patches@gcc.gnu.org Delivered-To: gcc-patches@gcc.gnu.org Received: from hamza.pair.com (hamza.pair.com [209.68.5.143]) by sourceware.org (Postfix) with ESMTPS id E98C33858D26 for ; Sat, 10 Aug 2024 20:03:44 +0000 (GMT) DMARC-Filter: OpenDMARC Filter v1.4.2 sourceware.org E98C33858D26 Authentication-Results: sourceware.org; dmarc=none (p=none dis=none) header.from=pfeifer.com Authentication-Results: sourceware.org; spf=pass smtp.mailfrom=pfeifer.com ARC-Filter: OpenARC Filter v1.0.0 sourceware.org E98C33858D26 Authentication-Results: server2.sourceware.org; arc=none smtp.remote-ip=209.68.5.143 ARC-Seal: i=1; a=rsa-sha256; d=sourceware.org; s=key; t=1723320227; cv=none; b=XEAkg1qfu451D8lw9L5V5oBQRq7yj+m2/3nDgW7Qx1W5Watm2eQiBu2rY1gjCJo4nZ7TfrCpB/ZoW15sMuiWZQTHWgibX5LA26eII93IED7lrlKvjLiur99dtz4CTI2MdaVUoOgA25Cdye+2/apniJWB02K09OSPZK1uLYSgI5U= ARC-Message-Signature: i=1; a=rsa-sha256; d=sourceware.org; s=key; t=1723320227; c=relaxed/simple; bh=f+14XzPicgk9/LYidSL2mPdzTe7iZkkioqT5xmpH1yQ=; h=Date:From:To:Subject:Message-ID:MIME-Version:DKIM-Signature; b=h2FfOR8gX5zzUHKAWnL2YLc3nYeuBNyu8ctYyUxheZzCFKmxgK66YOXtuEtcWkShkOy3RZt3vsXVE/B8tETUjPjh3OuAuf0Wjf4n+iV667MZNAaAhJZZtaSg1eUp35C5KUTI36Dy7Dn/fd2RsDagT7oPBLBr6z7Ldnq481kAXq0= ARC-Authentication-Results: i=1; server2.sourceware.org Received: from hamza.pair.com (localhost [127.0.0.1]) by hamza.pair.com (Postfix) with ESMTP id BD5E333E84; Sat, 10 Aug 2024 16:03:44 -0400 (EDT) Received: from daya.localdomain (188-23-0-15.adsl.highway.telekom.at [188.23.0.15]) (using TLSv1.3 with cipher TLS_AES_256_GCM_SHA384 (256/256 bits) key-exchange X25519 server-signature RSA-PSS (2048 bits) server-digest SHA256) (No client certificate requested) by hamza.pair.com (Postfix) with ESMTPSA id A2BEC33E81; Sat, 10 Aug 2024 16:03:43 -0400 (EDT) Date: Sat, 10 Aug 2024 22:03:41 +0200 (CEST) From: Gerald Pfeifer To: =?iso-8859-15?q?Marc_Poulhi=E8s?= cc: gcc-patches@gcc.gnu.org, Fernando Oleo Blanco , Piotr Trojanek Subject: [wwwdocs] Re: [COMMITTED] gcc-14: Add Ada changes In-Reply-To: <20240426085539.927586-1-poulhies@adacore.com> Message-ID: <5f622e5d-9c07-6e24-f4bd-1226f219ccfa@pfeifer.com> References: <20240426085539.927586-1-poulhies@adacore.com> MIME-Version: 1.0 DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=pfeifer.com; h=date:from:to:cc:subject:in-reply-to:message-id:references:mime-version:content-type; s=pair-202402271039; bh=52QUUHmFo5izFBwY1UuaHscFfv1zIVXXJwBfDsxzZ3c=; b=qtou3nWStV9qhUDBrBtnDDfQPhxuxXTMnYXGsl1aIKo6e9VIeJA7GERRiSH/8ypXktFsRw4YnPOe2j7SxwzuLq5KvnEn4qtTjfcSfZCCCIxMHTzwMdENW+1EfqN/q5TOMXimMZMmHT8F4ztDXvztmi19UYcfRsWLVTLGQOLkK5l5cdg/1CmfQM6eiuDNRbAfM0kON6+GAFh7uejc8NIVljY5t0NV1VwQhh3/b2t4jefYegt1V7En4orZW9aIqO3x42mDnzrWBTcvMpwCtrzTmBJmUBupayDiF4iW5x1SUzDhEeuL9olrrmtN+sEke791x3EkRkLBAWOoRj6XDVcg+A== X-Scanned-By: mailmunge 3.11 on 209.68.5.143 X-Spam-Status: No, score=-10.0 required=5.0 tests=BAYES_00, DKIM_SIGNED, DKIM_VALID, DKIM_VALID_AU, DKIM_VALID_EF, GIT_PATCH_0, KAM_SHORT, RCVD_IN_BARRACUDACENTRAL, 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 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~incoming=patchwork.ozlabs.org@gcc.gnu.org On Fri, 26 Apr 2024, Marc Poulhiès wrote: > Co-authored-by: Fernando Oleo Blanco > Co-authored-by: Piotr Trojanek > Signed-off-by: Marc Poulhiès > --- > htdocs/gcc-14/changes.html | 67 +++++++++++++++++++++++++++++++++++++- This is really great how thoroughly you documented all these changes - thanks to the three of you! Below is a little follow-up I'd like to propose: It mostly simplifies the structure of bullet items a bit and changes "it may have output parameters ... and not terminate" to "it may have output parameters ... and fail to terminate", the former somehow feeling odd for me to read. What do you think? Gerald diff --git a/htdocs/gcc-14/changes.html b/htdocs/gcc-14/changes.html index aa1d97a8..03c4bd18 100644 --- a/htdocs/gcc-14/changes.html +++ b/htdocs/gcc-14/changes.html @@ -246,35 +246,35 @@ You may also want to check out our
  • New implementation-defined aspects and pragmas:
      -
    • Local_Restrictions, - which specifies that a particular subprogram does not violate one or more +
    • Local_Restrictions + specifies that a particular subprogram does not violate one or more local restrictions, nor can it call a subprogram that is not subject to the same requirements.
    • User_Aspect_Definition - and User_Aspect, - which provide a mechanism for avoiding textual duplication if some set of + and User_Aspect + provide a mechanism for avoiding textual duplication if some set of aspect specifications is needed in multiple places.
  • New implementation-defined aspects and pragmas for verification of the SPARK 2014 subset of Ada:
      -
    • Always_Terminates, - which provides a condition for a subprogram to necessarily complete +
    • Always_Terminates + provides a condition for a subprogram to necessarily complete (either return normally or raise an exception).
      • -
    • Ghost_Predicate, - which introduces a subtype predicate that can reference Ghost entities. +
    • Ghost_Predicate + introduces a subtype predicate that can reference Ghost entities.
      • -
    • Exceptional_Cases, - which lists exceptions that might be propagated by the subprogram with - side effects in the context of its precondition and associates them with a - specific postcondition. +
    • Exceptional_Cases + lists exceptions that might be propagated by the subprogram with + side effects in the context of its precondition and associates them + with a specific postcondition.
      • -
    • Side_Effects, - which indicates that a function should be handled like a procedure with +
    • Side_Effects + indicates that a function should be handled like a procedure with respect to parameter modes, Global contract, exceptional contract and termination: it may have output parameters, write global variables, raise - exceptions and not terminate.
      • + exceptions and fail to terminate.
  • The new attributes and contracts have been applied to the relevant parts @@ -297,7 +297,7 @@ You may also want to check out our
  • Experimental features:
    • Storage - Model: this feature proposes to redesign the concepts of Storage Pools + Model: proposes to redesign the concepts of Storage Pools into a more efficient model allowing higher performance and easier integration with low footprint embedded runtimes.
    • String