- Ada 2012
- Ada 2005 / 95 / 83
- Embedded Development
- Formal Methods
- Open Source
- Safety-Critical Development
- Static Analysis
Apr 29th, 2014
Limit SAL content to the closure of the interface
When using gprbuild to build a Stand-Alone Library, only the closure of the Ada interface is compiled, bound and put in the library file.
Apr 26th, 2014
Valid_Scalars attribute for variant record types
The 'Valid_Scalars attribute can now be applied to variant records, and it correctly checks just the variant fields that are present. Note that it is not legal to use 'Valid_Scalars on Unchecked_Union records (or on any type that recursively has an Unchecked_Union component).
Apr 23rd, 2014
The Translator now converts squized assertions
The translator now converts the following contract:
while cond --# assert inv; loopinto:
loop pragma Loop_Invariant (inv); exit when not (cond);
Secondary stack reclamation during elaboration
The compiler now reclaims the storage used by the secondary stack during the elaboration of a library level object declaration when the initialization expression contains a function returning a controlled or unconstrained result.
gnat2xml generates representation clauses
A new switch --rep-clauses causes gnat2xml to generate representation clauses for certain types. Size and Component_Size clauses, as well as record_representation_clauses, are generated as appropriate. These may be used to see the representation the compiler has chosen.
Apr 19th, 2014
New gprinstall option to copy only project sources
Using gprinstall's --sources-only option it is now possible to install projects sources only. In this mode it is not required for the project to have been built before.
Apr 18th, 2014
Better provability of checks on floats
GNATprove now analyzes type bounds of sub-expressions to compute when an overflow check or a range check cannot fail, because these bounds guarantee that the resulting bounds on the result fit into the required range. As a result, many run-time checks on floats that were previously not proved become proved.
Apr 18th, 2014
Implement workaround for FPU store errata on LEON3
The compiler switch -mfix-ut699 has been enhanced to work around the store forwarding problem of the FPU in Aeroflex Gaisler's LEON3 Microprocessor.
Apr 17th, 2014
New warning on equality of Unchecked_Union objects
The compiler emits a warning on an equality when the operands are of an Unchecked_Union type and their discriminants cannot be determined statically, resulting in a Program_Error exception being raised.
Apr 16th, 2014
Debugger support for variable length arrays in C
The debugger has been enhanced to print the value of C variable length arrays correctly. The sizeof operator now also prints the correct value.
Apr 15th, 2014
Support contextual analysis of local subprograms
GNATprove can now analyze local subprograms without contracts in the context of their calls, as if their body was inlined. This makes it possible to get a very precise analysis, without requiring that the user writes a contract on these subprograms.
Apr 14th, 2014
Warn on postconditions for No_Return Subprograms
The only postcondition that makes sense for a subprogram labeled as being No_Return (using the pragma of that name) is an explicit False test. Any other postcondition is useless and suspicious. A warning (under control of -gnatw.t/-gnatw.T) is now given for such useless postconditions.
Apr 13th, 2014
gnatcheck now supports the --incremental switch, similarly to gnat2xml and gnatpp. --incremental invokes incremental processing on a per-file basis. Source files are only processed if they have been modified, or if files they depend on have been modified. This is similar to the way gnatmake/gprbuild only compiles files that need to be recompiled.
Apr 12th, 2014
Add a time-stamp in all gprslave’s message
All gprslave's messages are now prefixed with a time-stamp in verbose mode. This will help tracking down possible issues with the slave.
Apr 11th, 2014
A new switch -gnateC is introduced, providing a compiler-like behavior to analyze files one by one quickly, with no global analysis and no database. This switch should be used by calling directly codepeer-gprbuild with --codepeer -gnateC.
Apr 11th, 2014
New implementation of Ada.Task_Attributes
The package Ada.Task_Attributes has been reimplemented, taking advantage of RM permission C.7.2(28), and putting a maximum number of task attributes supported to simplify the implementation and make it more efficient (the limit is 32 on most platforms). In addition, a special case is made for task attributes holding an address/pointer-sized object (or something smaller) and whose Initial_Value is 0 (or null for access types) which is more efficient and doesn't require the use of an indirection (and therefore, no extra dynamic memory allocation, and no locking). In addition, Ada.Task_Attributes now supports also foreign threads (created outside Ada).
Apr 8th, 2014
Contracts of functions available in assertions
An axiom is now generated for contracts of non-recursive normal functions. As a consequence, the contracts of non-recursive normal functions is now available for proof even if the function is called in a contract or an assertion.
GPS: Show “withs” in Outline view
New filter in Outline view enables visualization of with-clauses in current compilation unit to find them easier among unsorted clauses and comments.
Apr 7th, 2014
Improved parallelism for proof
GNATprove is now able to better parallelize proof attempts. This results in better performance of GNATprove on multi-core systems, when the switch -j is used.
Apr 4th, 2014
Use of box symbol in attribute ‘Update
The use of box symbol <> anywhere in the expression of attribute 'Update is forbidden.
Apr 4th, 2014
Compilation date and time are now available
The compiler now prints the compilation time in -gnatv or -gnatl mode (suppressible with debug flag -gnatd7). It also provides new functions in GNAT.Source_Info to obtain the compilation date and time (in a form compatible with the use of the C macros __DATE__ and __TIME__). Finally a new function System.OS_Lib.Current_Time_String is introduced (and used by the compiler to implement this functionality).
GPS: Implement auto-refresh mode for memory view
The memory view is now refreshed automatically during debugging sessions. Changed pieces of data are hightlighted. This feature can also deactivated via a preference.
Apr 2nd, 2014
Short message when main library project up to date
When the main project is a library project and is up to date, gprbuild instead of running silently now displays a short message such as:
"libmain.a" up to date "libmain.so" up to date
Improved run time performance for large array reset
The compiler generates faster code to reset a large array of integers to 0 by means of an aggregate with a single Others choice and, more generally, to set a large array of storage units to a single value by the same means.
gnatstub can generate subunits for body stubs
A new option '--subunits' is added to gnatstub. It allows to generate subunits for body stubs.
New package GNAT.Formatted_String
A new package GNAT.Formatted_String (file g-forstr.ads) provides a C/C++ printf() like formatted string support. Some generic routines are provided to be able to use types derived from Integer, Float or enumerations as values for the formatted string.
Additional use of Constrained attribute documented
In addition to the usage of this attribute in the Ada RM, GNAT also permits the use of the 'Constrained attribute in a generic template for any type, including types without discriminants. The value of this attribute in the generic instance when applied to a scalar type or a record type without discriminants is always True. This is now properly documented (the feature has been implemented for a while but not documented). This provides compatibility with some older Ada 83 compilers (notably DEC Ada).
Inheritance of variables in extending projects
Variables declared in project being extended are now inherited in the extending project: a variable V declared in a project A that is extended by a project B may be referenced as V in project B or as B.V in any other project that imports B.