Tool Development and Support

 

SPARK Toolset Release Note 8.1.1

 

 

 

 

 

 

 

 

 

 

 

RN

Issue: 3.0

Status: Definitive

27th April 2009

 

DOCTYPE:Praxis title:varchar=title reference:varchar=reference status:varchar=status issue:varchar=issue date:varchar=date projectname:varchar=DocumentSet

Issue 3.0, Definitive, 27th April 2009

000_000 SPARK Toolset Release Note 8.1.1

 

 

 

Originator

 

 

SPARK Team

 

 

 

Approver

 

 

SPARK Team Line Manager

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 



Copyright

The contents of this manual are the subject of copyright and all rights in it are reserved. The manual may not be copied, in whole or in part, without the written consent of Praxis High Integrity Systems Limited.

 

Limited Warranty

Praxis High Integrity Systems Limited save as required by law makes no warranty or representation, either express or implied, with respect to this software, its quality, performance, merchantability or fitness for a purpose. As a result, the licence to use this software is sold ‘as is’ and you, the purchaser, are assuming the entire risk as to its quality and performance.

Praxis High Integrity Systems Limited accepts no liability for direct, indirect, special or consequential damages nor any other legal liability whatsoever and howsoever arising resulting from any defect in the software or its documentation, even if advised of the possibility of such damages. In particular Praxis High Integrity Systems Limited accepts no liability for any programs or data stored or processed using Praxis High Integrity Systems Limited products, including the costs of recovering such programs or data.

SPADE is a trademark of Praxis High Integrity Systems Limited

Note:  The SPARK programming language is not sponsored by or affiliated with SPARC International Inc. and is not based on SPARC™ architecture.


Contents

1       Introduction

2       SPARK language changes

3       Examiner changes

3.1     Warn if -vcg specified but no VCs generated (SEPR 2651)

3.2     Additional proof rules for task discriminants (SEPR 2088)

3.3     Removal of Examiner –concatenate and –tree switches (SEPR 2665)

3.4     Correct modelling of dynamic “for” loop nested inside a case statement (SEPR 608)

3.5     FDL declarations and rules for numeric constants used in proof rules (SEPR 2684)

3.6     New –debug=V switch for visualization of VCG graphs (SEPR 2657)

4       Simplifier changes

4.1     Improved equality substitution (SEPR 2362 and SEPR 2047)

5       Proof Checker changes

6       POGS changes

7       SPARKFormat changes

7.1     Prevent removal of annotations that immediately follow global annotations (SEPR 2674)

8       SPARKMake changes

8.1     Normalized order of file and directory scanning

9       Backward incompatibilities

10     User manual change summary

11     Limitations and known errors

11.1   Tool limitations

11.2   Known error summary

12     Change Summary from Release 2.0

12.1   Release 2.0 - November 1995

12.2   Release 2.1 - July 1996

12.3   Release 2.5 - March 1997

12.4   Release 3.0 - September 1997

12.5   Release 4.0 - December 1998

12.6   Release 5.0 - June 2000

12.7   Release 6.0 - November 2001

12.8   Release 6.1 - June 2002

12.9   Release 6.3 – December 2002

12.10Release 7.0 – July 2003

12.11Release 7.2 – December 2004

12.12Release 7.3 – February 2006

12.13Release 7.31 – April 2006

12.14Release 7.4 – January 2007

12.15Release 7.5 – May 2007

12.16Release 7.6 – June 2008

12.17Release 7.6.2 – February 2009

12.18Release 8.1.0 – March 2009

13     Operating system compatibility

13.1   VAX/VMS

13.2   SPARC/Solaris

13.3   Windows

13.4   Intel/Linux

13.5   Apple OS X

Document Control and References

Changes history

Changes forecast

Document references

File under

 

 


1                       Introduction

Continued development of the SPARK Toolset has resulted in the development of a number of useful features that have been incorporated into Toolset Release 8.1.1.

