Pragma/aspect Suppress_Initialization for variables
Suppress_Initialization can now be used as a boolean aspect as well as a pragma, and now applies to variables as well as types. When applied to a variable it suppresses all implicit initialization for that variable.
Improved messages in configurable run-time mode
The error messages for unsupported features in a configurable run-time have been enhanced for the cases of task rendezvous not supported, and specified array packing not supported. Instead of just listing the (possibly obscure) name of the missing entity in these cases, a clear error message is now given saying that the feature is not supported. In the latter case an error is now issued on the array type declaration itself, as well as on packed operations.
Aug 21st, 2014
Support for manual proof with Coq
GNATprove now offers suppor to use of Coq to manually prove SPARK 2014 VCs. This includes:
- Extraction and verification of files containing SPARK 2014 VC that must be completed by the user with proof. - Definition of a project attribute to specify the location of VC files. - Communication with GPS environment for SPARK 2014 to perform manual proof from the IDE.
This is the manual for administering and using GNATdashboard.
GNATdoc User’s Guide
This User’s Guide describes how to use GNATdoc, a documentation tool for Ada which processes source files, extracts documentation directly from the sources, and generates annotated HTML files.
GNATbench for Eclipse User’s Guide
This User’s Guide describes how to use the GNATbench Ada plug-in for Eclipse. Specific help is provided for configuring projects, building systems, and debugging.
GNAT User’s Guide for native platforms
This guide describes the use of GNAT, a compiler and software development toolset for the full Ada programming language.
It describes the features of the compiler and tools, and details how to use them to build Ada 95 applications.
SPARK 2014 Toolset User’s Guide
This guide is aimed at getting new users up and running with the SPARK 2014 tools.