- Ada 2012
- Ada 2005 / 95 / 83
- Embedded Development
- Formal Methods
- Open Source
- Safety-Critical Development
- Static Analysis
Dec 28th, 2014
Eliminate false warnings for unused entities
If no entities of a package are directly used, but the package is used as a generic actual parameter, the compiler could still give a warning that no entities of the package were used. These unhelpful warnings have now been eliminated.
Dec 26th, 2014
More complete warnings in validity checking mode
In some cases, the warning about a variable not being modified (so that it could be a constant) gets lost if validity checking is turned on. This warning is now given in validity checking mode.
Dec 23rd, 2014
Warning for suspicious Subprogram’Access
A warning is now given for P'Access, where P is a subprogram in the same package as the P'Access, and the P'Access is evaluated at elaboration time, and occurs before the body of P. For example, "X : T := P'Access;" would allow a subsequent call to X.all to be an access-before-elaboration error; hence the warning. This warning is enabled by the -gnatw.f switch.
Dec 19th, 2014
More automated proof on conversions to float
Proof automation has been improved on code that converts between integers and floats.
Dec 18th, 2014
Linking with—lto=nn when -jnn and—lto are used
When gprbuild is invoked with -jnn (nn > 1) and with the linker switch --lto (or -flto), the linker is invoked with --lto=nn (or -flto=nn) to speed up linking.
Warning on misuse of attribute Update
A common mistake when using attribute Update in postconditions or loop invariants is to forget to use it in combination with attribute Old or Loop_Entry, which results in nonsensical expressions of the form
X = X'Update(...)instead of the intended (in a postcondition)
X = X'Old'Update(...)or (in a loop invariant)
X = X'Loop_Entry'Update(...)GNAT and GNATprove now issue a warning by default on the nonsensical form, controlled with warning switches -gnatw.t/-gnatw.T
Add search path for project files
The GNATprove tool now has a commandline option "-aP" similar to the same option of gprbuild, which allows to add search paths for the location of project files.
Dec 16th, 2014
Simplified code in Delay_Until in Ravenscar Cert
The implementation of delay until operations in the Ravenscar Cert runtime library for Vxworks Cert has been greatly simplified since many conditions cannot occur under the Ravenscar restrictions.
Dec 15th, 2014
Subprograms without exports no longer ineffective
Flow analysis used to flag calls to subprograms without exports as ineffective. This is no longer the case.
Dec 12th, 2014
Improved handling of floating point conversions
The SPARK toolset has now improved handling of conversions between single and double precision floating point types. The result is more proved checks in the presence of such conversions.
Shared manual proof files
User's can now provide theorem libraries to GNATprove in order to access contained theorems during manual proof. To do so, the user needs to provide the sources of the library in the Proof_Dir and GNATprove will be in charge to compile it.
Accept “alt-ergo” as prover name
A common typo is to type "alt-ergo" instead of "altergo" when specifying the prover "Alt-Ergo" using the option --prover. The tool now accepts both variants.
Dec 10th, 2014
GPRinstall Mode & Install_Name attributes
It is now possible to set the Mode and Install_Name value in the package Install of a project. These attributes are equivalent to the GPSinstall command line options but allow per project fine tuning of the installation setup.
Setting custom linker script for LEON run times
User-defined linker scripts for bare board LEON targets can be set by simply defining the environment variable LDSCRIPT to point to the file to use.
Implement new restriction No_Use_Of_Entity
A new restriction No_Use_Of_Entity is implemented. The form of this is pragma Restriction[_Warning]s (No_Use_Of_Entity => NAME), where NAME is a fully qualified entity name. The effect is to forbid references to this entity in the main unit, its spec, and any subunits. For example, the use of pragma Restrictions (No_Use_Of_Entity => Ada.Text_IO.Put_Line) would forbid references to Put_Line, but references to Put would still be allowed.
Trap table for LEON not modified at execution time
The run-time libraries for bare board LEON processors install statically the minimum number of trap entries. Hence, the trap table can be easily kept in ROM.
Dec 8th, 2014
Inline_Always effective on instances without -gnatN
On targets where inlining of calls must be done by the front end (such as JVM, .NET, AAMP), calls to subprograms marked with Inline_Always that are declared within a generic instantiation are now inlined by default (without use of -gnatN).
Dec 5th, 2014
Implement NaN semantics for floating-point ‘Min/Max
In GNAT, Machine_Overflows is generally False for floating-point types, which means that operations such as 0.0/0.0 can generate NaN's. The Min and Max attributes have been enhanced to yield a predictable outcome in their presence: if either operand is a Nan, the other operand is returned; if both operands are NaN's, a NaN is returned.
Dec 2nd, 2014
New formal vectors both definite and indefinite
The API of formal vectors has been simplified for efficiency, and a new standard unit Ada.Containers.Formal_Indefinite_Vectors is defined to hold elements of an indefinite type, for example a classwide type. Both units can be used in SPARK code, and GNATprove then generates checks that the API is used correctly.
Dec 1st, 2014
Consistent casing of flow messages
The casing in flow messages now precisely matches the user's code.
Do not warn that ineffective Inline is redundant
Previously, if a pragma Inline was ineffective, and warn on redundant constructs was in effect (-gnatwr, included in -gnatwa), then a warning would be given that the Inline was redundant. This is not a helpful warning, and it is now suppressed.
S’Img is static for a static enum type expression
If the GNAT attribute 'Img is applied to a prefix which is of an enumeration type and is a static expression, then the result is static (and is the literal from the enumeration type). This works even if Discard_Names is in effect. This allows for example X'Img as the operand for External_Tag.