This document describes changes in the behaviour of all variants of the SPARK Toolset Release 8.1.1 compared to Release 8.1.0.

2                       SPARK language changes

This section describes SPARK language changes supported by Toolset Release 8.1.1 since release 8.1.0.

None.

3                       Examiner changes

This section documents other significant changes to the SPARK Examiner made for release 8.1.1. Where appropriate, SPARK Examiner Performance Report (SEPR) numbers are given.

3.1               Warn if -vcg specified but no VCs generated (SEPR 2651)

The Examiner now issues the following warning:

                Warning - VC Generation requested but no bodies presented. No VCs generated.

This warning is issued when the VC generator is active (i.e. any of the –rtc, -exp, or –vcg switches have been given), but no bodies that actually generate any VCs have been presented to the Examiner. This prevents the common error of presenting only package specifications to the Examiner, resulting in no VCs, or (perhaps worse) leaving previously generated VCs in place.

3.2               Additional proof rules for task discriminants (SEPR 2088)

The Examiner now generates a proof rule in the RLS file indicating that a task discriminant is always within its indicated scalar subtype. This improves completeness of proof for task types where the value of the task discriminant is used within the task body.

3.3               Removal of Examiner –concatenate and –tree switches (SEPR 2665)

The –concatenate switch caused the Examiner to generate VCs in files with long concatenated filenames, instead of in a tree of subdirectories.  This switch was only ever intended for use on VAX/VMS, so is now removed.

The default and only behaviour is now that of the existing –tree switch. The –tree switch can still be given to the Examiner, but is ignored. These options no longer appear in the Examiner’s report file.

3.4               Correct modelling of dynamic “for” loop nested inside a case statement (SEPR 608)

In all Examiner versions prior to 8.1.1, the VCG model for a dynamic-range “for” loop nested inside a case statement was incorrect.  This led the VC Generator to report that the enclosing subprogram had a cyclic path with no assertion, and no VCs were generated.

This problem is now fixed in Release 8.1.1 of the Examiner.  For example, VCs for the following code are now correct:

   type T is (Red, Green);

 

   procedure Op1 (X : in T; Y : in out Integer)

   --# derives Y from Y, X;

   is

   begin

      case X is

         when Red =>

            for I in S range 1 .. 5 loop

               Y := Y + 1;

            end loop;

         when others =>

            null;

      end case;

   end Op1;

3.5               FDL declarations and rules for numeric constants used in proof rules (SEPR 2684)

The Examiner now generates FDL declarations and rules for numeric types that appear as fields of records or elements of arrays, even if those types do not appear explicitly in the VC itself. This ensures that, when the Simplifier creates additional hypotheses from those rules, the resulting VC is acceptable to the Proof Checker.

In some cases, the automatic proof of a VC may also be improved by this change. For example, given the following declarations:

type RawType is range 0 .. 70;

 

type MyEnumT is (None, FarLeft, Left, Middle, Right);

 

subtype IndexT is MyEnumT range FarLeft .. Right;

 

type MyArrayT is array (IndexT) of RawType;

 

C: constant MyArrayT := MyArrayT'(5, 10, 15, 20);

A type conversion expression such as:

Natural32 (C (Left))

Gives rise to a verification condition

C1:    element(c, [left]) >= 0 .

C2:    element(c, [left]) <= 2147483647 .

which cannot be proven by the Simplifier in Toolset Release 8.1.0, even though there is a rule in the RLS file such as:

rawtype__first <= element(c, [I]) may_be_deduced_from [farleft <= I, I <= right].

element(c, [I]) <= rawtype__last may_be_deduced_from [farleft <= I, I <= right].

Unfortunately, Simplifier 8.1.0 is unable to use this rule, owing to the lack of rules or declarations for rawtype__first and rawtype__last.

Examiner 8.1.1 generates additional FDL declarations:

type rawtype = integer;

const rawtype__last  : integer = pending;

const rawtype__first : integer = pending;

and rules:

