Fri 21 November 2014

[Adacore] GPRinstall new—no-build-var option

A new option --no-build-var has been introduced and is meant to be use for project with a single configuration (single installation). In this case there is no build/scenario variable generated.

Thu 20 November 2014

[Adacore] New directories in project path for gnatls—RTS=

Two new directories are added in the project path, when gnatls is invoked with --RTS=, just before the two directories for the target. When the runtime is a single name, the directories are:
  <prefix>/<target>/<runtime>/lib/gnat
  <prefix>/<target>/<runtime>/share/gpr
Otherwise, the runtime directory is either an absolute path or a path relative to the current working directory and the two added directories are:
  <runtime_directory>/lib/gnat
  <runtime_directory>/share/gpr

[Adacore] Do not trust Elaborate in SPARK

In normal GNAT static elaboration mode, a pragma Elaborate is trusted to be sufficient, and the use of such a pragma disables the static checking. In SPARK mode, the pragma Elaborate is allowed, but it is not trusted to be sufficient, since this cannot be verified at compile time. This means that we may require Elaborate_All even if a pragma Elaborate is present.

[Adacore] Actual parameters with property Async_Writers

Actual volatile parameters with enabled external property Async_Writers can now appear in procedure calls where the corresponding formal is of mode OUT.

Wed 19 November 2014

[Adacore] Managing Avionics Safety Certification in UAS Platforms

Safety certification for avionics hardware and software is an expensive, complicated process, but absolutely necessary to ensure safe skies for commercial aircraft passengers and military jets flying in the national airspace. Now unmanned aircraft flight critical electronics will also have to meet these same safety requirements as the U.S. Federal Aviation Administration (FAA) starts to open up the national airspace to unmanned aerial systems (UASs). While the rules are still being drawn up, embedded software and hardware designers are already looking at ways for UAS platform integrators to solve certification challenges and manage the process of compliance with safety certification standards such as DO-178B & C. This webcast of industry experts will discuss how to enable safety certification of UAS platforms through efficient and cost-effective solutions.

[Adacore] Managing Avionics Safety Certification in UAS Platforms

Safety certification for avionics hardware and software is an expensive, complicated process, but absolutely necessary to ensure safe skies for commercial aircraft passengers and military jets flying in the national airspace. Now unmanned aircraft flight critical electronics will also have to meet these same safety requirements as the U.S. Federal Aviation Administration (FAA) starts to open up the national airspace to unmanned aerial systems (UASs). While the rules are still being drawn up, embedded software and hardware designers are already looking at ways for UAS platform integrators to solve certification challenges and manage the process of compliance with safety certification standards such as DO-178B & C. This webcast of industry experts will discuss how to enable safety certification of UAS platforms through efficient and cost-effective solutions.

[Adacore] Ignore Suppress (Elaboration_Check) in SPARK

In normal GNAT mode, Suppress (Elaboration_Check) disconnects the normal static elaboration mode circuitry. We don't want that in SPARK, where the elaboration rules are important static legality rules that must not be compromised. So in SPARK mode, we ignore the attempt with a warning.

Tue 18 November 2014

[Adacore] Require Elaborate_All for SPARK mode variable ref

In SPARK mode, a variable reference to a variable in another package requires an explicit Elaborate_All call, and this is now implemented. Note that the current SPARK manual specified this is only required for read/write references, so the rule implemented is more restrictive. It is not clear exactly what constitutes a read/write reference, which is why the more general, more easily stated, rule is implemented.

Mon 17 November 2014

[Adacore] Tune options for CVC4

The options used for CVC4 have been tuned, so that more VCs are discharged automatically.

Sun 16 November 2014

[Adacore] Require pragma Elaborate_All in SPARK mode

In SPARK mode, we always operate in the static elaboration mode, but we do not generate implicit Elaborate_All pragmas; instead we require such pragmas to be explicitly present. This requirement is now implemented

[Adacore] Handle aspects before initialization expression

Aspect specifications belong after the initialization expression in an object declaration, not before, but the compiler now accepts them before with a clear error message

Fri 14 November 2014

[Adacore] gnatpp:&#8212;split-line-before-op

The --split-line-before-op switch is added to gnatpp. If it is necessary to split a line at a binary operator, by default the line is split after the operator, as always. With this option, it is split before the operator.