- Ada 2012
- Ada 2005 / 95 / 83
- Embedded Development
- Formal Methods
- Open Source
- Safety-Critical Development
- Static Analysis
Jul 30th, 2017
More accurate C binding for enumerals and constants
The C and C++ bindings generated by means of the -fdump-ada-spec option can now use a more accurate Ada type for enumeral types and support the declaration of const-qualified variables.
Directory of gprbuild added to the PATH
When gprbuild is invoked, it now adds the directory of its executable to PATH, so that gprconfig can be found when using auto-configuration.
Jul 24th, 2017
Efficient array reset for all elementary types
The compiler now generates efficient code to reset a large array of any elementary component type to zeros, or an equivalent value for the component type, so now includes arrays of floating-point and access values instead of being limited to arrays with a discrete component type.
Jul 21st, 2017
Conversion between arrays with different components
GNATprove now supports conversion between array types with different component types as long as the component types are statically matching (as allowed by the Ada RM).
Jul 21st, 2017
Pragma Ada_2020 can be used to enable Ada 2020 features that have been implemented in GNAT. Ada_2020 is a configuration pragma. This is in addition to the -gnat2020 command-line switch.
Jul 19th, 2017
Automatically unroll static loops w/o loop invariant
Loop invariants are a known difficulty for beginners to use formal program verification. At the same time, many loops written in exercises and to familiarize oneself with the technology have static bounds and a small range. This enhancement implements loop unrolling for such loops with static bounds and not too many iterations (current threshold is at 20 iterations maximum). This way, simple loops with static bounds are proved without requiring a loop invariant. We let the user decide if she wants to use this feature or not: - by only unrolling FOR loops that have no loop (in)variant. - by disabling this feature when the switch --no-loop-unrolling is used.
Object files in alphabetical order in libraries
To be able to reproduce the same executable and libraries on different machines, the object files are put in libraries in alphabetical order of their path names.
Jul 11th, 2017
New gnatcheck rule Downward_View_Conversions
This rule flags downward view conversions.
Jul 10th, 2017
New gnatcheck rule Printable_ASCII
This rule flags characters in source code that are not part of the printable ASCII character set.
Jul 7th, 2017
New gnatcheck rule No_Inherited_Classwide_Pre
This rule flags a declaration of an overriding primitive operation of a tagged type if at least one of the operations it overrides or implements does not have any (explicitly defined or inherited) Pre'Class attribute defined for it.
GPS: New API to create nested messages
A python method create_nested_message has been added to the GPS.Message class, to create nested messages.
Jul 3rd, 2017
New gnatcheck rule Specific_Pre_Post
This rule flags each Pre and Post aspect that is a part of an explicit declaration of a primitive operation of a tagged type. Pre'Class and Post'Class aspects are not flagged.
GPS: Auto fix for Range attribute usage
The compiler is clever enough to detect that the Range attribute should be used to loop over the content of an array. GPS now offers an autofix for such warnings.
Improved gprconfig performance
Gprconfig performance substantially improved by caching results of all external calls.