rawtype__first may_be_replaced_by 0.

rawtype__last  may_be_replaced_by 70.

which enable the Simplifier to discharge this VC.

3.6               New –debug=V switch for visualization of VCG graphs (SEPR 2657)

A new “debug” switch has been added in release 8.1.1.

The switch –debug=v was added in release 8.1.0 – this produces the VC-Generator’s Basic Path Graph (BPG) in “DOT” format following the “BuildGraph” phase of its processing.

The new switch –debug=V goes further, and produces the BPG at each iteration of the VCG process, up to and including the final BPG with VCs labelling each arc. The resulting files have a numeric suffix to indicate the iteration of the VCG process.

For information about the “DOT” format for describing graphs, and tools with which to view them, see www.graphviz.org

 

 

4                       Simplifier changes

Simplifier 8.1.1 includes the following improvements, and includes the following changes.

4.1               Improved equality substitution (SEPR 2362 and SEPR 2047)

Extended the Simplifier’s search strategy to utilise hypotheses that specify equivalence relationships between the same fields of two variables of the same record type in discharging VCs – e.g.

    fld_x(blah_one) = fld_x(blah_two)

 

5                       Proof Checker changes

Proof Checker 8.1.1 includes the following improvements and changes over release 8.1.0:

None.

 

6                       POGS changes

POGS 8.1.1 includes the improvements and changes over release 8.1.0:

None.

 

7                       SPARKFormat changes

SPARKFormat version 8.1.1 includes the following changes and improvements:

7.1               Prevent removal of annotations that immediately follow global annotations (SEPR 2674)

Previously, in legal SPARK code, where accept, end, for, function or type annotations immediately follow global annotations, these annotations were incorrectly removed. SPARKFormat now correctly preserves these annotations.

8                       SPARKMake changes

SPARKMake 8.1.1 includes the following changes and improvements:

8.1               Normalized order of file and directory scanning

SPARKMake has been modified so that the order of entries in generated index and meta-files is the same on all platforms.

Previously, the order produced could depend on the order in which the underlying operating system generated the list of files in a directory. SPARKMake now sorts these filenames into lexicographic order before further processing, thus ensuring consistent behaviour on all platforms.

 

9                       Backward incompatibilities

The following backward incompatibilities were introduced between Examiner Releases 8.1.0 and 8.1.1.

None.

10                 User manual change summary

The following user manuals have been changed between Examiner Releases 8.1.0 and 8.1.1.

·          Examiner User Manual

·           Documents new warning when VCs requested but not generated (see section 3.1 of this document).

·           Removal –tree and –concatenate switches.

·           Documentation of new debug=V switch. (section 3.1.4 of the Examiner User Manual)

·          SPARK Quick Reference Guides 1, 3 and 4

·           Updated to reflect preferred use of “-“ for command-line switches on all platforms and the
-vcg Examiner switch.

11                 Limitations and known errors

11.1          Tool limitations

This section describes limitations of the Examiner tool arising mainly from incomplete implementation of planned features.  Where appropriate a SPARK Examiner Performance Report (SEPR) number is given.

11.1.1  General

1         The SPARK 95 language definition removes the distinction between initial and later declarative items; this distinction remains in force in the Examiner that requires SPARK 83 declaration orders even in SPARK 95 mode. (SEPR 813)

2         The Examiner does not yet permit the use of 8-bit characters in SPARK 95 user-defined identifiers. (SEPR 818)

3         Universal expressions in a modular context may sometimes require type qualification. (SEPR 1591)

4         The Examiner does not yet permit the use of “use type” following an embedded package specification. (SEPR 747)

5         The Examiner does not yet permit the renaming of packages in the same way that subprograms can be renamed. (SEPR 1391)

6         The Examiner does not yet allow the ‘Base attribute when not used as a prefix. (SEPR 1114)

7         The Examiner does not yet allow S’Range where S is scalar. (SEPR 1115)

11.1.2  Verification Condition Generation and Run-time Checks

