- Ada 2012
- Ada 2005 / 95 / 83
- Embedded Development
- Formal Methods
- Open Source
- Safety-Critical Development
- Static Analysis
doinstall script can be executed from any directory
The doinstall script, used to install GNAT on Unix hosts, can now be executed from any directory location. In particular, it is now possible to execute the script from a graphical tool such as a file explorer.
Link executables with -pie by default on Android
On Android, the compiler now links all executables as a Position Independent Executable (PIE) by default.
Sep 28th, 2015
Relaxed checking of restriction No_Dependence
The partition-wide check on restriction No_Dependence has been relaxed and no longer checks that this restriction applies to bodies of runtime units used by the application.
Sep 27th, 2015
GPRinstall now installs all sources by default
GPRinstall now installs all sources by default. To revert to the previous behavior the -m (minimal) switch has been introduced. Note that -a switch has been kept for compatibility reason but does nothing now.
Sep 25th, 2015
Examples from SPARK Book included in distribution
The SPARK distribution now packages the examples presented in the SPARK Book by McCormick and Chapin ("Building High Integrity Applications with SPARK"), in example directories called spark_book and thumper. A short description of both has been added to SPARK User's Guide.
Sep 25th, 2015
Warning on incorrect -W switch in pragma Warnings
The compiler now issues a warning if an incorrect or ineffective -W switch is passed to pragma Warnings.
Sep 24th, 2015
User mode support libraries for visium-elf
The visium-elf toolchain now comes with a user-mode variant of the libc, libm, and libgcc support libraries in addition to the supervisor-mode variant. The compiler still operates in supervisor-mode by default and selects the library variants from command line options at link time: user-mode libs with -muser-mode, supervisor-mode libs otherwise. The ZFP Ada runtime library comes as a single user-mode variant, so can be linked with either user or supervisor mode applications.
Sep 24th, 2015
New partitioning algorithm
CodePeer will now take into account the project file hierarchy (.gpr files) to create corresponding partitions when analyzing a large set of sources, grouping units in a more logical way.
Sep 24th, 2015
Generate symlink for library major version
GPRinstall now creates symlink for the library major version if needed.
Sep 23rd, 2015
New switch—level to adjust proof power
A new switch --level allows to set together the group of switches that control proof power, so that --level=0 corresponds to the fastest mode, and --level=4 corresponds to the most precise mode. The new default of switch --prover is now cvc4 instead of cvc4,altergo.
WB: add support for VxWorks 7
Add support for VWind River xWorks 7 & Workbench 4.4.x.
Sep 15th, 2015
Improved handling of array comparisons
CodePeer does a more precise comparison of strings and simple arrays, element by element if known. In the general case, the array comparison is now handled as a regular inlined operation rather than an unanalyzed call.
Sep 8th, 2015
Warn when -gstabs or -gstabs+ is used
GNAT no longer supports generating STABS debugging information for Ada. When STABS is explicitly requested while compiling Ada (through the -gstabs or the -gstabs+ command line options), a warning is now issued.
Sep 7th, 2015
Suppress more messages in messages min mode
Suppress more messages that are likely false positives when -messages min is specified. The newly suppressed messages include messages that depend on a variable modified in a loop where CodePeer is not able to compute its precise range, and messages that depend on array index or dereference not precisely tracked by CodePeer.
Sep 6th, 2015
More efficient code generated for object overlays
The code generated for overlays of variables, i.e. for variables subject to an address clause whose value is the address of another object, has been improved when optimization is enabled.
Sep 5th, 2015
More exhaustive warning on overlaid constants
The warning issued on overlaid constants now detects more cases.
Sep 1st, 2015
Improved support for machine code insertions
Machine code insertions written for use with other compilers may contain constructs which the GNAT compiler would not normally accept (e.g., uses of the "Ref" attribute in ways that are inconsistent with GNAT's definition of that implementation-defined attribute). Formerly, this would be treated as a semantic error and CodePeer would be unable to analyze the unit. Such machine code insertions are accepted now, thereby allowing analysis of the containing unit.