Issue: 1.1 |
||
Status: Definitive |
||
8th May 2001 |
||
|
||
Originator |
|
|
Rod Chapman |
||
|
||
Approver |
|
|
Peter Amey |
||
|
||
|
||
|
|
|
|
|
|
|
|
|
Continued Examiner development has led to version 5.03 which is a development of the current full commercial release, 5.0. This Release Note briefly describes the changes made. It is intended for those making use of Examiner Release 5.03 prior to the next full Examiner release. This document should be read in conjunction with the Release Note for Release 5.0
For further information about this document please contact Praxis Critical Systems:
By phone: 01225 466991
By FAX: 01225 469006
By email: sparkinfo@praxis-cs.co.uk
The verification condition generator does not word-wrap long type attribute names in the generated VCG file.
The InstallShield application for Windows NT has been corrected to modre robustly handle the setting of environment variables, and to co-exist with other tools, such as Rational APEX.
The Examiner no longer malfunctions when both a superindex and an auxiliary index file are references in a single index file.
The Examiner now generates a valid proof model of for loops through type Boolean. Previously the FDL model generated included inequalities between Boolean types which are not permitted.
The Examiner now warns if it detects a declaration of an own variable where there is no means by which the own variable could ever be given an initial value. The warning is issued if:
· the own variable is not declared in the visible part of the package (where it could be directly assigned to); and
· the own variable does not appear in an initialization clause (stating that it is initialized during elaboration or by the system environment); and
· there is no exported procedure which exports the own variable without importing it.
Under certain uncommon circumstances, the Examiner wrongly considered global variables to be visible when they were not. The problem was associated only with own variables declared in the visible part of a package being viewed from inside a loop. There was no risk of an undetected error occurring since consequential error messages were always generated. SEPR 889 corrects this problem. SEPR 1083 is a special case of this problem involving record fields.
Certain malformed Examiner command lines (e.g. spark /i ) where an expected argument was omitted caused the Examiner to terminate with a constraint error.
If an abstract own variable was “type-announced” and there was no abstract definition of that type provided, the somewhat misleading error message "XXX has already been declared or refined" was issued if a later attempt was made to refine the own variable. The error message is misleading since at the point where it is issued the own variable is neither declared nor refined! SEPR 1085 tries to distinguish between an illegal refinement and a missing abstract type declaration and provide a suitable error message for each case.
Ada 95 attribute ΄Valid is now implemented.
When the Examiner cross checked global modes against the derives annotation any errors were not prefixed with the package name which could make them hard to understand. SEPR 1094 adds package prefixes where necessary.
If a type was announced in an own variable declaration and was later implemented as an unconstrained array type the Examiner gave the message "Private types may not be unconstrained arrays"; this is a bit misleading. SEPR 604 provides appropriate error messages for the own variable and private type cases.
When the predefined ** (exponentiation) operator is used with a Float parameter as Left, and an Integer as Right, there is the possibility of Constraint_Error being raised if Left = 0.0 and Right is negative. When in /rtc /real or /exp /real mode, the Examiner did not generate a VC to eliminate this exception. SEPR 1004 adds a check of the form:
--# check (Left = 0.0) -> Right >= 0;
for all occurrences of Left ** Right where Left is of any floating point type and Right is an Integer type. See LRM 4.5.6(9-13)
The Examiner wrongly allowed package prefixes to be repeated in annotation expression. For example, it is possible to refer to variable X in package P as P.P.P...X. SEPR 1029 corrects this error.
The rules of SPARK require that array component subtypes statically match in array type conversions. Prior to SEPR 1079 the Examiner generated RTC VCs to show this; however, the Examiner also checks this statically. Since no well-formed SPARK array type conversion can cause a run-time error the RTC check is unnecessary and has been removed.
The Examiner index mechanism malfunctioned if an attempt was made to look up children of package Ada. SEPRs 1099 and 1103 correct this error.
All Ada95 Attributes are now recognized in SPARK95 mode, although a number listed in the SPARK95 report remain unimplemented in this release. The unimplemented attributes are: 'Ceiling, 'Exponent, 'Floor, 'Fraction, 'Machine, 'Model, 'Rounding, 'Truncation, 'Unbiased_Rounding, 'Adjacent, 'Compose, 'Copy_Sign, 'Leading_Part, 'Remainder, 'Scaling, 'Base (when not used as a prefix), and S'Range (where S is a scalar.)
A mal-formed pragma Import (SPARK95) or Interface (SPARK83) does not complete the body of the corresponding subprogram.
When Examiner semantic “notes” are suppressed in the warning control file, the total number of these is now correctly reported in the Examiner Report file.
Attributes (such as 'First and 'Last) of constrained subtypes of unconstrained arrays are now allowed by the Examiner.
The Examiner now issues a warning when a “others” clause is redundant in a case statement. A new keyword “others_clauses” can be used to suppress this warning in the warning control file.
The “POGS” tool now recognizes and processes the verification conditions produced by the Examiner for the refinment of abstract own variables.
The Examiner now allows global variables of functions to have an explicit “in” mode.
The SPARK95 attributes 'Min and 'Max are now fully implemented.
Since its release, a single new problem has been discovered with release 5.03. If a case statement over a type with the same range as type Natural (i.e. 0 .. Integer'Last) is written and the case statement has an 'others' clause the Examiner may raise a constraint error and stop; this will be reported as "unexpected internal error".
Document Control and References
Praxis Critical Systems Limited, 20 Manvers Street, Bath BA1 1PX, UK.
Copyright Praxis Critical Systems Limited 2001. All rights reserved.
Issue 0.1 (31st Janiary 2001): First draft
Issue 1.0 (2nd February 2001): Definitive issue following inspection.
Issue 1.1 (8th May 2001): Updated to include known problems in 5.03.
Nil.