1         Ada string inequality and ordering operators are not modelled. (SEPR 712)

2         VCs involving string catenation that includes the character ASCII.NUL will be incorrect. (SEPR 661)

3         Aggregates of multi-dimensional arrays cannot be modelled although aggregates of arrays of arrays can. (SEPR 590)

4         Verification conditions involving real numbers are evaluated using infinite precision or perfect arithmetic; this allows the correctness of an algorithm to be shown but cannot guard against the effects of cumulative rounding errors for example.

5         The Examiner does not generate VCs for package initialization parts.  Statically determinable constraint errors will be detected during well-formation checking of package initialization. (SEPR 288)

6         The VC Generator cannot model the implementation-dependent attributes of floating and fixed-point types; see section 11.1.3.

11.1.3       Attribute limitations

11.1.3.1    Unimplemented attributes

The following attributes are officially supported by SPARK according to the language definition, but are not yet implemented by the Examiner.  The Examiner will generate error number 30 (“Attribute XXX is not yet implemented in the Examiner”) if you try to use them.

·          Adjacent

·          Compose

·          Copy_Sign

·          Leading_Part

·          Remainder

·          Scaling

·          Exponent

·          Fraction

·          Machine

·          Model

·          Rounding

·          Truncation

·          Unbiased_Rounding

Note that these are all function-like attributes concerning floating- and fixed-point types.

11.1.3.2    Unevaluable attributes

The Machine_* and Model_* attributes are accepted by the Examiner, but it does not know how to statically evaluate them since they are inherently implementation dependent.  For example, the package:

package F is

   type T is digits 6 range –10.0 .. 10.0;

   C : constant := T’Machine_Emax;

end F;

is legal SPARK, but the Examiner does not know the actual numeric value of C.

11.2          Known error summary

This section lists known errors in the Examiner that are awaiting investigation and correction.

1         The SPARK rule that array actual parameters must have the same bounds as the formal parameter is not checked for function parameters where the actual parameter is a subtype of an unconstrained array type.  Since subtype bounds are static in SPARK errors of this kind should be detected by an Ada compiler.  If not an unconditional run-time error will occur. (SEPR 1060)

2         The Examiner permits the body of a subprogram to be entirely made up of proof statements thus breaching the Ada rule that at least one Ada statement must be present. (SEPR 278)

3         Where a package declares two or more private types the Examiner permits mutual recursion between their definitions in the private part of the package. (SEPR 848)

4         The Examiner does not take due account of a range constraint when determining the subtype of a loop variable; this affects completeness checking of case statements within the loop.  For example for I in Integer range 1..4 loop would require only values 1, 2, 3 and 4 to be covered by the case statement. (SEPR 693)

5         When summarising the counts of pragmas found during an analysis the totals may depend on whether units are selected via the command line (or metafile) or using the index mechanism.  The difference affects only pragmas placed between program units and arises because placing a file name on the command line causes the entire file to be analysed whereas selecting it using indexes causes only the required unit to be read from the file. (SEPR 483)

12                 Change Summary from Release 2.0

A release note detailing changes from the previous version accompanies each toolset release; this section simply summarises the various changes that have been made.

12.1          Release 2.0 - November 1995

Release 2.0 added:

·          static expression evaluation;

·          variable initialization at declaration;

·          full-range scalar subtypes; and

·          operator renaming in package specifications.

12.2          Release 2.1 - July 1996

Release 2.1 added:

·          facilities for proof of absence of run-time errors

12.3          Release 2.5 - March 1997

Release 2.5 was distributed with “High Integrity Ada - the SPARK Approach” and provided initial facilities for SPARK 95

12.4          Release 3.0 - September 1997

Windows NT was supported for the first time with this release.  Release 3.0 also added:

·          additional SPARK 95 support;

·          flow analysis of record fields;

·          command line meta files;

·          named numbers;

·          unqualified string literals;

·          moded global annotations; and

·          optional information flow analysis.

