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] Clean ups in SPARK mode


1) Remove special expansion of NOT IN operator in SPARK verification

The special expansion for NOT IN operator in the SPARK formal verification
mode is not needed anymore. Now removed.

2) Document additional requirements on tree for SPARK verification

Formal verification of SPARK code is done in a special mode, in which
the tree generated by the frontend must respect additional requirements.
These are now described in a special section of sinfo.ads

2013-10-17  Yannick Moy  <moy@adacore.com>

	* exp_spark.adb (Expand_SPARK): Remove special case for NOT IN
	operation.
	* sinfo.ads: Add special comment section to describe SPARK mode
	effect on tree.
	* exp_spark.ads: Remove comments, moved to sinfo.ads.

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]