Tool Development and Support

SPARK Examiner Release Note - Release 5.03

S.P0468.73.77

Issue: 1.1

Status: Definitive

 8th May 2001

 

Originator     

 

Rod Chapman

 

Approver      

 

Peter Amey

 

 

 

 

 

 

 

 



Contents

1       Introduction

2     Contact Information

3     Changes Introduced at 5.01

3.1   SEPR 1073

4     Changes Introduced at 5.02

4.1   SEPR 1072, 1075

4.2   SEPR 1081

5     Changes Introduced at 5.03

5.1   SEPR 714, 1101

5.2   SEPR 726

5.3   SEPR 889, 1083

5.4   SEPR 1082

5.5   SEPR 1085

5.6   SEPR 1090, 1106

5.7   SEPR 1094

5.8   SEPR 604

5.9   SEPR 1004

5.10SEPR 1029

5.11SEPR 1079

5.12SEPR 1099, 1103

5.13SEPR 814

5.14SEPR 823

5.15SEPR 830

5.16SEPR 855

5.17SEPR 1054

5.18SEPR 1065

5.19SEPR 1095

5.20SEPR 1107, 1110

5.21Known Problems in Release 5.03

 

 


 



1                   Introduction

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

2                   Contact Information

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

3                   Changes Introduced at 5.01

3.1              SEPR 1073

The verification condition generator does not word-wrap long type attribute names in the generated VCG file.

4                   Changes Introduced at 5.02

4.1              SEPR 1072, 1075

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.

4.2              SEPR 1081

The Examiner no longer malfunctions when both a superindex and an auxiliary index file are references in a single index file.

5                   Changes Introduced at 5.03

5.1              SEPR 714, 1101

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.

5.2              SEPR 726

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.

5.3              SEPR 889, 1083

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.

5.4              SEPR 1082

Certain malformed Examiner command lines (e.g. spark /i ) where an expected argument was omitted caused the Examiner to terminate with a constraint error.

5.5              SEPR 1085

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.

5.6              SEPR 1090, 1106

Ada 95 attribute ΄Valid is now implemented.

5.7              SEPR 1094

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.

5.8              SEPR 604

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.

5.9              SEPR 1004

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)

5.10          SEPR 1029

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.

5.11          SEPR 1079

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.

5.12          SEPR 1099, 1103

The Examiner index mechanism malfunctioned if an attempt was made to look up children of package Ada.  SEPRs 1099 and 1103 correct this error.

5.13          SEPR 814

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

5.14          SEPR 823

A mal-formed pragma Import (SPARK95) or Interface (SPARK83) does not complete the body of the corresponding subprogram.

5.15          SEPR 830

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.

5.16          SEPR 855

Attributes (such as 'First and 'Last) of constrained subtypes of unconstrained arrays are now allowed by the Examiner.

5.17          SEPR 1054

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.

5.18          SEPR 1065

The “POGS” tool now recognizes and processes the verification conditions produced by the Examiner for the refinment of abstract own variables.

5.19          SEPR 1095

The Examiner now allows global variables of functions to have an explicit “in” mode.

5.20          SEPR 1107, 1110

The SPARK95 attributes 'Min and 'Max are now fully implemented.

5.21          Known Problems in Release 5.03

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.

Changes history

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.

Changes forecast

Nil.