- Ada 2012
- Ada 2005 / 95 / 83
- Embedded Development
- Formal Methods
- Open Source
- Safety-Critical Development
- Static Analysis
Oct 29th, 2014
Windows GNAT.OS_Lib.Wait_Process improvement
On Windows the Wait_Process routine now follows the UNIX semantics more closely. The main improvement are:
- It is possible to have multiple tasks waiting for a child process to terminate. - When a child terminates, a single wait call will receive the corresponding process id. - A call to wait will handle new incoming child processes.
Oct 29th, 2014
Suppressing analysis via Annotate pragmas
By adding "pragma Annotate (CodePeer, Skip_Analysis);" at the start of the declaration list of a subprogram body or a package body, CodePeer's analysis of selected subprogram bodies can be suppressed. This is typically done in order to improve performance. For details, see CodePeer User's Guide section 2.4 ("Running CodePeer Faster").
Oct 24th, 2014
Better error locations for flow analysis
Flow analysis used to point at the export (Something) when it issued messages like
warning: incorrect dependency "Something => State"We now point at the incorrect dependency (State) instead.
Lower gnatls error code severity in some cases
In some common use cases, gnatls used to return error code 4 (fatal), which was unfriendly for analysis. Calling gnatls with no arguments or arguments "-h" or "-v" has been changed to return 0 (success).
GPS:—version and—help no longer require GUI
The switches are parsed before GPS attempts to connect to the GUI environment. As a result, it is possible to get the help or the version even when the environment is not setup for GUI.
Support for overriding keyword in Ada 95 mode
For compatibility with some Ada 95 compilers which support only the overriding keyword of Ada 2005, the -gnatd.D debug switch can now be used along with -gnat95 to achieve a similar effect with GNAT.
Oct 22nd, 2014
Win32Ada has some WinCrypt support
Some Windows WinCrypt routines has been added into the Win32Ada binding. They can be found into the Win32-WinCrypt unit.
Oct 21st, 2014
Mark Ghost functions in formal containers
Functions First_To_Previous, Current_To_Last and Strict_Equal introduced in units of the formal container library should only be used in contracts and assertions, as they are very inefficient. They are now marked as Ghost functions, which prevents use outside assertions and ghost code.
Oct 21st, 2014
Use of floating-point in fixed-point operations
In the presence of restriction No_Floating_Point, a multiplication of two fixed point quantities of the same fixed point type in an integer context does not generate conversions to floating-point for run-time evaluation.
Raise, no-return and statically-false assertions
Flow analysis now ignores all statements that inevitably lead to a raise statement, a statically-false assertion or a non-returning procedure. Additionally, all statements that follow a raise statement, a statically-false assertion or a non-returning procedure that are not otherwise reachable from the start of the subprogram are also ignored.
New implementation of Ghost entities
The SPARK toolset now implements the new semantic and legality rules of Ghost entities. This feature now encompasses objects, subprograms, packages and types. As a result, convention Ghost has been replaced with aspect Ghost.
Support for Runtime & Target attributes in projects
These two new attributes are now supported by GPS and should replace the use of the IDE'Gnatlist attribute to specify the same information.
Oct 15th, 2014
GPRslave control of simultaneous responses
A new option has been added to GPRslave to control the number of simultaneous responses (sending back object code and ALI files) supported. This was hard coded to 2, it is now possible to set this value between 1 and the maximum number of simultaneous compilations.
Oct 14th, 2014
Replay facility always reissue warnings
When a unit or the units on which it depends have not changed, GNATprove detects it and avoids re-analyzing the unit. This caused some warnings to be issued only the first time a unit was analyzed. Now, a new replay facility is used in GNATprove to always reissue warning and check messages when a unit is considered, even when it does not require re-analysis.
Oct 13th, 2014
Extend fast-path CDR marshalling to nested arrays
The fast-path CDR marsahlling circuitry, allowing efficient marshalling of common aggregates such as arrays of bytes or integers, has been extended to the case of nested arrays.
Runtime specific directories in the project path
For each non default runtime, there are now two more directories in the project path: <runtime_root>/lib/gnat and <runtime_root>/share/gpr, where <runtime_root> is either:
- <runtime> ifthe runtime is explicitly specified as an absolute path - <compiler_root>/<target>/<runtime> if the runtime is not explicitly specified as an absolute path
Project path depends on compilers
For tools gprbuild, gprclean and gprinstall, the project path depends on the compilers, not the prefix of the tool. For each compiler driver in a "bin" subdirectory, the compiler root is the parent directory of this "bin" subdirectory and the directories in the project path are, in order:
<compiler_root>/<target>/lib/gnat <compiler_root>/<target>/share/gpr <compiler_root>/share/gpr <compiler_root>/lib/gnat
New gprbuild option—complete-output
A new option --complete-output is added to gprbuild, allowed only on the command line and incompatible with option --distributed=. When this option is used, the standard output and standard error of the compiler are redirected to text files. When these files exist for a source that is up to date, their content is output to stdout and stderr.
Oct 13th, 2014
New function Non_Blocking_Spawn
A new function Non_Blocking_Spawn is added to GNAT.OS_Lib. This function redirects standard error and standard output to two different files.
Inlining of renamed subprograms
The compiler now supports inlining of renamed subprograms.
Inlining of unchecked conversion instantiations
Compiling with back-end inlining enabled the compiler supports implicit inlining of unchecked conversions defined in inlined subprograms (i.e. it is not necessary to add pragma Inline to instantiations of unchecked conversion defined in inlined subprograms).
GB: better scenario variables support
Scenario variables editor added capability to:
* set the variable for all projects * unset the variable for all projects to use GNAT project default valueScenario variables changes are taken into account immediately without having to restart GNATbench.
GB: add Ada/Environment preferences page
New Ada/Environment preferences page allows the configuration of the environment used when GNATbench launch any command.
Oct 7th, 2014
Support for POSIX binding shared library
Florist, the GNAT implementation of the standard Ada binding to the POSIX API, can now be built as a shared library by passing "--enable-shared" to its configure script.
Output of assumptions of verification results
The SPARK toolset now supports the option --assumptions. With this option, the tool outputs for each verication result in the result file gnatprove.out, the assumptions it depends on. Assumptions are properties which should hold for the verification results to be true, but which the SPARK toolset could not verify by itself. This can happen because the corresponding code is not in the SPARK subset or the verification of that code was not finished. Currently, output assumptions only include the assumptions on called subprograms of analysed subprograms, but not assumptions about the calling context of analysed subprograms.
Support for list of provers to try
The option --prover of the SPARK toolset has now been improved to allow a list of provers, e.g. the command line option --prover=altergo,cvc4 will first try to prove a VC with altergo, and if that fails, try again with CVC4. The same steps or timeout option applies to all provers.
GB: add support for “On File Change” builder target
A builder target having its launch mode set to "On File Change" will be automatically launched each time an ada file is saved. Wind River Workbench users can use this feature to have ada code analyzed as soon as it is saved. Builder target settings are accessible through Ada / Builder Targets preferences page.