- Ada 2012
- Ada 2005 / 95 / 83
- Embedded Development
- Formal Methods
- Open Source
- Safety-Critical Development
- Static Analysis
Mar 30th, 2017
Globals of renamed subprograms in code not-in-SPARK
GNATprove now synthesizes more precise Global contracts for subprograms annotated with SPARK_Mode => Off that make calls via subprogram renamings. Such calls happen, for example, in instances of generic units with formal subprogram parameters.
GPS: Auto fix for prefix of Result attribute
GPS provides auto fix to help with compiler errors of the form 'incorrect prefix for attribute "Result", expected "Incr2"'.
GNATDOC: Documentation for concurrent constructs
Detailed information is generated for task and protected objects, including their subprograms and entries.
Mar 27th, 2017
Better messages for null statements
CodePeer flags both dead null statements and predetermined test conditions which govern the possible execution of null statements.
Mar 27th, 2017
GNATdoc can now extract documentation from bodies
GNATdoc has a new capability, activated by the command-line switch '-d'; in this mode, GNATdoc processes bodies and extracts documentation for library-level entities.
Mar 24th, 2017
Empty “others” alternative in Case statement
Flow analysis now detects when an "others" alternative of a Case statement corresponds to an empty range and effectively considers its sequence of statements as unreachable. This helps to avoid spurious messages about variables not being referenced or initialized within that sequence of statements.
Mar 24th, 2017
Automatic reordering of components in record types
The compiler can now reorder components in record types with convention Ada in order to fix blatant inefficiencies that the layout of components in textual order would bring about. The reordering is automatic and silent by default, but both characteristics can be toggled: pragma No_Component_Reordering disables it either on a per-record-type or on a global basis, while -gnatw.q gives a warning for each affected component in record types.
Mar 23rd, 2017
Relax alignment constraint for record extensions
On x86 and, more generally, architectures that do not require strict alignment for memory accesses, the compiler now accepts size clauses on record type extensions that effectively lower the alignment of the type, if there is also a representation clause on the type.
Mar 21st, 2017
Simplified translation of simple private types
Untagged private types with no discriminant whose full view is not in SPARK are now translated in Why3 as clones of the predefined __private abstract type. This should allow users of interactive proof assistants to more easily map these private types to a logic type of their choice.
GPS: The Window menu now contains icons
Icons were added in the Window menu for editors. This allows displaying which editors are currently modified.
Mar 20th, 2017
Theories for conversion of discrete types realized
The Why3 theories used by GNATprove to model conversions between discrete types have been realized in Coq. This increases confidence in their correction.
GNATCOLL.Traces performance improvements
Performance has been significantly enhanced: streams no longer flush after each message by default (though this is now configurable in the configuration file), locking is done at the stream level, and can often be avoided altogether since the system provides its own locking, messages are created as a whole line and then sent once to the stream, which provides more flexibility when writing streams, and other various enhancements. In a single threaded application, we now output 6 million messages per second to a file.
Mar 16th, 2017
GNAT includes a ZFP runtime for Linux and Windows
The native ZFP (Zero Footprint) runtime for Linux and Windows is now part of the base GNAT package. It is now also available with 64-bit compilers. This runtime is similar to the ZFP runtimes that are delivered with our bare metal products and can be used to test an embedded project in a native environment.
Mar 15th, 2017
Better messages for .scil file creation failure
If CodePeer unsuccessfully attempts to create a .scil file, then generate an additional error message which includes the full name of the file which could not be created. If it appears likely that the source of the problem is a Windows-specfic restriction on filename lengths, then that is also noted in a message.
GNATCOLL.Mmap: support files larger than 2Gb
This package now supports mapping files up to 1 petabyte, on 64 bits systems. This is backward compatible, although to access such large files you will need to use some different functions. This package also includes support for the madvise() system call on Unix systems, which might provide a 5% performance improvements when accessing files sequentially.
GNATCOLL.Strings: new package
This package, and the generic implementation in GNATCOLL.Strings_Impl, provide a new string type. A XString is similar to an unbounded string, but more efficient (up to 10x for strings 23 characters or less, or when manipulating substrings, and up to 1.4 for larger strings), and with a more extensive API.
GNATCOLL.Promises: new package
This package provides a promise type, also known as a future in some language. This is a way to perform background computation, then chain a series of callbacks which can themselves perform asynchronous computation.
Mar 13th, 2017
Option to treat run-time exception warnings as errors
The compiler supports a new switch -gnatwE that treats warnings that run-time exceptions will occur as compile-time errors.
Ada Web Server
Mar 11th, 2017
Add support for type/subtype in ada2wsdl
The tool ada2wsdl will now generate proper WSDL out of Ada specs using types or subtypes to derived from other Ada specs.
Mar 9th, 2017
New switch produces header in gnatprove.out
The new switch --output-header produces a header in the generated file gnatprove.out, with useful information about the run of GNATprove, such as the version number, date, host platform and switches used.
Extending a package from a project being extended
In an extending project A, it is now possible to extend a package P from the project being extended B, when project B is extending another project C and package P is not declared in project B but has only been inherited from project C.
Ada Web Server
Mar 7th, 2017
Add support for xsd:dateTime in ada2wsdl
The ada2wsdl tool will now generate a SOAP xsd:dateTime for references to the standard Ada.Calendar.Time.
Mar 4th, 2017
Ceiling locking on Linux without root privileges
Ceiling locking on Linux no longer requires root privileges. Instead, you can run "sudo /sbin/setcap cap_sys_nice=ep exe_file" to set the relevant capability on the executable file, and then that program can use ceiling locking without running as root.
Ada Web Server
Mar 4th, 2017
Add support for selecting encoding in ada2wsdl
The ada2wsdl tool has a new option to select the encoding to be used by the SOAP services.