- Ada 2012
- Ada 2005 / 95 / 83
- Embedded Development
- Formal Methods
- Open Source
- Safety-Critical Development
- Static Analysis
May 31st, 2014
Improved messages for duplicated case values
For a case statement over an integer type, if there are duplicated values that are given named constants, use the name of these constants in the error messages instead of the integer values.
GPS: Clear locations view for an individual file
New contextual menu added to clear Location View from messages for current file only. Corresponding action allows binding key shortcut.
May 29th, 2014
New “subprogram” field in CSV output
The CSV output now contains a new field to indicate the enclosing subprogram where the message is generated.
May 28th, 2014
Add support for large files on 32bit systems
Stream_IO and Direct_IO are now fully functional for files larger than 2GB on 32-bit based systems. Previously such files could be read or written, but positional operations (Set_Index, Index, Size) did not work correctly. Note that this changes some implementation-defined types, notably the declaration of Ada.Streams.Stream_Element_Offset, which may require some modification of clients using any of the streams related packages.
May 28th, 2014
Less false alarms regarding unused statements
Flow analysis used to issue one unused statement warning per unused record component. This is no longer the case. We now only emit a single warning when no record component is used in any way.
WB: quickfix support on Wind River Workbench
Quick fix feature is now available for errors created during VxWorks projects build.
May 23rd, 2014
New gnattest switch—test-duration
A new switch --test-duration is added to gnattest. This switch causes the generated test driver to print time measurement for each test.
GPS: Review key shortcuts dialog
This dialog can now be embedded in the main GPS window, and kept open. Changes are automatically changed (the save button was removed). A filter has been added to make it easy to find the proper action or shortcut. User-defined shortcuts are displayed in bold. The icons associated with actions are displayed, for consistency with the rest of GPS. Menus are no longer displayed in the dialog, since it is better to associate the shortcuts with the corresponding action instead. Multiple key themes are provided and can dynamically be switched (the emacs.py plug-in was removed and replaced with an Emacs key theme instead)
Better proof for bounds of unconstrained arrays
The SPARK toolset now tracks bounds of unconstrained arrays stored in local variables better, especially when they are modified in a loop. This results in more proved verification conditions.
Better proof for bounds of unconstrained arrays
The SPARK toolset now tracks bounds of unconstrained arrays better than before, especially when they are passed to a procedure with mode "in out". This results in more proved verification conditions.
Improved Look and Feel of GPS integration
The integration into GPS of the SPARK toolset is now closer to the integration of other tools. The localisation of messages of inlined subprograms and instantiated generics has also been improved.
May 21st, 2014
Record bind environment in executable
A new binder command line switch "-Vkey=value" is introduced, allowing information to be captured at application bind time. This information is incorporated in the application, and can be retrieved at run time using a new runtime library package GNAT.Bind_Environment. This can be used for example to record a build timestamp.
GPS: “file changed on disk” dialog review
The dialog that pops up when a file has been modified on the disk has been modified. It will now list all such files in a single dialog (as opposed to having one dialog per file when it gets the focus). There is now also an option for automatically reloading files (which can be undone).
pragma Warnings for proof results
Pragma Warnings is now fully supported by the SPARK toolset, in particular non-proved checks can be accepted using pragma Warnings (Off), just as was already the case for warnings related to flow analysis.
Use of “aliased” keyword now accepted in SPARK
Use of the "aliased" keyword in the declaration of an object, a parameter or a record or array component is now allowed in SPARK. What is still not allowed is to introduce aliasing by converting an address to such an entity into a pointer.
May 19th, 2014
New pragma/aspect No_Elaboration_Code_All
A new program unit pragma and corresponding aspect No_Elaboration_Code_All are added. This aspect applies the restriction No_Elaboration_Code to all parts of the extended main unit (spec, body, and subunits). In addition, it requires that any with'ed unit also have the No_Elaboration_Code_All aspect (thus providing a transitive guarantee that a unit and its dependents all have no elaboration code).
Improved pdf for GNAT user manuals
The pdf files for the GNAT User's Guide, GNAT Reference Manual, User's Guide supplements for Cross Platforms and High-Integrity Edition, GPRbuild, and GNATstack now are formatted so that the text occupies full-sized pages (versus the "small book" format used previously).
Bind some heap related routines in Win32Ada
The routines HeapSetInformation and HeapQueryInformation are now available in the Win32Ada binding.
GPS: Setting for background color of expanded code
It is now possible to change the color of expanded code lines in GPS.
gnatinspect recognizes IDE’Xref_Database
This attribute is used to specify the location of the xref database. It was so far only recognized by GPS, which set up the appropriate command line switches for gnatinspect. This attribute is now also recognize by gnatinspect itself, so that it creates the database in the right location.
Support functions with mutually recursive spec
The SPARK toolset now supports subprograms with mutually recursive contracts.
Fewer false alarms involving unreferenced vars
Flow analysis used to generates warnings about ineffective statements that involved variables which were marked with pragma Unreferenced. This is no longer the case.
May 14th, 2014
Better warnings on non-static protected objects
The compiler distinguishes between private components of protected types whose size depends on a discriminant, from those whose size depends on some other non-static expression. When restriction No_Heap_Allocation is in force, these two cases lead to different warnings.
GPS: New syntax highlighting engine
GPS has a new extensible syntax highlighting engine, that will be used for C, C++ and python by default, and is extensible in python, as documented in GPS user's guide.
GPS: New technology for documentation generation
GPS is now shipped with a new command-line tool for documentation generation, called gnatdoc. Amongst the features of GNATdoc are:
- support of Javadoc/Doxygen style of tags in documentation comments - support for comment placement detection - support for separating documentation comments from code comments - a new extensible HTML back-end - support for users defined image directory - support for package groups
May 9th, 2014
Better error recovery from bad aspect name
The error message from a bad aspect now includes the bad aspect name, and the recovery is better, avoiding missing useful additional messages, and avoiding unnecessary duplicated messages in -gnatf mode.
May 8th, 2014
More accurate analysis of overflow for division
The compiler now avoids setting the flag to check overflow on division in many cases where overflow is impossible. This eases proof of absence of run-time errors, and also allows the compiler to do a better job in some cases of detecting conditions whose result is known at compile time.
May 7th, 2014
Handles Library_Options in gprinstall
When generating a project for a library (standard or aggregate), gprinstall now adds into the generated Linker_Options the options that were into the Library_Options.
May 6th, 2014
New subprograms Import_Node and Adopt_Node
These subprograms, part of respectively DOM level 2 and DOM level 3, are now implemented, and can be used to move or copy one node from a tree to another. In addition, subprograms like Append_Child will now correctly complain when the new node was not created for the same tree.
GPS: change icon for root project in Project view
The icon for the root project is now different from that of other projects, to make it easier to spot the root project.
May 5th, 2014
Recognize Sqrt with a positive argument is nonzero
CodePeer now recognizes that a call to the Sqrt (square root) function (as defined in the predefined Generic_Elementary_Functions generic package) with a positive argument will return a result greater than zero, avoiding divide-by-zero messages when the result is used as a divisor.
May 3rd, 2014
Integer overflow checking now enabled by default
The default behavior of the compiler is changed so that integer overflow checking (as required by the Ada RM) is now enabled by default. A switch -gnato0 is added which disables integer overflow checking (thus reverting to the previous default behavior).