12.5          Release 4.0 - December 1998

With Release 4.0 we upgraded all users to a single product standard supporting SPARK 83, SPARK 95 and analysis options up to an including proof facilities.  New features were:

·          full implementation of public and private child packages;

·          default switch file; and

·          provision of the INFORMED design document.

12.6          Release 5.0 - June 2000

·          Enhanced proof support:

                                            I.      facilities for proof of programs containing “abstract state”;

                                          II.      addition of quantified expressions;

                                         III.      proof rule generation for enumeration types;

                                        IV.      identification of the kind and source of each VC;

                                          V.      suppression of trivially true VCs;

                                        VI.      Proof Obligation Summariser tool (POGS)

·          Optional HTML output files with hyperlinks that can be “browsed” interactively

·          Better support for common Ada file naming conventions

·          User-selectable annotation character

·          Improved suppression of analysis were results might otherwise be misleading

·          Static expression evaluation in proof contexts

·          Singleton enumeration types

·          Revised SPARK_IO package

·          Error numbering

12.7          Release 6.0 - November 2001

·          Introduction of “external variables” to simplify modelling of the interactions between a SPARK program and its external environment.

·          Addition of the “null derives” annotation to describe information flows which affect only the external environment.

·          Introduction of modular types

·          Use of loop labels in exit statements

·          Use of global modes on function subprograms

·          Extended support for predefined types such as Long_Integer

·          Simplified run-time check generation for own variables

·          Relaxation of need for mandatory type announcement of own variables

·          Plain output option to simplify comparisons of Examiner output files

·          Platform-independent switch files and metafiles

·          Support for intentionally infinite loops

·          Detection of own variables that can never be initialized

·          Detection of unusable private types

·          Extra refinement checks on global variables when performing data flow analysis

·          Detection of unnecessary others clause in case statements

·          Extensions to the POGS tool

·          Improved error messages to distinguish different cases of variables which are “not declared or visible”

·          Improved SPADE Simplifier Release 2.0

·          New “SPARKSimp” Tool

12.8          Release 6.1 - June 2002

·          Introduction of tagged types

·          Introduction of type assertion annotations

·          Introduction of modular subtypes

·          Introduction of the configuration file

·          Introduction of the help command line switch

·          Demo Examiner now runs on Linux.

·          VCG generation for inherited operations of tagged types

·          Improved handling of null derives

·          Attributes ‘Floor and ‘Ceiling implemented

·          Detection of duplicate record fields

·          Improved overflow checks on universal integer expressions

·          Corrected handling of loop invariants in while loops

·          Strengthened behaviour of /noecho option

·          Trapping non-positive accuracy in real type declaration

·          Recursion in meta-files and index-files

·          Improved handling of Address clauses

·          Improved handling of Import and Interface pragmas

·          VCG Modelling of Boolean membership operators

·          Simplification of common Integer inequalities

·          Simplification of common enumerated inequalities

·          Simplification of VCs involving quantified expressions

·          Simplifier performance

·          Checker has new built-in rule families: MODULAR, BITWISE and ENUMERATION

·          Proved by review option in POGS

12.9          Release 6.3 – December 2002

Release 6.3 of the toolset was constructed to accompany the textbook “High Integrity Software: The SPARK Approach to Safety and Security” by John Barnes, but was not delivered to other users.  Its main new features were:

·          Slight revision to the rules regarding the placement of tagged type declarations.

·          Correction to the modelling of Boolean type membership operators in the verification conditions.

·          Support for generating VCs that allow the verification of the Liskov Substitution Principal (LSP) for tagged types and their operations.

·          Dramatically improved performance of the Simplifier, particularly in the simplification of quantified expressions.

12.10    Release 7.0 – July 2003

Release 7.0 of the toolset comprised:

Examiner version 7.0

Simplifier version 2.12

Release 7.0 added:

·          Ravenscar profile extensions to the language.

·          Support for Ada.Interrupts and Ada.Real_Time in the configuration file.

