Development Log

  • SPARK Pro
    Mar 26th, 2015

    Bodies of non-Ghost packages with Ghost constructs
    Ghost constructs that require a completion in a package body now always require the completion regardless of whether the enclosing package is a Ghost construct or not.

  • SPARK Pro
    Mar 24th, 2015

    Use of constants in contracts
    Constants with variable input can now appear in the following annotations: Global, Depends, Initializes, Part_Of, Refined_Global, Refined_Depends and Refined_State.

  • GNAT Pro|GNATbench | GNAT Pro|GPS
    Mar 24th, 2015

    GPS: makefile.py reads include statements
    Makefile targets found in included makefiles are now listed in the /Build/Makefile menu.

  • GNAT Pro
    Mar 21st, 2015

    New pragma/aspect Volatile_Full_Access
    A new pragma (and equivalent aspect) Volatile_Full_Access is implemented. This is similar to Volatile except that there is a guarantee that every read and write access to an object with this aspect will always use a single instruction which reads or writes all the bits of the object. This includes the case of referencing a component of the object. Note that this differs from Atomic in that there is no such guarantee for Atomic (the compiler can for instance read part of the object). It is not allowed to use Atomic and Volatile_Full_Access for the entity.

  • Ada Web Server
    Mar 20th, 2015

    Add support for encrypted server key file
    It is now possible to use a encrypted key file with AWS. In this case, a pass-phrase is required in order to start HTTPS sessions. This pass-phrase can be handed over to the server using Set_Password_Callback in AWS.Net.SSL.Certificate.

  • GNAT Pro|GNATbench | GNAT Pro|GPS
    Mar 17th, 2015

    GPS: new Color Theme window
    The plugin colorschemes.py has been modified: the way to switch between color themes is no longer through an entry in the Preferences dialog, but through a dedicated window, accessed using the menu Edit -> Color Themes. GPS now supports importing TextMate theme definitions, and a number of themes now ship by default with GPS.

  • GNAT Pro|GNATbench | GNAT Pro|GPS
    Mar 17th, 2015

    GPS: initial dir for the “Change Directory” dialog
    Under Linux/UNIX/Mac OS, the "Change directory" dialog now opens on the current directory, matching the behavior already present on Windows.

  • SPARK Pro
    Mar 17th, 2015

    Contracts on generic subprograms and packages
    The SPARK toolset now supports contracts on generic subprograms, packages and their respective bodies.

  • GNAT Pro
    Mar 17th, 2015

    Alignment_Check suppressed for non-strict alignment
    Alignment_Check is now suppressed by default for machines with non-strict alignment (such as the x86) since these machines handle unaligned references without any problem. Associated compile-time warnings are also suppressed if the run-time check is suppressed. The previous mode of operation (with this check enabled by default) can be obtained by placing in a configuration pragma file "pragma Unsuppress (Alignment_Check)".

  • GNAT Pro
    Mar 16th, 2015

    Add low bit rates to GNAT.Serial_Communications
    New literals B75, B110, B150, B300, and B600 have been added to type GNAT.Serial_Communications.Data_Rate to denote these low bit rates, in order to allow communication with legacy devices that require them.

  • GNAT Pro
    Mar 15th, 2015

    Exclude extended precision for ignored assertion
    If an assertion is compiled using the Ignore policy, and the overflow mode is Eliminate, then the extended precision arithmetic run-time unit (s-bignum) was being included in the build even though no code was being generated. This is now avoided, which is particularly important when using a configurable run-time that does not include this unit.

  • Ada Web Server
    Mar 14th, 2015

    Add support for document style SOAP/WSDL
    AWS now supports document style SOAP messages and WSDL documents.

  • PolyORB
    Mar 13th, 2015

    gnatdist now uses gprbuild by default
    The gnatdist partitioning tool will now use gprbuild by default to build partitions, if that tool is available. You can force the use of gnatmake using debugging switch -dM.

  • SPARK Pro
    Mar 13th, 2015

    Improve handling of dynamic types with dispatch
    The SPARK toolset now tracks bounds of dynamic scalar and array types better in particular in presence of dispatching calls and for verification of LSP conformance.

  • GNAT Pro|GPRbuild
    Mar 13th, 2015

    Dependency with different timestamp
    gprbuild now recompiles a file based source if one of its dependency source has a different time stamp, even when the time stamp is before the one of the object file.

  • Ada Web Server
    Mar 8th, 2015

    Add support for minOccurs/maxOccurs
    Add support for multi-occurrence SOAP elements. SOAP element declared with a minOccurs or maxOccurs different than 1 are now properly handled as multi-occurrence elements. If minOccurs is set to 0 the element can be omitted.

  • GNAT Pro
    Mar 5th, 2015

    Null procedures allowed in protected bodies
    AI12-0147 specifies that null procedures and expression functions are now allowed in protected bodies.

  • SPARK Pro
    Mar 5th, 2015

    Improve support of rotation of modular types
    The SPARK toolset now deals better with rotation of modular types of non constant amount.

  • GNAT Pro
    Mar 2nd, 2015

    Multiset libraries are indexing aspects
    The GNAT-specific ordered and indefinite multiset libraries have indexing aspects, and thus can be used in element iterators.

  • GPS: source navigation in CodePeer-only mode
    When GPS is used with CodePeer only (no GNAT installed), the build mode is automatically changed to properly load the cross-references information.

  • GPS: control jump to first message in plugins
    Python plugins can use new parameter of GPS.Message's class constructor to control automatic jump to first message in category.

  • Ada Web Server
    Feb 28th, 2015

    Add support for WSDL/SOAP type’s constraints
    The tools ada2wsdl and wsdl2aws handle now the type constraints. That is, ada2wsdl will check for range attribute, mod for modular types and array index to generate the corresponding constraints in the WSDL using the simpleType Length, minInclusive and maxInclusive attributes. Those attributes (plus the minExclusive and maxExclusive ones) are now used by wsdl2aws to generate Ada type constraints. Now a constrained string is generated instead of an Unbounded_String for a simpleType with a Length attribute whose base type is xsd:string. The simpleType Pattern attribute is now taken into account and a Dynamic_Predicate aspect is generated. For varying length string with attribute minLength and/or maxLength a Dynamic_Predicate aspect is also generated. Those now constraints will ensure that SOAP objects sent/received are not violating the constraints expressed into the WSDL making the new implementation safer.

  • GNAT Pro
    Feb 28th, 2015

    New pragma Ignore_Pragma
    A new pragma Ignore_Pragma is implemented. This is a configuration pragma that takes a single argument that is a simple identifier. Any subsequent use of a pragma whose pragma identifier matches this argument will be silently ignored. This may be useful when legacy code or code intended for compilation with some other compiler contains pragmas that match the name, but not the exact implementation, of a GNAT pragma. The use of this pragma allows such pragmas to be ignored, which may be useful in CodePeer mode, or during porting of legacy code.

  • SPARK Pro
    Feb 27th, 2015

    Optional Refined_Global/Depends aspects
    Users no longer have to provide a Refined_Global/Depends aspect when their Global/Depends mentions a state with visible refinement. Flow analysis now synthesizes and uses these aspects internally.

  • GNAT Pro
    Feb 27th, 2015

    Attribute Deref dereferences address expression
    A new attribute typ'Deref(expr) where expr is of type System.Address yields the variable of type typ that is located at the given address. It is similar to (totyp (expr).all), where totyp is an unchecked conversion from address to a named access-to-typ type, except that it yields a variable, so it can be used on the left side of an assignment. Note that this new attribute is not available for the .NET port).

  • GNAT Pro
    Feb 26th, 2015

    Convention pragma on generic formal access types
    The compiler now accepts a pragma Convention on a generic formal access to subprogram type, and verifies that an actual for such a formal obeys the same convention.

  • GNAT Pro|GNATbench | GNAT Pro|GPS
    Feb 24th, 2015

    GPS: use of perspective for CodePeer report
    GPS now has a perspective dedicated to viewing CodePeer results.

  • SPARK Pro
    Feb 23rd, 2015

    More precise analysis of bitwise operations
    GNATprove now handles more precisely bitwise operations on modular types by translating modular types to bitvectors for the underlying automatic provers. Currently, CVC4 is performing best on this kind of VCs. Some operations are still known to generate hard to prove VCs: conversions between modular and signed, modular used as array index, shift and rotate by a non constant amount.

  • SPARK Pro
    Feb 23rd, 2015

    Improve support for anonymous subtypes
    The SPARK toolset now deals better with checks associated with anonymous subtypes declared at the beginning of a subprogram.

  • CodePeer
    Feb 23rd, 2015

    Use Red/Orange/Yellow in CodePeer HTML report
    The HTML report was using Red/Yellow/Green for High/Medium/Low ranking messages. This was inconsistent with the Red/Orange/Yellow color coding used in GPS. The HTML report now uses Red/Orange/Yellow consistently for High/Medium/Low. There was no other change to the HTML output.

  • SPARK Pro
    Feb 20th, 2015

    Default initialized formal containers are empty
    When a formal container is default initialized, the SPARK toolset now knows it is empty.

  • SPARK Pro
    Feb 20th, 2015

    Accept “Runtime” and “Target” attributes
    The SPARK toolset now accepts the "Runtime" attribute of project files, which has the same effect as the --RTS commandline switch. The SPARK toolset now also accepts the "Target" attribute, although this attribute is currently ignored.

  • Ada Web Server
    Feb 18th, 2015

    Add support for documentation in WSDL
    AWS's wsdl2aws tool will now record the annotation/documentation nodes in the WSDL and generate comments out of them in the Ada generated code. These comments are handled for the WSDL operations and schema's types.

  • CodePeer
    Feb 18th, 2015

    Distinguish imported values of a global variable
    When the value of a global variable is used to initialize a global constant, it is possible that the value might change between when the global constant "captures" the variable's value, and when the value is subsequently fetched elsewhere in the program. CodePeer will now indicate in preconditions, postconditions, and other messages that a value of a variable was captured as part of initializing a global constant by adding a suffix on the global variable's name indicating the elaboration procedure initializing the constant. For example, "Global_Var@my_package'Elab_Spec" represents the value of Global_Var that was read by the My_Package spec elaboration procedure as part of initializing some constant declared in My_Package.

  • GNAT Pro
    Feb 18th, 2015

    Pre/Postconditions now count as WITH references
    If a package is with'ed and used only in pre and postconditions, then the package is still considered as referenced even if contracts are not enabled. This avoids a false positive warning "unit xxx is not referenced".

  • CodePeer
    Feb 17th, 2015

    Allow illegal comment characters
    Ada does not allow nongraphic characters (such as 16#7F#, DEL) in comments, but now CodePeer ignores this error, since some compilers do not flag this error, and it does not affect the CodePeer analysis of the code itself.

  • GNAT Pro
    Feb 17th, 2015

    Allow illegal comment characters in CodePeer mode
    Ada does not allow nongraphic characters (such as 16#7F#, DEL) in comments, but now CodePeer ignores this error, since some compilers do not flag this error, and it does not affect the CodePeer analysis of the code itself.

  • GNAT Pro
    Feb 14th, 2015

    Type_Invariant’Class on interface types implemented
    The Type_Invariant'Class aspect is now supported for interface types (as described in AI12-0041-1/03). When a type implements one or several interfaces, its inherited type invariant is the conjunction of all ancestor Type_Invariant'Class aspects.

  • GNAT Pro|GNATbench | GNAT Pro|GPS
    Feb 13th, 2015

    GPS: align.py enabled on gpr files
    When editing a .gpr project file, the Align contextual menu is now available, as it is in Ada files

  • GNAT Pro
    Feb 8th, 2015

    Better error message for Type_Invariant’Class
    In some error messages, the aspect name Type_Invariant'Class appeared as Type_Invariant_Class, and now the more accurate name with the quote is used.

  • GNAT Pro
    Feb 7th, 2015

    Better error message for bad use of prefix notation
    An attempt to use an untagged type with prefix notation now generates a more helpful message pointing out that this is specifically not allowed.

  • GNAT Pro
    Feb 7th, 2015

    Avoid internal names in error messages
    In some cases error messages would display internal compiler names that were not very helpful. Such messages are now fixed to display a more useful meaningful name, or eliminated.

  • GPS: display of CWEs from CodePeer
    GPS displays CWEs (Common Weakness Enumeration) for CodePeer's messages in Locations view and provides corresponding filter in CodePeer Report view.

  • GPS: project properties for uneditable projects
    The Project Properties dialog can now be displayed even in cases where the project cannot actually be edited graphically (aggregate project, project using variables,...).

  • GNAT Pro
    Feb 4th, 2015

    Better error recovery for statement in decls
    If a statement (e.g. an assignment statement) is used within a declaration sequence, then it is properly recognized now, so that if the -gnatQ option is used, the program compiles and executes successfully (after giving an appropriate error message).

  • Ada Web Server
    Feb 2nd, 2015

    Add explicit support for TLS 1.1 and 1.2
    Allow explicit support for TLS 1.1 and 1.2 on OpenSSL. This also enable to restrict use of these specific protocols.

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

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

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

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

  • GNAT Pro|GNATbench | GNAT Pro|GPS
    Jan 26th, 2015

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

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

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

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

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

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

  • GNAT Pro
    Dec 16th, 2014

    Simplified code in Delay_Until in Ravenscar Cert
    The implementation of delay until operations in the Ravenscar Cert runtime library for Vxworks Cert has been greatly simplified since many conditions cannot occur under the Ravenscar restrictions.

  • 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 2nd, 2014

    New formal vectors both definite and indefinite
    The API of formal vectors has been simplified for efficiency, and a new standard unit Ada.Containers.Formal_Indefinite_Vectors is defined to hold elements of an indefinite type, for example a classwide type. Both units can be used in SPARK code, and GNATprove then generates checks that the API is used correctly.

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

   1  2  3     Next »