- Ada 2012
- Ada 2005 / 95 / 83
- Embedded Development
- Formal Methods
- Open Source
- Safety-Critical Development
- Static Analysis
GPS: search icons in GPS_CUSTOM_PATH
Icons used in plug-ins are now also searched in any of the directories specified in the environment variable GPS_CUSTOM_PATH.
Aug 31st, 2016
Include package Ada.Numerics.Real_Arrays
The Ravenscar "full" runtime libraries now include the language- defined package Ada.Numerics.Real_Arrays.
Assume Initial_Condition of withed units
When checking compilation units, we now assume that the Initial_Condition aspect of each withed unit holds. It results in more discharged verification conditions in particular on main units.
Counterexamples involving quantified expressions
Some counterexamples are now printed for universally quantified variables (in loop invariants for example).
Aug 28th, 2016
gnatbind: New elaboration order algorithm
A new elaboration order algorithm is implemented, which is likely to be friendlier in most cases, especially with existing code that works with other compilers. It has the following useful properties: - Considering the graph of library units, each strongly connected component (SCC) is elaborated together, with no intervening units from other SCCs. In the absence of cycles in this graph, an SCC is a single library unit. If there are cycles, an SCC is a maximal group of units with cyclic dependences. Note that the nodes of this graph are library units, not library items. Cycles among library items are illegal (e.g. two specs cannot mention each other in nonlimited with clauses). Cycles among library units are legal (two packages may be mutually recursive, so long as at least one dependence is via a body. - In particular, this implies that if an SCC contains just a spec and the corresponding body, and nothing else, the body will be elaborated immediately after the spec. This is expected to result in a better elaboration order for most programs, because in this case, a call from outside the library unit cannot get ABE. - The elaboration order chosen is the same in static and dynamic mode. - Pragmas Elaborate_All (explicit and implicit) are ignored. Instead, we behave as if every legal pragma Elaborate_All were present. That is, if it would be legal to have "pragma Elaborate_All(Y);" on X, then we behave as if such a pragma exists, even if it does not.
Aug 26th, 2016
Support of Cortex-M0/M0+/M1 on arm-elf platform
The arm-elf bareboard compiler now supports Cortex-M0, Cortex-M0+ and Cortex-M1 cores. At this time there is no provided runtimes, but users can write their own ones.
Aug 19th, 2016
More info when reviewing a message in GPS
The GPS dialog for reviewing a single message now contains information about the message, similarly to the dialog for reviewing multiple messages.
GPS: more info when reviewing a codepeer message
The CodePeer dialog for reviewing a single message now contains information about a message, similariliy to the dialog for reviewing multiple messages.
Aug 19th, 2016
gnatcheck: In incremental mode, reflag errors
In --incremental mode, if gnatcheck gives an error message on a certain file, and you run it again, it will now give the error message on that file again.
GPS: preserve more build errors after recompiling
When the Locations view contains build errors, and one of the files is being recompiled, the Locations view will now only update the entries for that file, rather than removing all build errors.
Aug 16th, 2016
The UG section 8.6.4. Proof Limitations does now better document the support for storage place attributes. In particular, it states that First_Bit, Last_Bit and Position attributes are supported but in case there is no record representation clause then their value is assumed to be nonnegative.
schema: large values of maxOccurs
Values of maxOccurs larger than 300 previously resulted in an XML validation error. This is instead a limitation of XML/Ada, so this has now been changed to a warning (we still recommend using "unbounded" to limit the size of the state machine, but XML/Ada will now try to build that machine and use the XSD nonetheless).
Aug 16th, 2016
Speedup CodePeer WebServer startup
Startup time of CodePeer web server with large dababase was significantly reduced.
Aug 16th, 2016
Better error message on selected component
Compiler provides a better error report on a selected component Nam.Comp which appears in an object declaration, when Nam has several visible interpretations as a function, and there is a non- visible package in the context with the same name.
Aug 10th, 2016
Removing redundant checks on type conversions
Conversions to Standard_Integer of an attribute reference 'Pos applied to a nonstatic expression of an enumeration type do not generate a constraint check, given that the number of literals of any such type will not exceed Integer'Last.
GPS: wrong file view for multi-drive projects
When the 'Show files from project only' option is enabled, the Files view now correctly displays the project files that reside on multiple logical drives.
Aug 5th, 2016
More fine-grain placement rules for pragma Annotate
Previously, if pragma Annotate was placed e.g. at the start of a statement list, it would apply to the whole enclosing construct (e.g. an if statement including all branches and statements). Now it only applies to the range between the beginning of the enclosing statement and the pragma itself. This allows to e.g. apply a pragma Annotate to the condition of an if-statement, but not the other parts of the if-statement. Note that this may require changes to the placement of pragma Annotate in existing code, or more pragma Annotate than before.
GPS: new trace for old Xming compatibility
A new trace "Views.No_Transient_Views" has been added. When activated (in .gps/traces.cfg or via the --traceon switch), this prevents the use of "transient" windows for floating views. This is needed mostly for compatibility with the Xming X11 server which does not allow resizing transient windows, and calculates their size wrongly. Another trace "Store_Window_Positions" has been added: this is on by default, and, when switched off, will prevent GPS from saving the size and positions of floating windows.
Aug 3rd, 2016
C binding for preprocessor constant with 0. prefix
The C and C++ bindings generated by means of the -fdump-ada-spec option now correctly handle preprocessor floating constants with 0. prefix.
Aug 1st, 2016
Support for GNAT attribute System’To_Address
GNAT attribute System'To_Address, which is a static attribute equivalent to a call to System.Storage_Elements.To_Adress, is now supported.