|
|
|
|
|
|
||
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Issue: 3.5 Status: Definitive
DOCTYPE:Praxis title:varchar=title reference:varchar=reference status:varchar=status issue:varchar=issue date:varchar=date projectname:varchar=DocumentSet Issue 3.5, Definitive, 2ed February 2009 073_060 Supplementary Release Note — The OptFlow Option
|
|
|
|
Originator |
|
|
|
SPARK Team |
|
|
|
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 PraxisHigh 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 registered 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.
2 Data Flow Analysis of SPARK 83 Programs
Document Control and References
Contents
SPARK 95 introduced mode, or data flow direction, indications on global annotations. Where global modes are present, information flow analysis may optionally be suppressed and the SPARK 95 Examiner used just to perform a data flow analysis. Derives annotations are not required for simple data flow analysis in SPARK 95.
It is not possible to perform a similar data flow analysis on SPARK 83 programs because of differences between the Ada 83 and Ada 95 rules concerning the permitted use of subprogram parameters.
A facility to perform just data flow analysis can be provided for SPARK 83 programs by special arrangement; this document describes that facility.
2 Data Flow Analysis of SPARK 83 Programs
The facility to perform data flow analysis of SPARK 83 programs, without also performing information flow analysis, is enabled by the SPARK Examiner feature “OptFlow” in the FLEXlm licence file. If this feature is present, the command line option “flow=data” becomes available in the SPARK 83 as well as SPARK 95 modes of operation.
In SPARK 83, derives annotations remain mandatory even if information flow analysis is not being carried out. (Since Release 4.0 of the Examiner, global modes are permitted in SPARK 83 programs but they are checked only for consistency with the mandatory derives annotation and are not otherwise used). Data flow analysis of SPARK 83 programs, instead, relies on interpreting the derives annotation in a simplified way. Instead of reading the annotation as a true set of dependencies between imports and exports the Examiner uses it to determine only the direction of data flow. For example:
--# derives A from X, Y, Z &
--# B from B, X;
would, for data flow analysis purposes, signify only that A is only exported; B is both imported and exported; and X, Y and Z are only imported.
With this information, the Examiner:
· can check for compliance with SPARK language rules;
· check that all data items are set before any use is made of them; and
· can be used to generate VCs and Run-time Checks (but not Path Functions).
Information flow checks are not carried out and all messages associated with them are suppressed; however, any semantic and flow error messages that are produced remain valid.
The data flow option is primarily intended for use in situations where full derives annotations may be difficult to maintain and where the value of information flow analysis is considered to be limited. Typically this situation may occur near the “top” of a SPARK program, for example in a scheduler or main subprogram. Here all the visible system data will depend, in some rather complex way, on itself requiring a possibly lengthy description.
It is essential to show that there are no data flow errors at this level but information flow analysis may be considered less important. To carry out data flow analysis, a simplified derives annotation can be provided for the subprograms concerned; this would not attempt to define the complete flow relation but just show all exports to be derived from all imports. The earlier example would simplify to:
--# derives A, B from B, X, Y, Z;
which has the same meaning as the earlier one for data flow analysis purposes.
SPARK 83 data flow analysis is a fully-defined process with an exact meaning; however, it relies on the interpretation of derives annotations in a particular way which may be misleading to human readers of the SPARK source code. For example, a reader of the simplified annotation above might be misled into thinking that the initial value of B was expected to influence the final of value of A which the earlier, full, annotation clearly shows not to be the case.
Furthermore, since the Examiner cannot fully check a derives annotations which has been used only for data flow analysis, care must be taken not to attempt information flow analysis of other subprograms which may rely upon it. Information flow analysis of a subprogram is only complete if all subprograms it calls have also been subject to information flow analysis.
The listing files of code analysed with the data flow option will indicate that derives annotations have been interpreted in the simplified way described above and will also indicate that information flow analysis has not been carried out.
It is possible to perform just a data flow analysis of SPARK 83 program by simplifying the mandatory derives annotations and using them only as an indication of data flow direction rather than as a full description of information flow dependencies. This facility may simplify data flow analysis in some circumstances where fully-descriptive derives annotations might be difficult to provide.
If this facility is used, care should be taken that human readers of the source code are not misled by the simplified annotations used.
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.
$CVSROOT/userdocs/Examiner_SRN_OptFlow.doc (was P0468.73.60).
Issue 0.1 (16/3/99): First draft
Issue 1.0 (17/3/99): After formal review
Issue 2.0 (20/3/03): Updated to new template format
Issue 3.0 (5/6/03): Changes to new template, final format
Issue 3.1 (10/6/2003): Minor updates for Release 7.0 following review.
Issue 3.2 (23/11/2004): Company name change only.
Issue 3.3 (22/11/2005): Line Manager change.
Issue 3.4 (29/11/05) Updated following review S.P0468.79.90.
Issue 3.5 (2nd February 2009): Modify copyright notice.
Nil.
None.