CodePeer 2.1 – February 1, 2012
CodePeer 2.1 is a major new version and introduces many enhancements:
- - Full support for Ada 2012
- - More extensive analysis for race conditions
- - Support for elaboration code and order
- - More precise preconditions
- - Improved handling of unused assignments
A WEBINAR presenting the new features of CodePeer 2.1 tool will
take place on April 10th:
http://www.adacore.com/home/products/gnatpro/webinars/
For more information on CodePeer, please visit:
GNAT Pro 7.0.1 – February 1, 2012
GNAT Pro 7.0.1 is a major new release and includes many enhancements:
Compiler:
- - Complete Ada 2012 support
- - New controlled type implementation (better memory usage)
- - New warnings and improved error messages
- - Array processing and composite return values optimizations
Tools:
- - Many new options and pretty-printing improvements in gnatpp
- - Coupling metrics now available in gnatmetric
New Components:
-
- GNATtest (new Automatic Test Framework) to create and maintain
a complete unit testing infrastructure based on AUnit for complex
projects. It is based on a simple idea: each visible subprogram
should have (at least) one corresponding unit test.
A WEBINAR presenting the new GNATtest tool will take place on
March 20th:
http://www.adacore.com/home/products/gnatpro/webinars/
SPARK Pro 10.1 – January 3, 2012
AdaCore is pleased to announce the availability of SPARK Pro 10.1 on the following platforms:
- sparc-solaris
- x86-linux
- x86_64-darwin
- x86_64-linux
- x86-windows
This is a major release including many new features:
- Generics Phase 1 – Release 10.1 includes the first phase of the addition of support for Ada generics to the SPARK language and toolset
- Dynamic Flow Analyser and VCG Heaps
- Unicode characters now allowed in strings
- Improved use of types and subtypes in FDL
- Improvements to Simplifier tactics and performance
- Auto-generation of refinement rules
- Improvements to SPARKBridge
- New SPARKClean utility
The new features will be presented in a webinar on Tuesday February 21st, 2012.
For more information and to register, please visit:
www.adacore.com/home/products/sparkpro/language_toolsuite/webinars
Further details of the new features are as follows:
Generics Phase 1
Release 10.1 includes the first phase of the addition of support for Ada generics to the SPARK language and toolset. This first phase includes support for generic subprograms. Users can now write programs which declare a generic subprogram, then instantiate and call the instantiations. The SPARK toolset has been significantly updated to provide flow analysis and proof of VCs generated from the first phase subset of generics, although analysis of the generic subprogram body itself will be added in the next phase. Two new documents have been added to the user documentation set for
generics. “SPARK Generics – A user view” describes a subset of Ada Generics which is defined for SPARK 95 and onwards whilst maintaining the underlying design principles of SPARK. A more concise specification of SPARK generics is given in the “SPARK Generics LRM”. The motivation for incorporating generics into SPARK is – as with Ada – to provide the user with reusable components. In SPARK, these can be implemented and proven once but instantiated many times without requiring the implementation of the component to be re-analysed. The introduction of generics will provide a means, in a future release, to provide more SPARK versions of the Ada libraries, in particular the Ada Container Library.
Dynamic Flow Analyser and VCG Heaps
The main Examiner data structures used by the flow-analyser and the verification-condition generator have been re-implemented so they now extend themselves automatically rather than hitting a capacity limit. This means that the user no longer has to select between two statically-sized versions of the Examiner – spark and megaspark. A new debug option “-debug=t” has been implemented that gives more detail when “-statistics” is also selected. This option currently produces a histogram showing the peak usage of each major data structure.
As a result of the internal changes made in implementing this new feature users should also notice a reduction in the time taken to launch the Examiner.
Unicode characters now allowed in string literals
The Examiner now supports string literals containing Unicode characters. This allows, for example, strings containing umlauts, as in Sausage : constant String := “Thüringer Bratwurst”;
Improved use of types and subtypes in FDL
It is now becoming increasingly common to use other proof systems such as Alt-Ergo (via SPARKBridge), Isabelle and Riposte to discharge SPARK VCs. It can be very beneficial to these proof systems to have richer type information included in the FDL. Consequently, the Examiner has been modified to produce this information.
This change is backward compatible, so the Simplifier will still accept the generated FDL and discharge VCs as before. Other proof systems can make use of this information to significantly narrow the bounds for variables they reason about.
Improvements to Simplifier tactics and performance
The Simplifier includes new deduction rules and tactics for numeric expressions and VCs that arise from loop statements that iterate over an unconstrained array type. These new rules and tactics will give improved performance from the Simplifier when discharging certain types
of VCs.
Auto-generation of refinement rules
The Examiner will now generate refinement rules for refined own variables alleviating the need for some user rules. This will benefit users performing proofs involving abstract/refined own variables by allowing more VCs to be discharged automatically.
SPARKBridge
Whilst still an experimental feature, a number of changes have been made to SPARKBridge and support for Victor – a feature that gives access to alternate theorem provers.
- The -solver option for Victor has been extended to allow additional SMT solvers to be used: CVC3, Yices and Z3. Alt-Ergo is still supported and remains the only prover actually shipped with SPARK.
- Victor has been updated to the latest upstream version. The most important new features are support for SMTLIB2 and support for user rules.
- Victor and Alt-Ergo are now shipped and supported for OSX. This expands experimental support for Victor to the main three platforms: Windows, GNU/Linux and OSX.
SPARKClean
A new utility has been added to SPARK to clean out files generated by the SPARK tools. By default this tool simply deletes all vcg, rep, lst, siv, sum, etc. files when invoked without arguments. A user manual for SPARKClean is available with the release that provides full documentation of the options available.
GPS 5.1 – October 18, 2011
AdaCore is pleased to announce the release of GPS 5.1. This major release sees many new enhancements including:
- Improved support for C/C++:
- Initial support for smart completion
- Ada-to-C source navigation
- Improved CodePeer support
- Availability of score card
- Improved filtering
- Locations view now synced with CodePeer report
- Ability to specify alternate database/output directories
- Detailed race condition report
- New facility for handling VCS menus
- All VCS menus are now handled in a centralized place allowing customization of the layout of all VCS menus
- Availability of additional automatic code fixes
- Export browser contents to PDF
- More intuitive handling of the MDI (multiple document interface), search window and code browsers
All new features are described in the release note section on GNAT Tracker. A selection will also be demoed in the upcoming webinar featuring GPS 5.1. For more information and to enroll, please visit:
http://www.adacore.com/home/gnatpro/webinars/
GPS 5.1. is compatible with GNAT Pro versions 3.16a1 up to 6.4.
GPS 5.1 is available for the GNU/Linux, Mac OS X, Solaris, and Windows hosts.
SPARK Pro 10 – June 28, 2011
AdaCore is pleased to announce the availability of SPARK Pro 10 on the following platforms:
- sparc-solaris
- x86-linux
- x86_64-darwin
- x86_64-linux
- x86-windows
This is a major release including many new features:
Automatic selection of flow analysis mode
The Examiner now supports automatic selection of information flow
or data flow analysis on a per subprogram basis.
KCG Language Profile
As part of a collaborative development with Esterel Technologies, a
new language profile has been added to the Examiner for processing
automatically-generated SPARK code produced by Esterel’s KCG code
generator for SCADE.
Derived Numeric Types
Definition of numeric types has been made easier in Release 10.0 by the
introduction of language and tool support for explicitly derived
numeric types.
SPARKBridge preview for Windows
SPARKBridge – a bridge between the SPARK tools and Satisfiable
Modulo Theories (SMT) solvers – is now available as a preview to
Windows users, allowing them to trial alternate provers for
discharging Verification Conditions.
Library Additions
The SPARK library has been augmented with several new packages
including:
- Interfaces
- Ada.Characters.Handling
- Ada.Text_IO
Improvements to Proof Tools
The Simplifier now has enhanced reasoning capabilities for modular
types, allowing more proofs to be automatically discharged. In
addition, the proof summary output (from the POGS tool) has been
improved to make the management of the proof process easier for
large projects.
The new features will be presented in a webinar on July 5. For more
information and to register, please visit:
www.adacore.com/home/products/sparkpro/language_toolsuite/webinars
CodePeer 2.0.1 – February 21, 2011
CodePeer 2.0.1 is available for the following platforms:
- sparc-solaris
- x86_64-linux
- x86_64-windows
- x86-linux
- x86-windows
This is a major release introducing many new enhancements:
- Support for access-to-subprogram types
- More efficient SCIL generation, with faster processing and simpler (and fewer) SCIL files.
- Fewer partitions by default to perform an analysis.
- Support for parallel SCIL generation. Users can now take advantage of the gnatmake -jxx switch to generate SCIL files in parallel on multiple cpus/cores.
- New warning, “useless self assignment”, when an assignment does not modify the destination variable.
- Fewer “false positives” (false alarms)
- Improved integration with the GPS IDE.
For more information on the CodePeer tool, please visit the product page.
GNAT Pro 6.4.1 – February 16, 2011
GNAT Pro 6.4.1 is a major release, for a full list of supported platforms, please visit:
www.adacore.com/home/gnatpro/supported_platforms
New GNAT Pro 6.4 features include:
- Ada 2012 preview including most of the currently finalized Ada Issues (AIs)
- Improved code generator based on GCC 4.5
- New switch (-fdump-xref) to generate cross reference information for C and C++
- More detailed exception messages (-gnateE switch)
- New gnatcheck rules
- New warnings
- Better debugger performance
- More flexible and more efficient project manager in gnatmake/gprbuild
- Improved handling of static aggregates
For more information, please visit the GNAT Pro product page.
GNATbench 2.5 – February 8, 2011
GNATbench 2.5 introduces both new functionality as well as both enhancements and corrections to existing capabilities. New functionality includes many new source completion proposals for the Code Assist feature, new entities displayed in the Outline view, and many new source code correction proposals for the Quick Fix feature. Performance has been increased as well. These additions and enhancements make development and use even easier and more productive.
GNATbench 2.5 is supported on Eclipse 3.5, Eclipse 3.6, Workbench 3.1 and Workbench 3.2.
1. Source code completion via Code Assist includes the following new capabilities:
- Task entries and accept statements
- Qualified aggregates
- Loop parameters (i.e., loop indexes)
- Components declared in the variant parts of discriminated records
- Entities declared in Ada package Standard
- Discriminants
- Pragmas and attributes, including display of the corresponding documentation
- Instances of generic units are now included in completion proposals
- Generic formal parameters are now supported for completions within the generic unit
- Ada 2005 interface types are now supported. All primitive operations will be offered by the completion, even those coming from multiple inheritance.
In addition to the above new capabilities, existing Code Assist completions have been enhanced:
- When completing “raise” statements, only exception names and packages names (for the sake of their visible exceptions) will be proposed
- When completing variables & parameters, only package names and type names will be proposed
2. New entities are now displayed in the Outline view and the view is more robust even when the source file is changing:
- Generic formal parameters are now displayed
- Nodes for project dependencies, i.e., the “with” clauses, are now displayed
3. Many new proposals have been added to the Auto-Fix feature. (Auto Fix parses error and warning messages from the tools and proposes corresponding source code corrections.)
- New proposals for several different warnings
- New proposals for several different style checks
- Disallowed blank line(s) at end of file
- Disallowed blank space
- References to variables for which a pragma Unreferenced is applied
- Unexpected tilde or percent character in SPARK annotations
- Undefined entities, even if the compiler didn’t find any potential match
4. Miscellaneous improvements have also been incorporated, including the following:
- The editor’s syntax highlighting and formatting actions now support Ada 2012 syntax.
- GNATbench now provides a partial navigation mode available even when files are not yet compiled.
- GNATbench startup time has been significantly reduced. This improvement is especially noticeable when using sources from a remote server.
GPS 5.0 – October 29, 2010
AdaCore is pleased to announce the release of GPS 5.0. This major release sees many new enhancements including:
- Improved support for C/C++:
- More accurate and complete source navigation
- Better outline view
- Improved automatic indentation
- More powerful source editing:
- More syntax highlighting
- Annotations on the side of the editor window
- Automatic compilation
- Enhanced code completion
- Partial Ada source navigation without compilation
- Additional automatic code fixes
- Improved ease of use:
- Easy target toolchain selection
- Faster processing on large projects
- Improved handling of desktop via perspectives
- Ability to quickly create projects from existing templates
- Better tool support:
- Support for GNATstack
- Improved support for CodePeer
- Enhanced documentation generation:
- Detection of entity names in comments and production of links to their definitions
- Handling of lists and intentional line returns in structured comments
All new features are described in the release note section on GNAT Tracker. A selection will also be demoed in the upcoming webinar featuring GPS 5.0. For more information and to enroll, please visit:
http://www.adacore.com/home/gnatpro/webinars/
GPS 5.0.0 is compatible with GNAT Pro versions 3.16a1 up to 6.4.
GPS 5.0.0 is available for the GNU/Linux, Mac OS X, Solaris, and Windows hosts.
SPARK Pro 9.0 – March 22, 2010
AdaCore is pleased to announce the availability of SPARK Pro 9 available on the following platforms:
sparc-solaris
x86-linux
x86_64-darwin
x86_64-linux
x86-windows
This is a major release including many new features:
- New information-flow verification for safety and security policies, such as Bell-LaPadula, based on integrity labeling of own variables.
- New SPARK2005 language profile is now available. At present, basic Ada2005 features supported include ‘Mod, ‘Machine_Rounding, new reserved words, and the static semantics of “overriding”.
- New ZombieScope tool that detects dead statements, branches and paths in SPARK code, complementing the capabilities of the Simplifier and POGS.
- Cross Referencing annotations in GPS.
- Function return annotations are now treated more like procedure post-conditions, being substituted into the VC hypotheses of the caller thus dramatically improving the effectiveness of the theorem prover.
- A new output format for POGS designed to be both easier to read and easier to search automatically. It also reflects the results of the new ZombieScope tool.
- Case checking. New Examiner switch that insists on consistent casing within annotations.
http://www.adacore.com/home/products/gnatpro/webinars