|
|
|
|
|
|
||
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Issue: 1.18 Status: Definitive Issue 1.15, Draft, 15th January 2010
|
|
|
|
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 Altran Praxis Limited.
Limited Warranty
Altran Praxis 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.
Altran Praxis 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 Altran Praxis Limited accepts no liability for any programs or data stored or processed using Altran Praxis Limited products, including the costs of recovering such programs or data.
SPADE is a trademark of Altran Praxis Limited
Note: The SPARK programming language is not sponsored by or affiliated with SPARC International Inc. and is not based on SPARC™ architecture.
Contents
Document Control and References
SPARK is an annotated sub language of Ada, intended for high-integrity programming. The language exists in variants based on Ada83, Ada95 and Ada2005. The SPARK language is described in the following reports:
· “SPARK83 — The SPADE Ada83 Kernel” [1]
· “SPARK — The SPADE Ada Kernel (Including RavenSPARK)” [2]
The Examiner [3] is the tool that is used to examine SPARK files. The SPARKMake tool automatically generates two files that can be used as arguments to the Examiner command line. The two files are:
1 The index file. The index file is described in [3] and associates compilation units with the files that contain them. The index file is used by the Examiner to locate required units that have not been specified on the command line either directly or via a meta file.
2 The meta file. The meta file is described in [3] and is a list of files. When the meta file is presented to the Examiner, the Examiner will examine the files in the order specified in the meta file exactly as if they had been presented individually on the command line.
This document describes how to use SPARKMake.
SPARKMake has two functions.
1 It builds an index file. SPARKMake recursively scans the current directory and any additional directories specified on the command line looking for files that match a regular expression (either the default or one specified on the command line). For each relevant file, the compilation unit is extracted and the association is recorded in the index file.
2 It builds a meta file. SPARKMake generates the closure of files (within the scope of the files recorded in the index file) that are required to examine the root file. If no root file is specified then the meta file will include all files within scope. These files are written to the meta file in the order in which they must be examined. If a package specification is included in the meta file then the corresponding package body (and any children and separates) will also be included if present.
1 Each file must contain exactly one compilation unit.
2 Path names must not contain spaces.
The command line syntax is as follows:
Command-line = “sparkmake” { Command-option } { File-spec }
The command line may include command options as described below. The command line may also have a file specification that identifies the root of the “make”. If no file specification is given then all files are included in the make as described in section 3.3.
The Command-options are given in the following tables. Note that the option names may be abbreviated: the minimum abbreviation is that given in the column specifying the command syntax.
3.2.1 Input Options
Option |
Syntax |
Default |
Multiple instances |
Description |
Directory |
-d=dir-spec |
Current directory |
The union is taken |
SPARKMake will search for units in and under the current directory AND the directories specified by instances of this switch. A relative path may be used here. |
include |
-inc=regexp (see section 3.2.2) |
*\.ad[bs] |
The union is taken |
SPARKMake will search for units in all directories as specified above but will limit its search to files whose full path names match this regular expression. The default equates to all files with extensions .ads and .adb |
exclude |
-e=regexp (see section3.2.2) |
No files are excluded |
The union is taken |
SPARKMake will exclude files (included by the include switch) whose full path names match this expression. |
The regular expression syntax is given below. The matching is case insensitive.
regexp ::= term
term ::= elmt
term ::= elmt elmt ... -- concatenation (elmt then elmt)
term ::= * -- any string of 0 or more characters
term ::= ? -- matches any character
term ::= [char char ...] -- matches any character listed
term ::= [char - char] -- matches any character in given range
elmt ::= nchr -- matches given character
elmt ::= [nchr nchr ...] -- matches any character listed
elmt ::= [^ nchr nchr ...] -- matches any character not listed
elmt ::= [char - char] -- matches chars in given range
elmt ::= . -- matches any single character
elmt ::= ( regexp ) -- parens used for grouping
char ::= any character, including special characters
nchr ::= any character except \()[].*+?^ or \char
Note: That for files with extensions the `.` character must be preceded by the \ character as the `.` character on its own means any single character. For example: -inc=*.ads will include the file “toads” and “to.ads” whereas -inc=*\.ads will only include the latter.
Note: On platforms that use “\” as a directory separator you will have to use “\\” to separate directories. For example: -inc=*\\myproject\\*\.ads will look in and under the directory myproject for file with the .ads or .ADS extension. But note also that Windows now accepts “/” as a directory separator so this form may also be used.
3.2.3 Behaviour Options
Option |
Syntax |
Default |
Multiple instances |
Description |
Duplicates_are_ |
-du |
Not set |
Ignored |
SPARKMake will fail if the directories searched contain any instances of the same unit contained in different files. By default a warning will be given, but SPARKMake will not fail. |
Annotation_ character |
-a |
# |
Not allowed |
If a character other than # has been used in the annotations for the code being examined, then inform SPARKMake using this switch. Must be a single character. |
Language_profile |
-l=83 | |
95 |
Not allowed |
Controls which language profile SPARKMake expects to be used in source files. This affects, for example, the set of predefined reserved words in the language. |
Option |
Syntax |
Default |
Multiple instances |
Description |
Index |
-ind=file-spec |
Root file name with extension .idx, or spark.idx if no root specified |
Not allowed |
Specifies the name of the required index file. If no extension is specified then the default .idx is used. |
Meta |
-m=file-spec |
Root file name with extension .smf, or spark.smf if no root specified |
Not allowed |
Specifies the name of the required meta file. If no extension is specified then the default .smf is used. |
NoIndexFile |
-noi |
False |
Ignored |
SPARKMake will not produce an index file if this option is specified. |
NoMetaFile |
-nom |
False |
Ignored |
SPARKMake will not produce a meta file if this option is specified. |
Path |
-path=full | relative |
Full |
Not allowed |
Selects output of full or relative path-names in output files. |
3.2.5 Help Options
Option |
Syntax |
Default |
Multiple instances |
Description |
Help |
-h |
|
Ignored |
Prints out help information |
Version |
-v |
|
Ignored |
Prints out version information |
Once a help option has been found on the command line, the requested information will be printed out and the rest of the command line ignored.
If exactly one file is specified on the command line then this file is used as the root of the make. The file specified as the root is included by default and does not have to match the -inc option and will not be excluded by the -exc option.
If no file is specified then SPARKMake will search all files in the current directory and its subdirectories (and any other directories specified by the Directory option). The include and exclude switches may be used to control the search as normal. The meta file produced will include all units found, in a suitable order for analysis by the Examiner. If the names of the index and meta files are not specified by command line options then they will default to:
spark.idx
spark.smf
SPARKMake may encounter SPARK source files that are not included in the meta file because it cannot determine an appropriate analysis order for them. Examples include packages with circular dependencies, or package bodies with no corresponding specifications. If this is the case then SPARKMake will output the message:
The following units were not included in the meta file:
followed by a list of filenames.
Examples
1 sparkmake main.adb
This is the most basic form and will consider files in and under the current directory that have extensions .ads and .adb. The index file main.idx and meta file main.smf will be created.
2 sparkmake -dir=../anotherdir main.adb
This command is similar to 1 with the addition that the files in and under ../anotherdir are also considered.
3 sparkmake -inc=*\.[12]\.ada main.2.ada
This command is similar to 1 except that we have overridden the default include switch so that only files ending in .1.ada and .2.ada are considered.
4 sparkmake -exc=*boundary*\.adb main.adb
This command is similar to 1 with the exception that .adb files containing the word boundary are not considered.
5 sparkmake -index=myindex.idx main.adb
This command overrides the default index file and writes to the file myindex.idx
6 sparkmake -index=myindex main.adb
This command overrides the default index file and writes to the file myindex.idx
7 sparkmake -noindex main.adb
This command inhibits index file generation. The default meta file will still be produced.
8 sparkmake -meta=mymeta.smf main.adb
This command overrides the default meta file and writes to the file mymeta.smf
9 sparkmake -meta=mymeta main.adb
This command overrides the default meta file and writes to the file mymeta.smf
10 sparkmake -nometa main.adb
This command inhibits meta file generation. The default index file will still be produced.
11 sparkmake -dir=../anotherdir -dir=onemoredir main.adb
This command is similar to 2. It looks first in the current directory, then in anotherdir directory, then in onemoredir. If any duplicate units are found it takes the first one it finds, and prints a warning to screen for any subsequent occurrences.
12 sparkmake -dir=../anotherdir -dir=onemoredir -duplicates main.adb
This command looks first in the current directory, then in the directories in the order specified. If any duplicate units are found it fails.
13 sparkmake
This command will search for units in all files in and under the current directory that have extensions .ads and .adb. The index file spark.idx and meta file spark.smf will be created. The meta file will list all units in a suitable order for examination.
The following warnings may be output:
>>> Sparkmake warning: File XXX does not contain a valid unit
This warning is reported when SPARKMake finds a file that does not contain a valid compilation unit. If it is meant to be a compilation unit then correct the syntax error. Otherwise restrict the -include switch or widen the -exclude switch to ensure it is not included.
>>> Sparkmake warning: Unit XXX in file YYY is already seen in ZZZ
This warning indicates that the search has located two files, YYY and ZZZ, that both contain the same compilation unit. Ensure that the directories are specified in the correct order so that the correct file is included in your index and meta files. Alternatively, consider restricting the -include switch or using the -exclude switch to exclude one of them, or using the -duplicates_are_errors switch.
>>> Sparkmake warning: Files XXX and YYY both contain main programs.
This warning is reported when SPARKMake encounters more than one file containing a main program (as may occur when no root file is specified). All files containing main units will be included in the meta file but the Examiner will raise an error as it only permits one main program.
The following errors may be output:
!!! Sparkmake error: Unit XXX is duplicated in files YYY and ZZZ
This error indicates that the search has located two files, YYY and ZZZ, that both contain the same compilation unit. Consider restricting the -include switch or using the -exclude switch to exclude one of them, or switch off the -duplicates_are_errors flag.
!!! Sparkmake error: XXX is not a recognised switch
This error indicates that XXX is not a recognised switch. See 3.2 for valid switches.
!!! Sparkmake error: XXX is not a valid argument for switch YYY.
This error indicates that the argument XXX is not valid for switch YYY. For valid switches and arguments see 3.2.
!!! Sparkmake error: The switch XXX cannot be duplicated
This error indicates that the switch has been duplicated. Output switches may not be duplicated.
!!! Sparkmake error: Could not find the file XXX.
This error indicates that the root file could not be found.
!!! Sparkmake error: Cannot open file XXX
This error is reported when file XXX cannot be opened. Try changing the privileges.
!!! Sparkmake error: Cannot close file XXX
This error is reported when file XXX cannot be closed.
Document Control and References
Altran Praxis Limited, 20 Manvers Street, Bath BA1 1PX, UK.
Copyright Altran Praxis Limited 2010. All rights reserved.
svn/userdocs/SPARKMake_UM.doc
Issue 0.1 (20 February 2004) First Draft.
Issue 1.0 (16 June 2004). Issued at Provisional following review.
Issue 1.1 (24 November 2004): Company name changed only.
Issue 1.2 (5 January 2005): Definitive issue following review S.P0468.79.88.
Issue 1.3 (26 July 2005): Updated following addition of /duplicates_are_errors switch.
Issue 1.4 (8 October 2005): Updated following addition of /annotation_character switch.
Issue 1.5 (22nd November 2005): Changed Line Manager.
Issue 1.6 (1st December 2005): Updated following review S.P0468.79.90.
Issue 1.7 (4th January 2006): Updated following addition of /help and /version switches.
Issue 1.8 (7th December 2006): Addition of /path switch.
Issue 1.9 (13th March 2008): Addition of /noindexfile and /nometafile switches. CFR 1864.
Issue 1.10 (26th March 2008): Update for processing all files in a directory. CFR 1869.
Issue 1.11 (26th August 2008): Make manual platform-independent. CFR 1938.
Issue 1.12 (3rd November 2008): Change remaining instance of ‘/’ to ‘-’.
Issue 1.13 (7th January 2009): Factored out contact details.
Issue 1.14 (2nd February 2009): Modify copyright notice.
Issue 1.15 (15th January 2010): Added new language switch [IA16-037].
Issue 1.16 (4th February 2010): Rebrand to Altran Praxis Limited.
Issue 1.17 (1st March 2010): Definitive issue following review.
Issue 1.18 (12th October 2010): Correct references to the Examiner.
Updates as a result of reviews
1 SPARK83 — The SPADE Ada83 Kernel, Altran Praxis
2 SPARK — The SPADE Ada Kernel (Including RavenSPARK), Altran Praxis