·          The new /noduration command line switch.

·          VC generation for unconstrained formal parameters.

·          Suppression of VC generation for illegal function bodies.

·          New “SPARKFormat” tool.

12.11    Release 7.2 – December 2004

Release 7.2 of the toolset comprised:

Examiner version 7.2

Simplifier version 2.17

Release 7.2 added:

·          Unconstrained string constants to the language.

·          Instantiation of Unchecked_Conversion to the language.

·          (Full) record subtypes to the language.

·          Declaration of subprograms in the private part of packages.

·          Refined proof annotations for private types.

·          % suffix for referring to value of variable on entry to loop in proof contexts.

·          Extra hypotheses for local variables.

·          Suppression of VC generation for illegal function bodies.

·          Replacement rules for composite constants.

·          Concurrent simplification with SPARKSimp.

·          Improved simplification of VCs with large structured objects.

·          Improved simplification of arithmetic and logical expressions.

·          New “SPARKMake” tool.

12.12    Release 7.3 – February 2006

Release 7.3 of the toolset comprised:

                   Examiner version 7.3

                   Simplifier 2.22

                   Checker 2.06

Significant features of this release included:

·          Improved VC Generation.

·          New “error explanations” switch for Examiner.

·          Generation of proof rules for ‘Size.

·          Improved diagnosis and reporting of common syntax errors.

·          Error and warning count summary in Examiner output.

·          Use of pragma Import to complete an external own variable.

·          Correction to FDL declaration order for private and announced types.

·          New Simplifier tactics for dealing with rational inequalities and Examiner-generated proof rules.

·          User-defined proof rules for the Simplifier.

·          New Checker rules for MODULAR expressions.

·          Significant performance improvement for Simplifier and Checker.

12.13    Release 7.31 – April 2006

Release 7.31 of the toolset comprised:

                   Examiner version 7.31

                   Simplifier 2.24

                   Checker 2.07

Significant features of this release included:

·          Correction to flow analysis of array element “out” parameters.

·          Port of “Demo” toolset to Mac OS X.

·          New /typecheck option in Simplifier.

·          Improved validity checking of user-defined proof rules in the Simplifier.

·          Correction to ARITH proof rules in the Checker.

12.14    Release 7.4 – January 2007

Release 7.4 of the toolset comprised:

                   Examiner version 7.4

                   Simplifier 2.30

                   Checker 2.08

Significant features of this release included:

·          The ‘accept’ annotation.

·          Conditional flow errors are now reported as errors.

·          The Simplifier supports user defined proof rules.

·          SPARKFormat supports a wider range of annotations.

·          SPARKMake has the ability to generate relative pathnames.

12.15    Release 7.5 – May 2007

Release 7.5 of the toolset comprised:

                   Examiner version 7.5

                   Simplifier 2.32

                   Checker 2.08

Significant features of this release included:

·         Correct VC generation for record fields and array elements used as “in” or “in out” parameters.

12.16    Release 7.6 – June 2008

Release 7.6 of the toolset comprised:

                   Examiner version 7.6

                   Simplifier 2.39

                   Checker 2.11

Significant features of this release included:

·         Allows single-field record type to be Atomic in RavenSPARK mode.

·         Simpler modelling of Character’Pos and ‘Val in VCs.

·         Better modelling of S’Valid where S is a subtype.

·         New “Output_Directory” option for the Examiner.

·         New “Order” option for SPARKFormat.

12.17    Release 7.6.2 – February 2009

From release 7.6.2 of the toolset the version numbers of all the SPARK tools were made consistent, ie all tools had the version number 7.6.2. This was an interim release, the significant feature being the correction to SEPR 2517. All users were informed of the availability of this release and it was made available on demand. As the majority of users did not take this release, the changes detailed in the release note for 7.6.2 were also included in the release note for 8.1.0.

12.18    Release 8.1.0 – March 2009

Significant features of this release included:

