From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Received: from mail-wr1-x432.google.com (mail-wr1-x432.google.com [IPv6:2a00:1450:4864:20::432]) by sourceware.org (Postfix) with ESMTPS id 2233238515D9 for ; Mon, 12 Sep 2022 08:19:34 +0000 (GMT) DMARC-Filter: OpenDMARC Filter v1.4.1 sourceware.org 2233238515D9 Authentication-Results: sourceware.org; dmarc=pass (p=none dis=none) header.from=adacore.com Authentication-Results: sourceware.org; spf=pass smtp.mailfrom=adacore.com Received: by mail-wr1-x432.google.com with SMTP id c11so14029295wrp.11 for ; Mon, 12 Sep 2022 01:19:34 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=adacore.com; s=google; h=content-disposition:mime-version:message-id:subject:cc:to:from:date :from:to:cc:subject:date; bh=+w+hQw1IFuVdamYe+rJbRq5/FWg29rg7LpmtPQE4lgA=; b=dW44CvbqyALKbsekz3xKfrBbWFhuDYMQirCgMRHFoqrIA4fkgujJTstnJe3aRmOsm8 HJHhw0bwo5VlBVOI89/RChmlPENwg3B5boZADuj0hxoPbd9uzrjdkPhM4JKfE8+v0A8/ 0nUmOWM2HWA4aw/JJ4LNAgFyOOMvZ9IM+m9dmlPcgzD/GkIIfusyxZdDYPjT+BQ33059 ku1yXW/UGhfKe9wN1MEsJrMZP15Oljdef996aIazPeFC6ZfF3OK8Uuq2aWgDcN2Y58xF gN9os/pGthwOm75MxrnOwzpnbKJwEZqLn31Ohpaz9ZKivdfkScxFBRYAY7apEtFW1+At 06nA== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20210112; h=content-disposition:mime-version:message-id:subject:cc:to:from:date :x-gm-message-state:from:to:cc:subject:date; bh=+w+hQw1IFuVdamYe+rJbRq5/FWg29rg7LpmtPQE4lgA=; b=LsBb5spJ1A6NMee8LH+uAD2eAi4lbjmkzETRpD3FzSJ9fAAEsTibd0B14UQe53/AkF 3FrGF+0nJQoTKyvbM22UYVI7gWpwNnN6Lck3nTsaX9qmxAWBB0oBJ0fX3t4QvrUw8kdg F9V2IWvqUyPoxXIy/x2cTPtG7KyBUq+4FoaAMw5nRwP3duYXL8Afm6RGFUfpnUkSsOgi jv+mIpnPqj1nwWcZivbwgzWceBGdOaPrThRBgaWTJDnrO+k5R9Q0pqtBLhPnXRcGTTXZ hCSMcHwKgIM8SYX9EpRUa7FAbjzFGy684oAT2RNZCCTglOza9k21X9RD/XpvQn0Vdq2m 37PA== X-Gm-Message-State: ACgBeo16jgE2GZYWxz1Kwvo94z8oGdivND+UsnQfLL7Tka1xGiz7ySIu dwtxFfXarPYG0mdfmYA54o6Nha17F/5wEw== X-Google-Smtp-Source: AA6agR7UPNLX9xXDtBXR8bK4XVSiaNLzaDtVp11F8ttWg6rZX/kRMb0LmYqFJGQ+TC39w/3ySag4gg== X-Received: by 2002:adf:f94b:0:b0:22a:4306:b773 with SMTP id q11-20020adff94b000000b0022a4306b773mr6992013wrr.307.1662970773739; Mon, 12 Sep 2022 01:19:33 -0700 (PDT) Received: from poulhies-Precision-5550 (lmontsouris-659-1-24-67.w81-250.abo.wanadoo.fr. [81.250.175.67]) by smtp.gmail.com with ESMTPSA id h17-20020a05600c2cb100b003a5ca627333sm9541253wmc.8.2022.09.12.01.19.33 (version=TLS1_3 cipher=TLS_AES_256_GCM_SHA384 bits=256/256); Mon, 12 Sep 2022 01:19:33 -0700 (PDT) Date: Mon, 12 Sep 2022 10:19:32 +0200 From: Marc =?iso-8859-1?Q?Poulhi=E8s?= To: gcc-patches@gcc.gnu.org Cc: Yannick Moy Subject: [Ada] Reject use in SPARK of Asm intrinsics for code insertions Message-ID: <20220912081932.GA1512996@poulhies-Precision-5550> MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="wac7ysb48OaltWcw" Content-Disposition: inline X-Spam-Status: No, score=-12.8 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 List-Id: --wac7ysb48OaltWcw Content-Type: text/plain; charset=us-ascii Content-Disposition: inline SPARK does not allow code insertions. This applies also to calls to Asm intrinsics defined in System.Machine_Code. Tested on x86_64-pc-linux-gnu, committed on trunk gcc/ada/ * libgnat/s-maccod.ads: Mark package as SPARK_Mode Off. --wac7ysb48OaltWcw Content-Type: text/x-diff; charset=us-ascii Content-Disposition: attachment; filename="patch.diff" diff --git a/gcc/ada/libgnat/s-maccod.ads b/gcc/ada/libgnat/s-maccod.ads --- a/gcc/ada/libgnat/s-maccod.ads +++ b/gcc/ada/libgnat/s-maccod.ads @@ -33,7 +33,9 @@ -- operations, and also for machine code statements. See GNAT documentation -- for full details. -package System.Machine_Code is +package System.Machine_Code + with SPARK_Mode => Off +is pragma No_Elaboration_Code_All; pragma Pure; --wac7ysb48OaltWcw--