Fri 19 December 2014

[Adacore] More automated proof on conversions to float

Proof automation has been improved on code that converts between integers and floats.

Thu 18 December 2014

[Adacore] Linking with—lto=nn when -jnn and—lto are used

When gprbuild is invoked with -jnn (nn > 1) and with the linker switch --lto, the linker is invoked with --lto=nn to speed up linking.

Wed 17 December 2014

[Adacore] 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.

Tue 16 December 2014

[Adacore] 2014 Workshop on Spacecraft Flight Software

Dec 16-18, 2014 – California, USA

Tucker Taft gave a talk on "A Complete High-Integrity Software Development Stack".

Mon 15 December 2014

[Adacore] Subprograms without exports no longer ineffective

Flow analysis used to flag calls to subprograms without exports as ineffective. This is no longer the case.

Fri 12 December 2014

[Adacore] 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.

Thu 11 December 2014

[Adacore] Accept “alt-ergo” as prover name

An 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.

[Adacore] 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.

Wed 10 December 2014

[Adacore] 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.

Tue 09 December 2014

[Adacore] 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.

[Adacore] 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.

[Adacore] 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.