·         New –vcg and –noswitch Examiner switches;

·         Documentation of the Examiner’s –debug switch;

·         Significantly improved Simplifier performance.

·         New platforms supported in SPARK Pro: 32-bit Linux, 64-bit Linux, Apple OS X.

 

 

 

13                 Operating system compatibility

13.1          VAX/VMS

Toolset 8.1.1 is not available on VAX/VMS.

13.2          SPARC/Solaris

The toolset is compatible with Solaris 8 through to 10 including those with a 64-bit kernel.

n.b. Solaris 6 and 7 are no longer supported.

13.3          Windows

The toolset is compatible with Windows XP, Server 2003, 32-bit Vista, and 64-bit Vista.

13.4          Intel/Linux

The toolset is compatible with Intel x86-based Linux operating systems, in both 32-bit and 64-bit versions. The toolset is built, tested and packaged on RedHat Enterprise Linux 4.7. Other distributions may work, but are not formally supported.

13.5          Apple OS X

The toolset is compatible with Apple’s Intel-based OS X/Darwin operating systems. The toolset is built and tested on OS X version 10.5.6.

Document Control and References

Praxis High Integrity Systems Limited, 20 Manvers Street, Bath BA1 1PX, UK.

Copyright Praxis High Integrity Systems Limited 2009. All rights reserved.

Changes history

Issue 0.1 (20th August 2008):  First draft for release 7.6.1

Issue 0.2 (21st August 2008):    First draft for release 7.6.2, adding SEPR 2437

Issue 0.3 (28th August 2008):  Added SEPR 2432 regarding “-“ as a switch character.

Issue 0.5 (16th September 2008): Added new “-vcg” Examiner switch (SEPR 2475).

Issue 0.6 (18th September 2008): Removed references to free demo (SEPR 2476).

Issue 0.7 (6th November 2008): Added SEPR 2495 regarding visibility in protected types.

Issue 0.8 (12th November 2008): Added section for SEPR 2517.

Issue 0.9 (21st November 2008): Added SEPR 2531 and 2532.

Issue 1.0 (24th November 2008): Added subsection regarding Examiner debug switches.

Issue 1.1  (26th November 2008): Definitive issue following review.

Issue 1.2 (12th December 2008): Update for release 7.6.3. Change to generation and suppression of warning 302 (SEPR 2548).

Issue 1.3 (9th January 2009): Factor out contact details.

Issue 1.4 (13th January 2009): Added SEPRs 2557 and 2558.

Issue 1.5 (2nd February 2009): Modify copyright notice.

Issue 1.6 (3rd February 2009): Update for release 8.0.0.

Issue 1.7 (16th February 2009): Update for release 8.0.1 on Windows (SEPR 2612)

Issue 1.8 (13th March 2009): Update for release 8.0.2 (SEPRs 2597 and 2622)

Issue 1.9 (17th March 2009): Update for release 8.1.0.

Issue 2.0 (18th March 2009): Definitive issue following review S.P0468.7.104.

Issue 2.1  (30th March 2009): First draft following release 8.1.0.

Issue 2.3 (9th March 2009): Remove –concat and –tree switches from Examiner (SEPR 2665)

Issue 2.4 (15th April 2009): Document known error in VCG recorded in SEPR 608.

Issue 2.5 (16th April 2009): SEPR 608 now fixed, so move to section 3.4.

Issue 2.6 (20th April 2009): Added note on SPARKMake behaviour (SEPR 2678).

Issue 2.7 (22nd April 2009): Document SPARKFormat improvement (SEPR 2674).

Issue 2.8 (24th April 2009): Updates list of changed user manuals (SEPR 2682).

Issue 2.9 (24th April 2009): Add section 3.5 describing SEPR 2684.

Issue 3.0  (27th April 2009): Definitive issue following review 7.148 and final cross-check against verification report.

 

Changes forecast

None.

Document references

None.

File under

SVN:trunk/userdocs/Release_Note_HEAD.doc