|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Issue: 2.0 Status: Definitive
DOCTYPE:Praxis title:varchar=title reference:varchar=reference status:varchar=status issue:varchar=issue date:varchar=date projectname:varchar=DocumentSet Issue 2.0, Definitive, 18th March 2009 000_000 SPARK Toolset Release Note 8.1.0
|
|
|
|
Originator |
|
|
|
|
|
|
|
Approver |
|
|
|
SPARK Team Line Manager |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
||
|
|
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
4 SEPR 2517 – Important Information for Users
4.2 SPARK Examiner versions affected
5.1 OptFlow and RealRTCs options now always enabled (SEPR 2431)
5.2 Command-line switches using “-” on Windows (SEPR 2432)
5.4 “Real” is an FDL reserved identifier (SEPR 2437)
5.5 New –vcg Examiner switch (SEPR 2475)
5.6 Correction to scope checking in protected types (SEPR 2495)
5.7 New –noswitch Examiner switch (SEPR 2531)
5.8 Improvements to brief output mode
5.9 Documentation of Examiner “debug” switches
5.10 Change to behaviour of warning 302 for ambiguous expression ordering
5.11 Removal of largespark.exe (SEPR 2551)
6.1 Replace echo switch with verbose switch (SEPR 2390)
6.2 Concise rule error syntax reporting (SEPR 2212)
6.3 Command-line switches may use “-” (SEPR 2432)
6.4 Introduce a help switch (SEPR 2308)
6.5 Introduce a version switch (SEPR 2006)
6.6 Correctly parse limit switches (SEPR 2444)
6.7 Prevent infinite-loop in reasoning about implication (SEPR 2506)
6.8 Improve restructuring of quantified expressions (SEPR 2611)
6.9 Improve Simplifier performance for range of size 0 (SEPR 2622)
6.10 Improve Simplifier performance by refactoring hypothesis database (SEPR 2597)
7.1 Command-line switches using “-” on Windows (SEPR 2432)
7.2 Introduce a version and help switch (SEPR 2456)
7.3 Correct behaviour of resume switch (SEPR 2450)
7.4 Remove line printer support (SEPR 2490)
7.5 Improvement to inference routines (SEPR 2503)
7.6 Improve restructuring of quantified expressions (SEPR 2611)
8.1 Command-line switches using “-” on Windows (SEPR 2432)
8.2 Treat PRV file errors consistently (SEPR 2406)
8.3 Input directory switch (SEPR 2557)
8.4 Output file switch (SEPR 2558)
9.1 Command-line switches using “-” on Windows (SEPR 2432)
9.2 New –noswitch switch (SEPR 2531)
10.1 Command-line switches using “-” on Windows (SEPR 2432)
11.1 Command-line switches using “-” on Windows (SEPR 2432)
13 Limitations and known errors
14 Change Summary from Release 2.0
14.1 Release 2.0 - November 1995
14.4 Release 3.0 - September 1997
14.5 Release 4.0 - December 1998
14.7 Release 6.0 - November 2001
14.9 Release 6.3 – December 2002
14.11Release 7.2 – December 2004
14.12Release 7.3 – February 2006
14.13Release 7.31 – April 2006
14.14Release 7.4 – January 2007
14.17Release 7.6.2 – February 2009
15 Operating system compatibility
Document Control and References
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.0.
This document describes changes in the behaviour of all variants of the SPARK Toolset Release 8.1.0 compared to Release 7.6.
This section describes SPARK language changes supported by Toolset Release 8.1.0.
None.
From this release onwards, all SPARK tools now report the same, consistent version number. All tools have a “version” switch that reports the tool’s name, version number, build date and build number. For example:
spark –version
Reports
*******************************************************
SPARK Examiner Pro Edition, Version 8.1.0, Build Date 20090320, Build 12345
Copyright (C) 2009 Praxis High Integrity Systems Ltd., Bath, U.K.
*******************************************************
The “Build Date” is 8 digits, reported as year, month and day when the tool was constructed.
4 SEPR 2517 – Important Information for Users
SEPR 2517 concerns a case where the Examiner can generate incorrect proof rules for unconstrained formal parameters of type String when the null String literal “” is passed as an actual parameter.
The incorrect rules mean that the Simplifier and POGS may report all VCs proved for a subprogram, even though a potential run-time error does exist.
The exact circumstances for this problem to occur are as follows:
· A subprogram takes an unconstrained formal parameter of type String.
· The body of that subprogram assumes that the given String parameter is at least one character long (or, more specifically, assumes that the ‘Last of the given String is greater than or equal to one.)
· A calling unit calls that subprogram, but passes the null string literal “” (or a constant with that value) as the actual parameter.
Unconstrained array types other than String are not affected.
4.2 SPARK Examiner versions affected
Examiner versions 7.4, 7.5 and 7.6 are affected by this problem.
Prior to version 7.4, the null string literal “” was not supported by the VC generator at all, so these versions cannot be affected. The problem was corrected in release 7.6.2.
Consider the following function:
function SL (Data : String) return Positive is
begin
return Data'Length;
end SL;
Release 7.6 of the toolset discharges all VCs associated with this function, which is not correct, since Data’Length could be 0 if the null String literal “” has been passed as the actual parameter. This would then result in a Constraint_Error since the function is expected to return a Positive value.
The defect lies in the proof rules generated by the Examiner for String parameters. In this case:
sl_rules(17):
data__index__subtype__1__first >=
positive__first may_be_deduced.
sl_rules(18): data__index__subtype__1__last
<=
positive__last may_be_deduced.
sl_rules(19): data__index__subtype__1__first
<=
data__index__subtype__1__last
may_be_deduced.
sl_rules(20): data__index__subtype__1__last
>=
positive__first may_be_deduced.
sl_rules(21): data__index__subtype__1__first
<=
positive__last may_be_deduced.
sl_rules(22): data__index__subtype__1__first may_be_replaced_by 1.
Rules 17, 18, 21 and 22 are correct, but rules 19 and 20 are not, since for a string T where T = “”, T’First = 1 but T’Last = 0 — the only case of a null-range array object in SPARK.
Now, the Examiner generates a different set of rules:
string_lengt_rules(17):
data__index__subtype__1__first
may_be_replaced_by 1.
string_lengt_rules(18):
data__index__subtype__1__last <=
positive__last may_be_deduced.
string_lengt_rules(19): data__index__subtype__1__last
>= 0
may_be_deduced.
Reflecting that T’Last might be zero.
With these rules, the test case above leaves a single undischarged VC as expected.
We recommend the following actions:
· Review the Examiner version in use with respect to section 5.2 above.
· Review source code for any use of the null string literal “”.
· If users’ code does make use of “”, then we recommend a complete back-to-back analysis and “diff” of proof results using toolset 8.1.0.
· Following re-analysis with 8.1.0, some subprograms may produce undischarged VCs that were previously proved. Such instances should be reviewed carefully to determine if the code in question is robust in the face of a null string parameter.
· Users may choose to add a pre-condition to subprograms that are not willing to take an actual parameter which is a null string. For example, adding:
function SL (Data : String) return Positive
--# pre Data’Last > 0;
is
begin
return Data'Length;
end SL;
restores the 100% proof of this subprogram, but moves the obligation onto calling units to supply a non-null parameter.
This section documents other significant changes to the SPARK Examiner made for release 8.1.0. Where appropriate, SPARK Examiner Performance Report (SEPR) numbers are given.
5.1 OptFlow and RealRTCs options now always enabled (SEPR 2431)
The “Optflow” (-flow=data switch in SPARK83 mode) and RealRTCs (-realrtcs switch) are now enabled at all times. They are no longer controlled by a FLEXlm licence feature.
5.2 Command-line switches using “-” on Windows (SEPR 2432)
On Windows, the Examiner now accepts either “/” or “-” to introduce command-line switches.
In future, the use of “/” on Windows will be removed, so all users should consider moving to the use of “-” in analysis scripts and spark.sw files at this point.
5.3 Examiner capacity overflow for warnings 392 and 393 when error explanations are active (SEPR 2438)
In developing release 7.6, the explanations of warnings 392 and 393 became longer. This can cause a capacity limit to be exceeded in the Examiner in the following circumstances:
· Code under analysis raises warning 392 or 393.
· The Examiner is run with –error_explanations=first or –error_explanations=every.
Workaround: if you encounter this problem with release 7.6, then run the Examiner with –error_explanations=off. This defect is corrected in release 8.1.0.
5.4 “Real” is an FDL reserved identifier (SEPR 2437)
“Real” is the name of a pre-defined type in FDL, and so should be classed as an FDL reserved identifier by the Examiner. Release 7.6 did not do this, and SPARK programs using “Real” as an identifier could generate illegal FDL that would be rejected by the Simplifier.
Release 8.1.0 corrects this issue. The use of “Real” as an identifier in SPARK is now rejected when “-fdl=reject” is active.
The “fdl=<identifier>” switch can be used to analyse legacy code which breaks this rule.
5.5 New –vcg Examiner switch (SEPR 2475)
The Examiner supports a new switch “-vcg” that generates all VCs, including those for Overflow_Check and all real-numbers. This is equivalent to the combination of existing switches ”-exp -real”.
We recommend that all users should now use “-vcg” at all times. In future, the “-rtc”, “-exp” and”-real” switches will become obsolete and will be removed from the Examiner.
5.6 Correction to scope checking in protected types (SEPR 2495)
Note that this applies to RavenSPARK only.
When analysing the private part of a protected type, which was itself in the visible part of a public child package, previous versions of the Examiner would incorrectly permit visibility of entities in the private part of the parent package. This has now been corrected.
5.7 New –noswitch Examiner switch (SEPR 2531)
The Examiner supports a new switch “-noswitch” that suppresses processing of the default switch file. This can be useful when the Examiner is invoked from an IDE, or in general when the user wishes to override the default switch file for a particular analysis run.
5.8 Improvements to brief output mode
The format of messages produced by the Examiner in brief output mode (-brief) has been modified for improved compatibility with IDEs such as GPS. Previously, the Examiner would include ‘:’ characters around the error or warning number which could be incorrectly interpreted by the IDE, eg:
cells.adb:297:8: Flow Error:602: The undefined initial value of X may be used in the derivation of Y.
From this release, the additional ‘:’ characters have been replaced, eg:
cells.adb:297:8: Flow Error 602 - The undefined initial value of X may be used in the derivation of Y.
5.9 Documentation of Examiner “debug” switches
The Examiner User Manual (section 3.1.4) now documents the “debug” command-line option that allows various forms of tracing and debugging information to be produced by the Examiner as it runs.
5.10 Change to behaviour of warning 302 for ambiguous expression ordering
In Examiner 7.6 and earlier, warning 302 is issued if VCs are being generated and an expression is encountered with a potentially ambiguous evaluation order that could affect the validity of RTC Proof.
Here, this behaviour has been changed. Warning 302 is now always raised for such expressions, regardless of whether the VC Generator is active. To reduce false alarm rate, the warning is suppressed in two cases. Firstly, if an expression is in a context where a static expression is required, then no ambiguity exists and a compiler will always evaluate that expression with no possibility of arithmetic overflow. For example:
type T is range B * 2 / 3 .. 100;
does not result in an instance of warning 302.
Secondly, modular types have no overflow check associated with them, so this warning is suppressed for an expression that has a sequence of equal-precedence operators which are identical and commutative – namely addition and multiplication. For example:
type T is mod 256
D : constant T := A + B + C;
Does not raise warning 302, since (A + B) + C = A + (B + C) in “mod 256” arithmetic.
A new warning control file keyword “expression_reordering” is also available which suppresses the generation of warning 302 if the VC Generator is not active.
Warning 302 can always be suppressed with the use of an accept annotation.
5.11 Removal of largespark.exe (SEPR 2551)
Previously, the executable files provided in the SPARK Toolset included both spark and largespark. Despite the different names, largespark was simply an exact copy of spark. To avoid confusion, the duplicate executable largespark is now no longer provided as part of the SPARK Toolset.
Simplifier 8.1.0 includes the following improvements, and includes the following changes.
6.1 Replace echo switch with verbose switch (SEPR 2390)
Previously, where an -echo switch was present, two operations would be performed. Firstly, as the VCG file was read in, it would be displayed on the screen. Secondly, the top-level simplification strategies attempted would be displayed on the screen. The echo command is now removed, and a new switch
-verbose is available. The verbose switch only provides the second behaviour of the old echo switch: where the verbose switch is present, the top-level simplification strategies attempted are displayed on the screen.
6.2 Concise rule error syntax reporting (SEPR 2212)
Previously, under some circumstances, where a syntax error was detected in a rule file the same error would be reported twice - once with little contextual information, and again with the contextual information in place. Now, each error is displayed only once, with the contextual information in place.
6.3 Command-line switches may use “-” (SEPR 2432)
On all platforms, the Simplifier now accepts either “/” or “-” to introduce command-line switches. In future, the use of “/” will be removed, so all users should consider moving to the use of “-” at this point.
6.4 Introduce a help switch (SEPR 2308)
The simplifier now accepts a “-help” switch on the command line. Where present, the Simplifier will report its version information followed by a brief summary of the various switches accepted.
6.5 Introduce a version switch (SEPR 2006)
As described in section 3, the Simplifier now accepts a “-version” switch.
6.6 Correctly parse limit switches (SEPR 2444)
Previously, the simplifier failed to accept legal forms of the limit switches: -complexity_limit=Limit, -depth_limit=Limit, -inference_limit=Limit. This error has been resolved.
6.7 Prevent infinite-loop in reasoning about implication (SEPR 2506)
Previously, where reasoning about implication, the Simplifier may have entered an infinite loop, eventually running out of resources and failing with ‘! too many dynamic choicepoints’. The reasoning strategy is now modified, to prevent the Simplifier from entering this infinite-loop.
6.8 Improve restructuring of quantified expressions (SEPR 2611)
Previously, the Simplifier never performed type simplification during the restructuring of quantified expressions. Further, in certain cases, the Simplifier could abort during the restructuring of quantified expressions. The Simplifier is improved so that it no longer aborts on these cases. Additionally, the Simplifier now attempts to perform a type simplification during the restructuring of quantified expressions.
6.9 Improve Simplifier performance for range of size 0 (SEPR 2622)
Previously, the Simplifier took a considerable time to simplify VCs that corresponded to SPARK code containing several occurrences of size zero types (e.g. “type X is range 0 .. 0;”). The Simplifier is modified so that it now offers significantly improved performance for these cases.
6.10 Improve Simplifier performance by refactoring hypothesis database (SEPR 2597)
This SEPR improved the performance of Simplifier by refactoring code for managing the hypothesis database. For example, the SHOLIS application software generates 9685 VCs. Version 8.0.1 of the Simplifier processes these in 675 seconds (Quad-Core Intel Core i7 processor), while version 8.1.0 produces identical results in 329 seconds – slightly over twice as fast.
6.11.1 Command-line switches using “-” (SEPRs 2432, 2612)
On all platforms, SPARKSimp now accepts “-” to introduce command-line switches.
On Windows, SPARKSimp also accepts “/” to introduce switches for backwards compatibility with existing scripts and development environments. We recommend that all users should switch to using “-” as soon as possible.
Proof Checker 8.1.0 includes the following improvements and changes:
7.1 Command-line switches using “-” on Windows (SEPR 2432)
On Windows, the Checker now accepts either “/” or “-” to introduce command-line switches. In future, the use of “/” on Windows will be removed, so all users should consider moving to the use of “-” at this point.
7.2 Introduce a version and help switch (SEPR 2456)
The Checker now accepts a “-help” switch on the command line. Where present, the Checker will report its version information followed by a brief summary of the various switches accepted. As described in section 3, the Checker also now accepts a “-version” switch.
7.3 Correct behaviour of resume switch (SEPR 2450)
The Checker resume facility now operates correctly. However, the resume facility may now only be requested via the resume switch on the command line (previously, the intention was that a resume could also be specified interactively).
7.4 Remove line printer support (SEPR 2490)
Originally, the Checker ‘printvc’ command was intended to send the current VC to an external line printer. The behaviour of the command is now modified, removing line printer support, and instead storing the current VC into a file.
7.5 Improvement to inference routines (SEPR 2503)
The Checker’s inference routines were wrongly restricted following certain reasoning activities. For example, in performing a proof by cases, with two cases, a proof of the first case (a reasoning activity) may hinder the Checker’s ability to prove the second case. The over-eager restriction of the inference routines is now removed, increasing the Checker’s reasoning abilities.
A consequence of this change is that this version of the Checker may behave differently to earlier versions of the Checker on the same proof commands. This has the capacity to impact regression proof where a CMD script generated with a previous version of the Checker is used to drive this version of the Checker. Where migrating to this Checker, three possible scenarios are possible:
1 No change – No change is observed. This is quite likely, especially if the CMD file does not contain proofs by cases. No actions are required.
2 Different PLG file, but overall proof is the same – This version of the Checker may reach a proof in a different manner, possibly raising syntax errors. Here, this leads to a different PLG file, while the actual numbers of the VCs proved remain the same. The reference PLG results should be updated to reflect the different route to proof.
3 Different PLG file, and overall proof is different – This version of the Checker may become out-of-synch with the CMD file such that some proofs are no longer found, possibly raising syntax errors. Here, this leads to a different PLG file, and a reduced number of VCs proved. The CMD file will need to be updated to recover overall proof. Note that the differences in the PLG file should give strong guidance on what changes need to be made to the CMD file. Once a correct CMD file has been determined, the reference PLG results should be updated.
7.6 Improve restructuring of quantified expressions (SEPR 2611)
In certain cases, the Checker could abort during the restructuring of quantified expressions. The Checker is improved so that it no longer aborts on these cases.
POGS 8.1.0 includes the improvements covered in the following subsections.
8.1 Command-line switches using “-” on Windows (SEPR 2432)
On Windows, POGS now accepts either “/” or “-” to introduce command-line switches.
In future, the use of “/” on Windows will be removed, so all users should consider moving to the use of “-” at this point.
8.2 Treat PRV file errors consistently (SEPR 2406)
Previously, an error in a PRV file was treated inconsistently when compared to errors detected in other files. Now, as for errors detected other files, an error in a PRV file leads to its subprogram table being suppressed and its subprogram being counted in the summary table of subprograms with errors.
8.3 Input directory switch (SEPR 2557)
POGS now supports a new switch, -d=directory. When this switch is present, POGS will search for proof files to summarise in the specified directory and its subdirectories. It will write its output to a summary file named directory.sum within the specified directory (unless this is overridden by the –o switch). For more details see the POGS User Manual.
8.4 Output file switch (SEPR 2558)
POGS now supports a new switch, -o=output_file. When this switch is present, POGS will write its summary output to the specified file. For more details see the POGS User Manual.
SPARKFormat version 8.1.0 includes the following changes and improvements:
9.1 Command-line switches using “-” on Windows (SEPR 2432)
On Windows, SPARKFormat now accepts either “/” or “-” to introduce command-line switches.
In future, the use of “/” on Windows will be removed, so all users should consider moving to the use of “-” at this point.
9.2 New –noswitch switch (SEPR 2531)
SPARKFormat supports a new switch “-noswitch” that suppresses processing of the default switch file (as per the Examiner change described in section 5.7).
SPARKMake 8.1.0 includes the following changes and improvements:
10.1 Command-line switches using “-” on Windows (SEPR 2432)
On all platforms, SPARKMake now requires “-” to introduce command-line switches.
The following backward incompatibilities were introduced between Examiner Releases 7.6 and 8.1.0.
11.1 Command-line switches using “-” on Windows (SEPR 2432)
For consistency across tools and platforms the SPARKMake tool now requires “-“ to introduce command-line switches on all platforms. Previous versions of this tool required “/” to introduce switches on Windows. Any scripts which invoke this tool on Windows platforms and specify options using “/” will need to be modified to use “-“.
The following user manuals have been changed between Examiner Releases 7.6 and 8.1.0.
· Examiner User Manual
· Allows for “-” to introduce command-line switches on Windows.
· Lists “real” as an FDL reserved identifier.
· Adds documentation of “debug”, “dictionary_file”, “vcg” and “noswitch” switches.
· Simplifier User Manual
· Allows for “-” to introduce command-line switches on Windows.
· Checker User Manual
· Describe amended switch format and the new help and version switches.
· Describe the modified behaviour of the ‘printvc’ command.
· Generation of VCs manual
· Lists “real” as an FDL reserved identifier.
· SPARKMake User Manual
· SPARKMake now requires “-“ to introduce command-line switches on all platforms.
· POGS User Manual
· Allows for “-” to introduce command-line switches on Windows.
· Includes new switches “-d” and “-o”.
· SPARKFormat User Manual
· Allows for “-” to introduce command-line switches on Windows.
· Describes –noswitch option.
13 Limitations and known errors
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.
13.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)
13.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 13.1.3.
13.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.
13.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.
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)
14 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.
14.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.
Release 2.1 added:
· facilities for proof of absence of run-time errors
Release 2.5 was distributed with “High Integrity Ada - the SPARK Approach” and provided initial facilities for SPARK 95
14.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.
14.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.
· 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
14.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
· 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
14.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.
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.
14.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.
14.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.
14.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.
14.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.
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.
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.
14.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 are also included in the release note for 8.1.0.
15 Operating system compatibility
Toolset 8.1.0 is not available on VAX/VMS.
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.
The toolset is compatible with Windows NT 4.0, 2000, Server 2003, XP and Vista.
The toolset is compatible with Intel-based Linux operating systems, in both 32-bit and 64-bit versions.
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.
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.
None.
None.
SVN:trunk/userdocs/Release_Note_8.doc