- Ada 2012
- Ada 2005 / 95 / 83
- Embedded Development
- Formal Methods
- Open Source
- Safety-Critical Development
- Static Analysis
Jun 26th, 2015
Constant can now appear in contracts
The SPARK toolset now allows for constants with variable input to appear in flow-related contracts. This allows for more precise information flow analysis.
Jun 25th, 2015
Support for volatile functions
The SPARK toolset now correctly implements the semantics of the Boolean aspect volatile_function in both flow analysis and proof.
Jun 24th, 2015
Detect violations of language restrictions
The SPARK toolset now checks settings of the pragma Restrictions before analyzing the code; previously they were only checked by the compiler.
GPS: Navigation from race conditions report
CodePeer's Race contitions report allows to navigate to location of access to shared object in source code.
Jun 19th, 2015
Better progress bar in graphical interface
SPARK now provides better progress information when the --ide-progress-bar switch is used, so that the progress bar in graphical interfaces can convey this information to the user.
Jun 19th, 2015
Array comparison on reconfigurable runtimes
Comparison operations on arrays of discrete components are now allowed on ZFP and Ravenscar-SFP runtimes.
Jun 18th, 2015
Value of Runtime when—RTS= is specified
When --RTS= is specified for a language on the command line, the value of attribute reference 'Runtime (<language>) is the value specified by the switch --RTS=, even when attribute Runtime (<language>) has been declared.
Jun 18th, 2015
New restriction - No_Task_At_Interrupt_Priority
A new restriction No_Task_At_Interrupt_Priority has been implemented. It forbids pragma or aspect Interrupt_Priority on tasks. This restriction is enforced in Ravenscar for Cortex-M runtimes on the ARM-elf platform.
Jun 17th, 2015
Integration with Jenkins
A Jenkins plug-in is now distributed with CodePeer. It provides a Build Step to configure a run of CodePeer as part of a Jenkins build.
Jun 16th, 2015
Debug info for limited class-wide objects
The compiler now generates debug info for a limited class-wide object initialized by a function call.
Jun 15th, 2015
Add variables in gprinstall’s generated projects
Project generated with gprinstall will now contains global variables as found in the original project.
Restrictions to refine No_Implicit_Heap_Allocations
Two new restrictions have been added: No_Implicit_Task_Allocations and No_Implicit_Protected_Object_Allocations. They could be used to refine the wider No_Implicit_Heap_Allocations restriction.
UET_Address attribute removed
The unused and internal use only attribute UET_Address has been removed.
Jun 11th, 2015
Do not generate spurious discriminant checks
Discriminant checks were previously generated on all component accesses on discriminant records. These only correspond to an actual language check when the component is defined in a variant part. Thus, GNATprove has been improved to only generate these checks when mandated by the language.
GB: use selected project as project to convert
When running "convert to ada..." action, use current selected project as project to convert initial value.
Jun 10th, 2015
Sanitizer libraries on GNU/Linux native platforms
Native x86 and x86_64 Linux toolchains now come with a family of "Sanitizer" libraries that can help with the debugging or anticipation of various run-time misbehaviors in an application. The "Address Sanitizer" library, for example, tracks and reports memory management hazards such as buffer overruns (including on static arrays), multiple deallocations or memory leaks. Taking advantage of this library simply requires to compile and link with -fsanitize=address.
Jun 9th, 2015
Ada exception message in catchpoint condition
In the debugger, an Ada exception catchpoint can now be made conditional on the contents of the exception's message, whose content is available through a variable called "Message". For instance:
(gdb) catch exception if message = "EXCEPTION_ACCESS_VIOLATION"
For loops on type with Iterable aspect
The SPARK toolset now supports for loops on objects of types with the Iterable aspect specified. In particular, it is the case for loops on formal containers. Both iteration over cursors (for in) and over elements (for of) are supported.
Support for iterators on arrays
Iterators on arrays, both in loop statements and in quantified expressions, are now supported by GNATprove, except for the case of a quantified expression with an iterator over a multi-dimensional array.
Jun 7th, 2015
Better support for fixed-point division
The SPARK toolset now supports division of fixed-point values when the result type is integer and both operands have the same base type.
Jun 5th, 2015
Image function for dimensioned quantities
The package System.Dim.float_IO now includes a function Image, that provides a string representation of a dimensioned quantity, where the numeric value is followed by the declared symbol for the corresponding unit, or the expression that enumerates its dimensions.
Jun 3rd, 2015
Improve tracking of bounds on slice assignments
The SPARK toolset now tracks better the values of dynamic array bounds when assigning into a slice of an array, especially when this array is itself contained in a composite variable.
Jun 2nd, 2015
Better error recovery for misplaced access keyword
The compiler provides a meaningful error message when the keywords constant and access are interchanged in an access discriminant specification.
Jun 1st, 2015
Create a symlink for the versioned libraries
A symlink is now created on the main library directory for a library name with a version (Library_Version attribute).
Jun 1st, 2015
Suppressing checks in containers
Two new check names, Container_Checks and Tampering_Check, are added to allow suppression of checks in Ada.Containers packages. You can put:
pragma Suppress (Container_Checks);before an instantiation of (say) Ada.Containers.Vectors, and all checking code is removed. More importantly, all the controlled-type machinery involved with tampering checks is also removed. You can Suppress (Tampering_Check) to suppress just the tampering checks and machinery (which are the most expensive, and least effective at catching bugs). Suppress(All_Checks) and the -gnatp switch also work.