- Ada 2012
- Ada 2005 / 95 / 83
- Embedded Development
- Formal Methods
- Open Source
- Safety-Critical Development
- Static Analysis
Support optional refinement in private part/child
SPARK Reference Manual now allows refinement through the user of pragma or aspect Refined_Global and/or Refined_Depends in scopes where the full refinement of an abstract state is not visible, like the private part of the package defining the abstract state, or one of its child packages. The special rules in SPARK RM 7.2.4 for this so-called optional refinement are now supported in GNAT and GNATprove.
Global variables known to be initialized in loops
GNATprove now knows that in out global variables and parameters that are modified in loops are always initialized and thus are in their types. In particular, variables are in their range for scalars and their dynamic predicate is true if they have one.
Jun 3rd, 2016
Suppressed wrong warning message for X’Address
SPARK does not look at X in X'Address as a used variable anymore and therefore it does not emit a warning message in case X is not initialised.
New atomic operations are provided, that change the value of an Atomic_Counter if, and only if, it currently has a given known value. This is useful to write lock-free algorithms.
Jun 3rd, 2016
gnattest: stub parent packages
Gnattest now generates stubs for parent packages of packages undet test in --stub mode.
unicode names from the Unicode 8 standard
The unicode-names-* packages were updated to match the Unicode 8 standard. The new bindings are generated via a new importer, which fixes a number of issues with the previous bindings:
- some characters were put in the wrong block (and thus wrong package) - some typos due to incorrect parsing of the Unicode files - some name aliases would hide canonical names occurring later (for instance 1F5E2 was hidden by 1F48B) - some unofficial aliases were used (Bell is not long valid, for instance)This change is not fully backward compatible, due to changes in the Unicode standard itself, since some blocks were renamed, as well as some characters. Contributed by Nicolas Boulenguez
Jun 1st, 2016
Improved version of attribute Type_Key
The attribute Type_Key, which is provided for compatibility with the APEX attribute of that name, now uses a CRC computed from the type declaration of the type, and the declaration of all its components, to provide a reliable signature that allows the detection of changes in the semantics of the type.