Mon 25 May 2015

[Adacore] New gnatcheck rule - Maximum_Parameters

A new rule named Maximum_Parameters is added to gnatcheck. It checks if a subprogram has more formal parameters than are specified by the rule parameter.

Fri 22 May 2015

[Adacore] Suppress no effect warning when user already knows

The SPARK toolset no longer emits a "subprogram Bla has no effect" warning when the user has added a Global/Depends aspect on Bla since this indicates that the effects of the subprogram are already known to her. The message is also suppressed when Bla is marked No_Return and is deemed to abnormaly terminate.

Thu 21 May 2015

[Adacore] Change of runtimes on powerpc-elf bareboard

The runtimes provided for powerpc-elf bareboard now runs on mpc8641 platforms instead of PReP. The former platform is still available, high performance while the latter has been deprecated for more than 10 years. The GNATemulator product has been updated too.

[Adacore] Lift restriction on calls to No_Return procedures

This lifts the SPARK RM restriction forcing calls to procedures marked No_Return to appear either at the end of a subprogram or as the only statement inside an if-statement without else/elsif part. Indeed, this restriction is not needed anymore, similarly to what was done for raise-statements already.

Wed 20 May 2015

[Adacore] Do not issue spurious warnings with—limit-subp

When analyzing a single subprogram (typically with 'Prove Subprogram' or 'Prove Line' in an GPS or GNATbench), spurious warnings were issued on justification pragmas (pragma Annotate(GNATprove,...)) in other subprograms. This is no longer the case.

Tue 19 May 2015

[Adacore] Static object allocation with complex static size

The compiler can now statically allocate objects declared at the library level and whose static size depends on a constant whose value is taken from a static array aggregate indexed by a character or enumeration type, as was already supported for an integer index type.

Mon 18 May 2015

[Adacore] GNATCOLL.Refcount: new package Shared_Pointers

A new implementation for reference counted types is provided. It provides a more flexible API than the Smart_Pointers (since the Element_Type does not need to be a tagged type derived from Refcounted), and is faster, thanks to the use of storage pools. The API is safer since Get now returns a reference type rather than a direct access to the element. This new package is used throughout GNATCOLL, in particular GNATCOLL.SQL. In general, this has no effect on existing code.

Fri 15 May 2015

[Adacore] More examples distributed with the release

The examples distributed with the release now include 7 small examples (a few dozen slocs), 20 medium-size examples (a single unit of a few hundred slocs at most) and 7 larger examples (of a few hundreds or thousands slocs). These examples include for example the 'Autopilot' case study distributed with John Barnes's books on SPARK 2005 and the well-known 'Tokeneer' case study commissioned by the NSA, both translated to SPARK 2014. See section 6.9 of the SPARK User's Guide 'Examples in the Toolset Distribution' for details.

[Adacore] TCP/IP in SPARK distributed as example

An implementation of TCP/IP in SPARK is distributed now in the 'examples' of the release. This implementation based on LWIP design is targeted at bare-board embedded applications in certifiable systems. Data dependency contracts are given for most subprograms. These contracts are proved by GNATprove flow analysis, which also proves the absence of reads of uninitialized data. See the description of this example in section 6.9 'Examples in the Toolset Distribution' in SPARK User's Guide, or the README in ipstack directory.

[Adacore] Allow manual proof of parts of Checks

Previously, it was not possible to run a manual prover on a VC that represents part of a check, i.e. that was obtained by option --proof=progressive. This is now possible.

Wed 13 May 2015

[Adacore] Linux Monotonic_Clock enhanced

The tasking Monotonic_Clock has been reimplemented with the function clock_gettime() vice gettimeofday().

[Adacore] Android Monotonic_Clock enhanced

The tasking Monotonic_Clock has been reimplemented with the function clock_gettime() vice gettimeofday().