- Ada 2012
- Ada 2005 / 95 / 83
- Embedded Development
- Formal Methods
- Open Source
- Safety-Critical Development
- Static Analysis
Jun 30th, 2016
New attribute Finalization_Size
When applied to an object or definite type, attribute Finalization_Size returns the size of any hidden data reserved by the compiler to handle finalization related actions. Note that only heap-allocated objects contain such hidden data.
Jun 28th, 2016
Simplify display of modular expressions
CodePeer now replaces "A mod K" with simply "A" when it is part of a larger expression that has an enclosing "mod K" operation, since a final "mod" operation is all that is required to faithfully represent the result of a tree of arithmetic operations on a modular type.
Jun 28th, 2016
Relative delays added in GNAT_Extended_Ravenscar
Relative delays are now supported by ravenscar-full runtime on bareboard platforms.
GPS: OpenOCD support to flash/debug boards
GPS now supports OpenOCD in order to flash and/or debug an external board. In order to use OpenOCD, set the IDE'Connection_Tool project attribute to 'openocd' and specify a board-specific OpenOCD configuration file via the IDE'Connection_Config_File project attribute (boat attributes are editable in the 'Embedded' Project Properties editor page).
Jun 23rd, 2016
New check_all mode for GNATprove
GNATprove now has a new mode for running the SPARK tools. This is the check_all mode, in which a full check of SPARK legality rules is done.
GPS: remove settings to auto-resize omnisearch
The omnisearch (i.e. the search box at the top-right corner of the GPS window) had a setting to automatically resize the popup window vertically. Unfortunately, due to limitations in the gtk+ toolkit in computing the ideal size of a window, this never worked correctly. This setting has thus been removed, and the window will now always occupy the full height of the GPS window.
Jun 23rd, 2016
Improved exception propagation on cert
For cert, ravenscar-cert and ravenscar-cert-rtp runtimes, a new mechanism to propagate exception is now used: backend SJLJ. This is more efficient than the previous mechanism.
New builtin function Split
A new builtin function Split is introduced. It takes two string parameters and returned a string list. Examples: Split ("-gnatf,-gnatv", ",") => ("-gnatf", "-gnatv") Split (external ("COMP_FLAGS", "-gnatf,-gnatv"), ",")
GPS: new menu /File/Save More/Projects
The menu /Project/Save All was moved to a new location to make its semantics easier to understand.
gprbuild switch -v is now equivalent to switch -vl (low verbosity) instead of -vh. And invoking gprbuild with -v or -vl no longer outputs information about the inner behavior of gprbuild.
New pragma/aspect Max_Queue_Length
When applied to a protected entry or entry family, pragma Max_Queue_Length restricts the maximum callers per entry.
Gold linker is available on native Linux
The gold linker is now available on native Linux platforms. It can be selected (instead of the default bfd linker) using linker switch -fuse-ld=gold. This linker is faster than the bfd linker.
A new gprbuild switch --build-script= is added, to create a shell script that would allow to repeat the same build with the same sources, provided that the temporary files created in the invocation of gprbuild are not deleted.
GPS: new function GPS.Entity.instance_of
A new python function is now available to find the generic entity that the current one instantiates.
No_Elaboration_Code for Ada.Unchecked_Conversion
Units Ada and Ada.Unchecked_Conversion have pragma No_Elaboration_Code_All, so these units can be with-ed from user units with that pragma.
Improved support for new socket options
GNAT.Sockets now has built-in support for Linux specific option Busy_Polling (SO_BUSY_POLL) when the compiler and runtime library are built on a recent enough host. Options not available at compiler build time can also now be set through a generic mechanism (Generic_Option).
Jun 16th, 2016
Improved info messages on objects initialization
Now we emit info messages for every constituent of an abstract state, including protected objects. Also, we only emit info messages on initialized objects if they are mentioned in an Initializes aspect.
Environment variable GPR_RUNTIME_PATH
When the Ada runtime directory is specified with switch --RTS or attribute Runtime ("Ada") as a relative path, the path may be relative to the project directory of the main project, or if the environment variable GPR_RUNTIME_PATH is defined to the path specified by the value of this environment variable.
Jun 15th, 2016
Entry guards are now taken into account
GNATprove now also takes into account the boolean expression provided as a guard of an entry of a protected type. This was previously not the case.
GPS: remove lines-with-code preference
GPS no longer supports the debugger preference to show lines with code. This preference has been disabled by default for a while now, and can be slow to run since it requires a lot of interaction with the debugger (and while the debugger is working on getting us the info, we can't send other commands like setting breakpoints). It also required extra space on the left of editors to display the info. As part of the simplification of the code, we removed the source_lines_revealed hook.
GPS: setting breakpoints before debugger starts
It is now possible to set breakpoints even before a debugger is started. This can be done as usual via the Debug/Set Breakpoint contextual menu, or by clicking on the side of editor lines. These breakpoints will be set automatically when a debugger is started. The permanent breakpoints are now saved and restored for every executable in the project, not for each executable individually. Lines with breakpoints now highlight the line number, and no longer display a red dot on the side of the line. Clicking on the line numbers toggles breakpoints on and off.
Ada Web Server
Jun 10th, 2016
Add support for generating document style WSDL
The tool ada2wsdl will now generate document style WSDL when passed the -doc option.
gprbuild default output
The default output of gprbuild is now synthetic, without any abridged commands to invoke the compilers, binder or linker. Example: $ gprbuild prj.gpr Compile [Ada] main.adb Bind [gprbind] main.bexch [Ada] main.ali Link [link] main.adb
GPS: display basenames in Project view
The Project view has gained a new configuration, to display only the basenames of the directories. So now if you have a project file at /some/path/file.gpr and one source directory at /some/path/sources/src1/, you can choose to display any of the following in the Project view:
/some/path/sources/src1/ (not showing basenames, and absolute paths) sources/src1/ (not showing basenames, and relatied paths) src1 (showing basenames)
GPS: improve debugger call stack view
This view now has a local configuration menu to chose which information should be displayed. When you chose not to show subprogram parameters, gdb is configured so that it also does not try to compute them, which on some systems might significantly speed up operations with the debugger.
GPS: new python function GPS.Debugger.breakpoints
GPS now exports the list of breakpoints that are currently set in the debugger. This is both more efficient and more reliable than having scripts parse it again, and avoids hard-coding gdb commands in scripts.
GPS: new functions exported to GPS.Debugger
GPS exports more debugger functions to python, allowing scripts to be more independent of which exact debugger is actually used. These are GPS.Debugger.value_of, GPS.Debugger.set_variable, GPS.Debugger.break_at_location and GPS.Debugger.unbreak_at_location.
Jun 8th, 2016
User replacement of intConnect on VxWorks
User can now use a custom interrupt connection routine on VxWorks. Package Interfaces.VxWorks.Int_Connection has been added.
Jun 7th, 2016
Pragmas Compile_Time_Error and Compile_Time_Warning
Pragmas Compile_Time_Warning and Compile_Time_Error now support the use of attributes 'Size and 'Alignment when they are known at compile time.
Support optional refinement in private part/child
SPARK Reference Manual now allows refinement through the use 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.
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.