- Ada 2012
- Ada 2005 / 95 / 83
- Embedded Development
- Formal Methods
- Open Source
- Safety-Critical Development
- Static Analysis
GPS: new Debugger Variables view
This view displays the same type of information as the Data Window (i.e. the value of variables) but in a tree, which might help keep things organized.
Apr 28th, 2016
Further improved unchecked conversion analysis
CodePeer now knows more about unchecked conversions involving fixed point types and enumeration types.
pragma Implicit_Packing for composite components
Pragma Implicit_Packing now works for record types that contain components of small composite types, in particular small record types.
pragma Implicit_Packing for byte-packed array types
Pragma Implicit_Packing now works for array types whose component type is a scalar with a size multiple of the storage unit but not a power of 2.
Task switching while debugging a core file
It is now possible to switch between Ada tasks when debugging a core file.
Faster access to small byte-packed array types
The code generated for accessing packed array types whose component type is a small record with a size multiple of the storage unit has been improved.
GPS: proposed value of message review status
In CodePeer message review dialog proposed value of message review status has been changed to current status of the message.
Apr 21st, 2016
Better default for GPS message review dialog box
When the "CodePeer message review" dialog box comes up in GPS, the default value for the "New status" field is no longer unconditionally "Unclassified", but is instead equal to the "Current status" field. In the case of a subsequent review of an already-classified message, this means that the default action is to preserve the current status of the message as opposed to setting the status back to "Unclassified".
New pragma Unused
When applied to an entity, pragma Unused causes each read or write attempt of the entity to be flagged as a warning.
Added GNATcheck usage example
An example demonstrating the use of GNATcheck coding standard verifier has been added to the distribution.
Apr 17th, 2016
More flexible elaboration rules with static model
GNATprove now implements a more flexible enforcement of SPARK elaboration rules, that does not always requires Elaborate_All for calls and reads of subprograms and variables defined in other units during elaboration. Specifically, when the static elaboration model of GNAT is used (i.e. when neither switch -gnatE nor pragma Elaboration_Checks (Dynamic) are used), the more powerful mechanism of the compiler is used to compute a safe elaboration order for calls across units during elaboration, and GNATprove only requires the use of Elaborate_Body on units that modify the value of library-level variables defined in the spec during the elaboration of the unit body (SPARK RM rule 7.7.1(5)).
Improving handling of User_Data
The following generic packages were modified:
Gdk.Event.Handler_Set_User_Data Gtk.Action_Group.Set_Translate_Func_User_Data Gtk.File_Filter.Add_Custom_User_Data Gtk.Widget.Add_Tick_Callback_User_DataThe Notify parameter was removed from the public API. Instead, GtkAda will call the Destroy procedure to release User_Data.
GPS: use Gtk dialog for open/save files
GtkFileChooserDialog used instead dialog of GPS if system doesn't have own dialog or this forbidden in a preferences and it is local file system. It is possible to use a dialog of GPS by turn off gtk_file_selector trace setting.
GPS: automatic fix for adding Elaborate_All pragma
The GPS code fixing capability was enhanced to handle compiler messages such as "Elaborate_All pragma required for NAME". To fix this GPS will add pragma Elaborate_All (NAME) after corresponding with-clause in the spec or body of given compilation unit.
Temporary config project with autoconfiguration
The Project Manager now creates a temporary configuration project file when in auto-configuration. This file is deleted when the tool terminates. This allows several project-aware tools invocations to work in parallel with the same object directory.
Apr 13th, 2016
Tighter array packing for small record component
The packing of array types subject to aspect/pragma Pack and whose component type is a small record, either that contains another small record component, or that has a size in the range 33 .. 63 bits, has been improved.
Apr 12th, 2016
Exclude source directories from analysis
A new project attribute Excluded_Source_Dirs in package CodePeer is available to easily exclude entire source directories from analysis.
GPS: Add the possibility to filter switches
Switches defined for a specific tool using XML can now be filtered by specifying a named filter for the 'filter' attribute of a switch tag. These filters can be either predefined in GPS or created by the user (see the <filter> tag in the XML files). Use the GPS.Filter.list static method to list all the registered named filters.
Creating baseline from previous runs
It is now possible to set a previous run as the default baseline review by allowing the -baseline or -set-baseline-id switches in -output-only mode.
Improved handling of baseline reviews
A project now has a single baseline review, which will be used by default for all review comparisons. It can be set to the current review using the -baseline switch or set to a previous review using -set-baseline-id. Note that the default review can still be temporarily overwritten by using the -cutoff switch.
Apr 7th, 2016
More options for reporting of results
The --report switch of the gnatprove tool now provides one more option to select from. If the option --report=provers is selected, gnatprove will show information about which provers have contributed to the proof of each check.
GPS: different icon for disabled breakpoints
The icons that are displayed on the side of editors to show where breakpoints are now have a different color when the breakpoint is disabled or is conditional.
GPS: speed up search and replace
The "search and replace all occurrences" has been sped up by a factor of seven in some cases.
GPS: do not highlight occurrences of keywords
The plug-in auto_highlight_occurrences.py highlights all occurrences of the word under the cursor in the whole file (possibly using smart cross reference information to only highlight the specific entity and not its homonyms). This plug-in has now learned not to highlight the language's keywords ("constant", "begin",...) which is useless and might be slow since these keywords generally occur often.
GPS: Home goes to beginning or first-non-blank
When using the Home key while in an editor (or any key bound to the action "beginning of line"), GPS will first go to the first column (as it has always done), but if you do it a second time it will then go to the first non-blank character of the line). This is a feature available in other code editors.
GPS: Support for arm-sysgo-pikeos
GPS now supports the arm-sysgo-pikeos toolchain.
Optimization of Unbounded_Priority_Queues
The efficiency of Ada.Containers.Unbounded_Priority_Queues has been improved, especially in the case where many same-priority items are enqueued.
Improved warning on absolute address clauses
The alignment warning issued on strict-alignment architectures for address clauses whose value is an absolute address is now more accurate, catches more cases and prints the alignment value.
New procedure Get_Closures
A new procedure GPR.Util.Get_Closures is added. It allows to get the full paths of the sources in the Ada closures of one or several mains.
Apr 1st, 2016
Expanded support for incomplete types in profiles
The support for incomplete types as parameter and result types introduced in Ada 2012 has been implemented for a broader range of types.