PVS Sun WorkShop Pascal 4.2

Pascal Validation Summary Report Sun WorkShop Pascal 4.2

The Pascal Version 4.2 compiler has been validated using Version 5.5 of the Pascal Validation Suite. It complies with FIPS PUB 109 ANSI/IEEE 770 X3.97-1983 and BS6192/ISO7185 at both level 0 and level 1. This appendix is a summary of the validation.

Test Conditions

The Pascal Version 4.2 compiler was validated under the Solaris 2.5 operating system on a SPARCstationTM 10 machine.
The following compiler options were used during each validation:

  • Level 1 mode
  • All checks
  • Runtime trace
  • All other default options

The following manufacturer’s statement of compliance is included in the Validation Summary Report for the architecture.

Manufacturer’s Statement of Compliance

The above processor complies with the requirements of both level 0 and level 1 (by means of a compiler switch) of BS 6192/ISO 7185, with no exceptions.

Implementation-Defined Features

The implementation-defined features are as follows:

E.1 The value of each char-type corresponding to each allowed string-character is the corresponding ISO 8859/1 (ASCII) character.
E.2 The subset of real numbers denoted by signed-real are the values representable in the single precision (32-bit) format of the IEC559:1982 Standard Binary Floating Point Arithmetic for Microprocessor Systems, which is the same format as in the IEEE standard P754.
E.3 The values of char-type are the ISO 8859/1 (ASCII) character set.
E.4 The ordinal numbers of each value of char-type are the corresponding ISO 8859/1 (ASCII) code value.
E.5 All file operations are performed at the point where they are encountered at execution time, with the exception of get (both explicit and where implied by reset and read), which is delayed in its execution to the point at which the file is next referenced–a technique known as “lazy I/O.”
E.6 The value of maxint is 2,147,483,647.
E.7 The accuracy of the approximations of the real operations and functions is determined by the representation (see E.2) and by the rounding of intermediate results. This gives approximately 16-decimal digits of precision.
E.8 The default value of TotalWidth for integer-type is 10.
E.9 The default value of TotalWidth for real-type is 21.
E.10 The default value of TotalWidth for boolean-type is 5.
E.11 The value of ExpDigits is 2.
E.12 The exponent character is e.
E.13 The case in the output of the value of boolean-type is uppercase for the initial letter, and lowercase for the remaining letters.
E.14 The procedure Page causes the contents of the output buffer (if any) to be written, and then outputs the ISO 8859/1 (ASCII) form-feed character. The effect on any device depends on that device.
E.15 There is no binding between physical files and program parameters of file-type. Variables of file-type are associated with physical files or devices automatically by the processor.
E.16 The effects of reset and rewrite on the standard files input and output depend on the binding of these files specified at the invocation of the program. In general, reset and rewrite have the effects described in clause 6.6.5.2 of the Pascal Standard1 when input and output have been bound to permanent files. When the binding is to a device, reset(input) has no effect other than discarding any partially processed line. rewrite(output) terminates any partially complete line but has no other effect. rewrite(input) and reset(output) are treated as errors.
E.17 This implementation supports the alternative representation of symbols permitted by the Standard.

Reporting of Errors

The following errors are detected prior to, or during, execution of a program:

D.1, D.3, D.7, D.9, D.10, D.11, D.14, D.15, D.16, D.17, D.18, D.23, D.26, D.29, D.33, D.34, D.35, D.36, D.37, D.40, D.41, D.42, D.45, D.46, D.47, D.49, D.51, D.52, D.53, D.54, D.55, D.56, D.57, D.58, D.59

The following errors are not, in general, reported:

D.2, D.4, D.5, D.6, D.8, D.12, D.13, D.19, D.20, D.21, D.22, D.24, D.25, D.27, D.28, D.30, D.31, D.32, D.38, D.39, D.43, D.44, D.48, D.50

Implementation-Dependent Features

Implementation-dependent features F.1 to F.11 of Pascal are treated as undetected errors.

Extensions

The processor does not contain any extensions to BS6192/ISO 7185. Such extensions must be enabled by means of a compiling option, not the subject of validation.

The American National Standard Pascal Computer Programming Language, ANSI/IEE 770 X3.97-1983, published by the Institute of Electrical and Electronics Engineers, Inc., 345 East 47th Street, New York,
NY 10017, c. 1983.