Development Log

  • 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 accicentally 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.

  • GNAT Pro|GNATbench | GNAT Pro|GPS
    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 signaling 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.
     

  • 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.

  • GNAT Pro|GNATbench | GNAT Pro|GPS
    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: 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.

  • GNAT Pro
    Dec 28th, 2014

    Eliminate false warnings for unused entities
    If no entities of a package are directly used, but the package is used as a generic actual parameter, the compiler could still give a warning that no entities of the package were used. These unhelpful warnings have now been eliminated.

  • GNAT Pro
    Dec 26th, 2014

    More complete warnings in validity checking mode
    In some cases, the warning about a variable not being modified (so that it could be a constant) gets lost if validity checking is turned on. This warning is now given in validity checking mode.

  • GNAT Pro
    Dec 23rd, 2014

    Warning for suspicious Subprogram’Access
    A warning is now given for P'Access, where P is a subprogram in the same package as the P'Access, and the P'Access is evaluated at elaboration time, and occurs before the body of P. For example, "X : T := P'Access;" would allow a subsequent call to X.all to be an access-before-elaboration error; hence the warning. This warning is enabled by the -gnatw.f switch.

  • SPARK Pro
    Dec 19th, 2014

    More automated proof on conversions to float
    Proof automation has been improved on code that converts between integers and floats.

  • GNAT Pro|GPRbuild
    Dec 18th, 2014

    Linking with—lto=nn when -jnn and—lto are used
    When gprbuild is invoked with -jnn (nn > 1) and with the linker switch --lto (or -flto), the linker is invoked with --lto=nn (or -flto=nn) to speed up linking.

  • SPARK Pro
    Dec 17th, 2014

    Warning on misuse of attribute Update
    A common mistake when using attribute Update in postconditions or loop invariants is to forget to use it in combination with attribute Old or Loop_Entry, which results in nonsensical expressions of the form

       X = X'Update(...)
    
    instead of the intended (in a postcondition)
       X = X'Old'Update(...)
    
    or (in a loop invariant)
       X = X'Loop_Entry'Update(...)
    
    GNAT and GNATprove now issue a warning by default on the nonsensical form, controlled with warning switches -gnatw.t/-gnatw.T

  • SPARK Pro
    Dec 17th, 2014

    Add search path for project files
    The GNATprove tool now has a commandline option "-aP" similar to the same option of gprbuild, which allows to add search paths for the location of project files.

  • SPARK Pro
    Dec 15th, 2014

    Subprograms without exports no longer ineffective
    Flow analysis used to flag calls to subprograms without exports as ineffective. This is no longer the case.

  • SPARK Pro
    Dec 12th, 2014

    Improved handling of floating point conversions
    The SPARK toolset has now improved handling of conversions between single and double precision floating point types. The result is more proved checks in the presence of such conversions.

  • SPARK Pro
    Dec 11th, 2014

    Shared manual proof files
    User's can now provide theorem libraries to GNATprove in order to access contained theorems during manual proof. To do so, the user needs to provide the sources of the library in the Proof_Dir and GNATprove will be in charge to compile it.

  • SPARK Pro
    Dec 11th, 2014

    Accept “alt-ergo” as prover name
    A common typo is to type "alt-ergo" instead of "altergo" when specifying the prover "Alt-Ergo" using the option --prover. The tool now accepts both variants.

  • GNAT Pro|GPRbuild
    Dec 10th, 2014

    GPRinstall Mode & Install_Name attributes
    It is now possible to set the Mode and Install_Name value in the package Install of a project. These attributes are equivalent to the GPSinstall command line options but allow per project fine tuning of the installation setup.

  • GNAT Pro
    Dec 9th, 2014

    Setting custom linker script for LEON run times
    User-defined linker scripts for bare board LEON targets can be set by simply defining the environment variable LDSCRIPT to point to the file to use.

  • GNAT Pro
    Dec 9th, 2014

    Implement new restriction No_Use_Of_Entity
    A new restriction No_Use_Of_Entity is implemented. The form of this is pragma Restriction[_Warning]s (No_Use_Of_Entity => NAME), where NAME is a fully qualified entity name. The effect is to forbid references to this entity in the main unit, its spec, and any subunits. For example, the use of pragma Restrictions (No_Use_Of_Entity => Ada.Text_IO.Put_Line) would forbid references to Put_Line, but references to Put would still be allowed.

  • GNAT Pro
    Dec 9th, 2014

    Trap table for LEON not modified at execution time
    The run-time libraries for bare board LEON processors install statically the minimum number of trap entries. Hence, the trap table can be easily kept in ROM.

  • GNAT Pro
    Dec 8th, 2014

    Inline_Always effective on instances without -gnatN
    On targets where inlining of calls must be done by the front end (such as JVM, .NET, AAMP), calls to subprograms marked with Inline_Always that are declared within a generic instantiation are now inlined by default (without use of -gnatN).

  • GNAT Pro
    Dec 5th, 2014

    Implement NaN semantics for floating-point ‘Min/Max
    In GNAT, Machine_Overflows is generally False for floating-point types, which means that operations such as 0.0/0.0 can generate NaN's. The Min and Max attributes have been enhanced to yield a predictable outcome in their presence: if either operand is a Nan, the other operand is returned; if both operands are NaN's, a NaN is returned.

  • SPARK Pro
    Dec 1st, 2014

    Consistent casing of flow messages
    The casing in flow messages now precisely matches the user's code.

  • GNAT Pro
    Dec 1st, 2014

    Do not warn that ineffective Inline is redundant
    Previously, if a pragma Inline was ineffective, and warn on redundant constructs was in effect (-gnatwr, included in -gnatwa), then a warning would be given that the Inline was redundant. This is not a helpful warning, and it is now suppressed.

  • GNAT Pro
    Dec 1st, 2014

    S’Img is static for a static enum type expression
    If the GNAT attribute 'Img is applied to a prefix which is of an enumeration type and is a static expression, then the result is static (and is the literal from the enumeration type). This works even if Discard_Names is in effect. This allows for example X'Img as the operand for External_Tag.

  • GNAT Pro
    Nov 27th, 2014

    Better error msg for USE of [generic] subprogram
    A USE clause is not allowed for a subprogram or generic subprogram. The compiler now gives a clearer error message for such an illegal attempt.

  • Ada Web Server
    Nov 26th, 2014

    Add support for schema root naming
    It is now possible to set the schema root name generated in the WSDL with ada2wsdl. This is needed when mixing multiple project to avoid name clashes. The same support has been added in the wsdl2aws tool to generate the sources under a specific prefix. Again this is to avoid name clashes when multiple Ada source codes are generated.

  • GNAT Pro
    Nov 24th, 2014

    Proper message on predicate with infinite recursion
    A dynamic predicate for a type that includes a call to a primitive operation of the type will lead to infinite recursion. The compiler now emits a proper error message in this case, rather than a complaint about premature use of the type in the predicate expression.

  • SPARK Pro
    Nov 24th, 2014

    Removed redundant warning of null globals assumed
    The tools used to issue a warning of "null globals assumed" both at the declaration of an imported subprogram and whenever that subprogram was called. The tools now only emit the later. These warnings can be suppressed via the use of a pragma Warnings. However, the proper solution would be to provide a global contract for the imported subprogram.

  • GNAT Pro
    Nov 23rd, 2014

    Warn when fixed-point end-points are out of range
    The compiler is allowed to adjust the declared end points of a fixed-point type by delta (RM 3.5.9(13)). This can result in a declared end-point of the range being outside the actual range of the type. GNAT takes advantage of this when it can result in the type just fitting in a convenient size (e.g. 32 bits instead of 33 bits). This situation now generates a warning.

  • GNAT Pro|GPRbuild
    Nov 21st, 2014

    GPRinstall new—no-build-var option
    A new option --no-build-var has been introduced and is meant to be use for project with a single configuration (single installation). In this case there is no build/scenario variable generated.

  • SPARK Pro
    Nov 20th, 2014

    Actual parameters with property Async_Writers
    Actual volatile parameters with enabled external property Async_Writers can now appear in procedure calls where the corresponding formal is of mode OUT.

  • GNAT Pro
    Nov 20th, 2014

    Do not trust Elaborate in SPARK
    In normal GNAT static elaboration mode, a pragma Elaborate is trusted to be sufficient, and the use of such a pragma disables the static checking. In SPARK mode, the pragma Elaborate is allowed, but it is not trusted to be sufficient, since this cannot be verified at compile time. This means that we may require Elaborate_All even if a pragma Elaborate is present.

  • GNAT Pro
    Nov 20th, 2014

    New directories in project path for gnatls—RTS=
    Two new directories are added in the project path, when gnatls is invoked with --RTS=, just before the two directories for the target. When the runtime is a single name, the directories are:

      <prefix>/<target>/<runtime>/lib/gnat
      <prefix>/<target>/<runtime>/share/gpr
    
    Otherwise, the runtime directory is either an absolute path or a path relative to the current working directory and the two added directories are:
      <runtime_directory>/lib/gnat
      <runtime_directory>/share/gpr
    

  • GNAT Pro
    Nov 19th, 2014

    Ignore Suppress (Elaboration_Check) in SPARK
    In normal GNAT mode, Suppress (Elaboration_Check) disconnects the normal static elaboration mode circuitry. We don't want that in SPARK, where the elaboration rules are important static legality rules that must not be compromised. So in SPARK mode, we ignore the attempt with a warning.

  • GNAT Pro
    Nov 18th, 2014

    Require Elaborate_All for SPARK mode variable ref
    In SPARK mode, a variable reference to a variable in another package requires an explicit Elaborate_All call, and this is now implemented. Note that the current SPARK manual specified this is only required for read/write references, so the rule implemented is more restrictive. It is not clear exactly what constitutes a read/write reference, which is why the more general, more easily stated, rule is implemented.

  • SPARK Pro
    Nov 17th, 2014

    Tune options for CVC4
    The options used for CVC4 have been tuned, so that more VCs are discharged automatically.

  • GNAT Pro
    Nov 16th, 2014

    Handle aspects before initialization expression
    Aspect specifications belong after the initialization expression in an object declaration, not before, but the compiler now accepts them before with a clear error message

  • GNAT Pro
    Nov 16th, 2014

    Require Elaborate_All for calls in SPARK mode
    In SPARK mode, we always operate in the static elaboration mode, but we do not generate implicit Elaborate_All pragmas; instead we require such pragmas to be explicitly present for calls in elaboration code. This requirement is now implemented

   1  2  3     Next »