Development Log in January 2015.

  • Ada Web Server
    Jan 31st, 2015

    Add support for xs:choice in WSDL complexType
    AWS's wsdl2aws tool has now partial support for complexType with xs:choice items. This is mapped in Ada with a record with discriminant. Only a single occcurence of each item is supported by this implementation.

  • SPARK Pro
    Jan 30th, 2015

    Improved placement of quotes in flow messages
    The placement of double quotes in flow messages has been improved. For example, instead of:

      medium: "private part of S" might not be initialized
      high: "extension of Log" is not initialized
    
    we now get:
      medium: private part of "S" might not be initialized
      high: extension of "Log" is not initialized
    

  • GNAT Pro
    Jan 30th, 2015

    No stand-alone code for Inline_Always intrinsics
    GCC-based compilers no longer produce stand-alone code for Inline_Always subprograms with convention Intrinsic. This allows the definition of Ada subprograms similar to "extern inline" functions in C.

  • SPARK Pro
    Jan 29th, 2015

    Useless pragma Annotate are flagged
    The SPARK toolset now flags uses of pragma Annotate which do not suppress any check message. This helps in maintaining projects where pragma Annotate is used.

  • GPS | GNATbench
    Jan 29th, 2015

    GPS: omni-search now searches in gpr files
    The 'Sources' context in the omni-search now also searches the gpr files themselves, in addition to the source files.

  • GNAT Pro
    Jan 29th, 2015

    Improve handling of pragma Independent[_Components]
    The implementation of aspects/pragmas Independent[_Components] has been overhauled so as to reject them in fewer cases, in particular with packing for record types, and make them consistent with similar aspects/pragmas.

  • GPS | GNATbench
    Jan 28th, 2015

    GPS: Revamp the project properties dialog
    We have redesigned the dialog to edit the project properties, to avoid the use of notebooks, since there was potentially a large number of pages in the notebook and it became difficult to select them.

  • SPARK Pro
    Jan 27th, 2015

    Improved error message about hidden state
    When a variable that is part of the hidden state of another package is used by a subprogram without having been mentioned in the subprogram's Global aspect the tools issue an error saying that a Global aspect is required to make the variable visible. The relevant message now also mentions the other package's variable that triggered the error.

  • GPRbuild
    Jan 27th, 2015

    Warnings when interface of a SAL is incomplete
    When gprbuild is invoked without -q, it checks if the interface of a SAL is complete, and warn if units of the project that are imported by the interface units are not themselves in the interface.

  • GPS | GNATbench
    Jan 26th, 2015

    GPS: Better fortran syntax highlighting
    A new syntax highlighter has been added for fortran, using the new python highlighters engine.

  • GPRbuild
    Jan 26th, 2015

    New gprbuild switch -z
    gprbuild now accepts the switch -z to build executable with no main subprogram, as gnatmake already does.

  • GNAT Pro
    Jan 26th, 2015

    Inline_Always overrides gcc -fno-inline
    For GCC-based compilers, pragma Inline_Always now enforces inlining even with -fno-inline passed on the command line, which makes the pragma behavior consistent with the use of an "always_inline" machine attribute.

  • GPS | GNATbench
    Jan 23rd, 2015

    GPS: \i for sequence number in regexp replacements
    When the regular expression replacement string contains "\i" or "\i(start, delta)" then this pattern will be replaced with sequence numbers in replacement text.

  • SPARK Pro
    Jan 21st, 2015

    Check that ‘Old prefix is an in[put]
    The GNATprove tool now issues a high check whenever a prefix of an attribute "Old" is not either a formal "in" parameter or a global "input".

  • SPARK Pro
    Jan 20th, 2015

    Use version 0.99.1 of Alt-Ergo
    The Alt-Ergo theorem prover shipped with GNATprove is now the 0.99.1 version instead of the 0.95.2 version, which allows slightly more proofs to be automated on average.

  • SPARK Pro
    Jan 20th, 2015

    Improve handling of dynamic private types
    The SPARK toolset now tracks bounds of dynamically constrained arrays and discriminants of dynamically constrained records better, especially when their type is private. This results in better automatic proof of run-time checks.

  • SPARK Pro
    Jan 19th, 2015

    New form of pragma Warnings for specific tool
    Users of GNATprove can now specify pragma Warnings for GNAT and GNATprove separately, to selectively disable warnings from the compiler or the formal verification tool, using the syntax

      pragma Warnings (GNATprove, ...);
    
    for GNATprove-specific warnings, and
      pragma Warnings (GNAT, ...);
    
    for GNAT-specific warnings. This also allows detecting useless pragma Warnings with switch -gnatw.w, which was not possible previously as using this switch caused the tools to issue spurious warnings on the those pragma Warnings meant for the other tool.

  • Ada Web Server
    Jan 18th, 2015

    Add support for external schema
    It is now possible to use WSDL with references to external schema. In this case, wsdl2aws tool, will check the schema locally and load it if found.

  • Ada Web Server
    Jan 18th, 2015

    Add support for derived types
    AWS's wsdl2aws tool has now full support for derived types. The namespace for the parent type is properly used when generating the corresponding Ada code. This has make it possible to clean-up some old code to handle Ada Character mapping for example. Any type derivation level is properly handled.

  • GNAT Pro
    Jan 18th, 2015

    Better error recovery for WHEN in place of WITH
    The compiler now handles the case of WHEN used accidentally instead of WITH to introduce aspect specifications, and gives a clear error message.

  • GNAT Pro
    Jan 17th, 2015

    New documentation on floating-point
    A new section on "Floating-Point Operations" is added to the users guide. This section documents the infinity/NaN behavior of most GNAT ports, and also describes the -msse2 and -mfpmath=sse2 switches to force use of SSE2 arithmetic operations when the target is an x86.

  • GPS | GNATbench
    Jan 14th, 2015

    GB: Debugger field added to toolchain editor
    Debugger command can be displayed and changed in the toolchain editor.

  • SPARK Pro
    Jan 13th, 2015

    Issue proof checks on calls to Assertions.Assert
    GNATprove now generates a check that Assertions.Assert procedures are always called with a Check argument of "True". This check shows as a precondition check when calling Assertions.Assert (a precondition added in the declarations of Assertions.Assert in a-assert.ads). The dynamic semantics of Assertions.Assert have not been modified, by setting the Assertion_Policy to Ignore for Pre in this unit (also in the same file).

  • SPARK Pro
    Jan 13th, 2015

    No implicit False pre on main loop subprogram
    During proof, GNATprove was treating all subprograms with No_Return aspect or pragma specified as error signalling subprograms, with an implicit precondition of "False". Now, subprograms with an output (parameter or global) are treated as main loop subprograms, hence without an implicit precondition of "False". This is similar to the distinction made in flow analysis.

  • Ada | Ada 2012
    Jan 12th, 2015

    Public Ada Training 2015

    This course, combining live lectures with hands-on lab sessions using the latest AdaCore tools and the STM32F4 Discovery Board, introduces software developers to the principal features of the Ada language with a special focus on embedded systems. Attendees will learn how to take advantage of Ada's software engineering support, including the contract-based programming features in Ada 2012, to produce reliable and readable code. No previous Ada experience is required.
     

  • GNAT Pro
    Jan 12th, 2015

    Optimized code with/without debug info on xcoff
    As was already done on other targets, GNAT now generates optimized code with debugging information that is identical to the optimized code generated without debugging information on LynxOS-178 and AIX targets.

  • SPARK Pro
    Jan 12th, 2015

    Support pragmas Precondition/Postcondition in body
    Pragmas Precondition and Postcondition (both GNAT-specific pragmas) inside subprogram bodies where currently ignored by GNATprove. They are now treated like assertions, occurring respectively on entry and on exit to the subprogram, so GNATprove generates checks to prove that they hold.

  • GPS | GNATbench
    Jan 12th, 2015

    GPS: organize /Build menu by project
    When your project (or the imported projects) has a large number of mains, the /Build/Project and /Build/Run menu could become very large and require scrolling. Instead, an extra level of menu has been added, for each project that has a main.

  • GNAT Pro
    Jan 12th, 2015

    New tag missing-check in known problems file
    A new tag "missing-check" is added to the known-problems-73 file. This is similar to "wrong-code", but is used specifically for the case where the compiler is omitting a required run-time check.

  • GNAT Pro
    Jan 10th, 2015

    Warn on use of pragma Import in Pure unit
    The use of pragma Import in a Pure unit is worrisome since it can be used to "smuggle" non-pure behavior into a pure unit. This usage now generates a warning that calls to a subprogram imported in this manner may in some cases be omitted by the compiler, as allowed for Pure units. This warning is suppressed if an explicit Pure_Function aspect is given.

  • GNAT Pro
    Jan 8th, 2015

    Improve always True/False warning
    The warning that a condition is always False is improved to give a special clearer message when the subexpression is a simple object.

  • GPS | GNATbench
    Jan 6th, 2015

    GPS: use unix-style paths when editing project
    When project properties are edited, all possible occurrences of backslashes are replaced with slashes. This makes it possible to use such project both under Windows and Linux.

  • SPARK Pro
    Jan 6th, 2015

    Support for multi-unit source files
    The SPARK toolset now supports the analysis of multi-unit source files, that is, files which define several library-level packages.