From patchwork Tue Dec 11 11:32:37 2018 Content-Type: text/plain; charset="utf-8" MIME-Version: 1.0 Content-Transfer-Encoding: 7bit X-Patchwork-Submitter: Pierre-Marie de Rodat X-Patchwork-Id: 1011054 Return-Path: X-Original-To: incoming@patchwork.ozlabs.org Delivered-To: patchwork-incoming@bilbo.ozlabs.org Authentication-Results: ozlabs.org; spf=pass (mailfrom) smtp.mailfrom=gcc.gnu.org (client-ip=209.132.180.131; helo=sourceware.org; envelope-from=gcc-patches-return-492094-incoming=patchwork.ozlabs.org@gcc.gnu.org; receiver=) Authentication-Results: ozlabs.org; dmarc=none (p=none dis=none) header.from=adacore.com Authentication-Results: ozlabs.org; dkim=pass (1024-bit key; unprotected) header.d=gcc.gnu.org header.i=@gcc.gnu.org header.b="RAB2ZDlz"; dkim-atps=neutral Received: from sourceware.org (server1.sourceware.org [209.132.180.131]) (using TLSv1.2 with cipher ECDHE-RSA-AES256-GCM-SHA384 (256/256 bits)) (No client certificate requested) by ozlabs.org (Postfix) with ESMTPS id 43Dd9Q089Fz9s3q for ; Tue, 11 Dec 2018 22:33:13 +1100 (AEDT) DomainKey-Signature: a=rsa-sha1; c=nofws; d=gcc.gnu.org; h=list-id :list-unsubscribe:list-archive:list-post:list-help:sender:date :from:to:cc:subject:message-id:mime-version:content-type; q=dns; s=default; b=IbCf4gtL6WON8xhT0KbR6Bk9sfR1pErbNGzUGFQ+va2iYvmcWe AragO8daNldOZxNMU9+tHxTMeXxVBno0bACsByJdnExHA4ZgN90IvkM7hkALbUZi D2/1gR6e3X+/Kc7OgIMklN4B0DMTgb6kSZj2G3+VjiHQDEWIBfKvvlbhg= DKIM-Signature: v=1; a=rsa-sha1; c=relaxed; d=gcc.gnu.org; h=list-id :list-unsubscribe:list-archive:list-post:list-help:sender:date :from:to:cc:subject:message-id:mime-version:content-type; s= default; bh=E+nSDbrCAPDQqU0pfhk12bkmIqg=; b=RAB2ZDlzyi1dkl17mcJ7 QU8lyEochc9hyeLeK1Sni7cpMgrq/W6DH5QhEMtEQpD5GyDxrkXbQZJIaahH6yPY B0dGwjoXkrUyo5bxA5lfNV8qqlAHisuF1UH/kDwESSFeUEFqkS9X8Jz1EfE1AyLJ sfto+KUPYJcUzgeOxgqPFxE= Received: (qmail 72001 invoked by alias); 11 Dec 2018 11:32:41 -0000 Mailing-List: contact gcc-patches-help@gcc.gnu.org; run by ezmlm Precedence: bulk List-Id: List-Unsubscribe: List-Archive: List-Post: List-Help: Sender: gcc-patches-owner@gcc.gnu.org Delivered-To: mailing list gcc-patches@gcc.gnu.org Received: (qmail 71924 invoked by uid 89); 11 Dec 2018 11:32:40 -0000 Authentication-Results: sourceware.org; auth=none X-Spam-SWARE-Status: No, score=-11.9 required=5.0 tests=BAYES_00, GIT_PATCH_2, GIT_PATCH_3, RCVD_IN_DNSWL_NONE, SPF_PASS autolearn=ham version=3.3.2 spammy=sem_util X-HELO: rock.gnat.com Received: from rock.gnat.com (HELO rock.gnat.com) (205.232.38.15) by sourceware.org (qpsmtpd/0.93/v0.84-503-g423c35a) with ESMTP; Tue, 11 Dec 2018 11:32:39 +0000 Received: from localhost (localhost.localdomain [127.0.0.1]) by filtered-rock.gnat.com (Postfix) with ESMTP id BF3395608A; Tue, 11 Dec 2018 06:32:37 -0500 (EST) Received: from rock.gnat.com ([127.0.0.1]) by localhost (rock.gnat.com [127.0.0.1]) (amavisd-new, port 10024) with LMTP id tUKTTwf+giPU; Tue, 11 Dec 2018 06:32:37 -0500 (EST) Received: from tron.gnat.com (tron.gnat.com [IPv6:2620:20:4000:0:46a8:42ff:fe0e:e294]) by rock.gnat.com (Postfix) with ESMTP id A13AA5608D; Tue, 11 Dec 2018 06:32:37 -0500 (EST) Received: by tron.gnat.com (Postfix, from userid 4862) id A047A3573; Tue, 11 Dec 2018 06:32:37 -0500 (EST) Date: Tue, 11 Dec 2018 06:32:37 -0500 From: Pierre-Marie de Rodat To: gcc-patches@gcc.gnu.org Cc: Yannick Moy Subject: [Ada] Support access types in GNATprove Message-ID: <20181211113237.GA105080@adacore.com> MIME-Version: 1.0 Content-Disposition: inline User-Agent: Mutt/1.5.23 (2014-03-12) X-IsSubscribed: yes SPARK RM has been updated to support access types in SPARK. Part of this support is that now SPARK RM 3.1 lists access types as having full default initialization. Now updated. There is no impact on compilation. Tested on x86_64-pc-linux-gnu, committed on trunk 2018-12-11 Yannick Moy gcc/ada/ * sem_util.adb (Has_Full_Default_Initialization): Consider access types as having full default initialization. --- gcc/ada/sem_util.adb +++ gcc/ada/sem_util.adb @@ -10880,6 +10880,11 @@ package body Sem_Util is if Is_Scalar_Type (Typ) then return Has_Default_Aspect (Typ); + -- An access type is fully default initialized by default + + elsif Is_Access_Type (Typ) then + return True; + -- An array type is fully default initialized if its element type is -- scalar and the array type carries aspect Default_Component_Value or -- the element type is fully default initialized.