Full details of all language and tool changes can be found
in the release notes for
release 7.4.
Supported, professional customers will receive upgrade packages
immediately.
New "accept" annotation system to indicate that
a particular error or warning is expected and justified.
New "Always_Valid" assertion to indicate that
the values read from an external input are trustworthy.
Obsolete SPARK83 floating-point attributes are now acceptable
in SPARK95 mode.
Better error messages for common syntax and semantic errors.
Complete re-implementation of VC Generation for single-
and multi-dimensional unconstrained array parameters. Supporting
improvements in the default invariant generator and Simplifier.
Conditional data- and information-flow anomalies are now
reported as errors not warnings.
Support for System.Bit_Order and System.Default_Bit_Order
in the configuration file.
The Examiner now issues a warning if an Ada2005 reserved
word is used as an identifier in SPARK95 mode.
The Simplifier's handling is user-defined and Examiner-generated
proof-rules has been unified and improved.
The Simplifier has a new family of proof tactics for enumerated
and integer inequalities where transitivity of the relational
operators is involved.
The implementation of the /p=N (multiprocessor) switch
in SPARKSimp has been re-implemented to make much better
use of all the available processing resources on multi-core
or multi-processor machines.
SPARKFormat now has options to reformat the own, initializes
and inherit annotations.
SPARKMake can now produce with absolute or relative pathnames
in the generated index and meta-files.
