This is the mail archive of the gcc-patches@gcc.gnu.org mailing list for the GCC project.

Index Nav:	[Date Index] [Subject Index] [Author Index] [Thread Index]
Message Nav:	[Date Prev] [Date Next]	[Thread Prev] [Thread Next]
Other format:	[Raw text]

[Ada] Remove SPARK legality checks performed in GNATprove

From: Arnaud Charlet <charlet at adacore dot com>
To: gcc-patches at gcc dot gnu dot org
Cc: Yannick Moy <moy at adacore dot com>
Date: Mon, 18 Apr 2016 06:37:58 -0400
Subject: [Ada] Remove SPARK legality checks performed in GNATprove
Authentication-results: sourceware.org; auth=none

Checks that some types and objects are fully default initialized should
be performed in GNATprove, where relevant information about SPARK status
of private types in particular is available. Move two tests performed in
the frontend to GNATprove here.

Tested on x86_64-pc-linux-gnu, committed on trunk

2016-04-18  Yannick Moy  <moy@adacore.com>

	* contracts.adb (Analyze_Object_Contract,
	Analyze_Protected_Contract): Remove tests performed in GNATprove.
	* sem_util.adb, sem_util.ads (Has_Full_Default_Initialization):
	Remove query for tests performed in GNATprove.

Attachment: difs
Description: Text document

Index Nav:	[Date Index] [Subject Index] [Author Index] [Thread Index]
Message Nav:	[Date Prev] [Date Next]	[Thread Prev] [Thread Next]