|
|
|
|
|
|
SPARK SPARKMake |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
SPARKMake Issue: 1.14 Status: Definitive 2nd February 2009
DOCTYPE:Praxis title:varchar=title reference:varchar=reference status:varchar=status issue:varchar=issue date:varchar=date projectname:varchar=DocumentSet Issue 1.14, Definitive,
2nd February 2009 000_000 SPARKMake
|
|
|
|
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.
The
software tools referred to in this manual are the subject of copyright and all
rights in them are reserved. The rights in these tools are owned by Praxis High
Integrity Systems Limited, and it may not be copied, in whole or in part,
without the written consent of this company, except for reasonable back-up
purposes. The same proprietary and copyright notices must be affixed to any
permitted copies as were affixed to the original. This exception does not allow
copies to be made for others, whether or not sold, and none of the material
purchased may be sold, given or loaned to another person or organisation. Under
law copying includes translating into another language or format.
©1991-20098 Praxis
High Integrity Systems Limited, 20 Manvers St, Bath BA1 1PX
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 Praxis High 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 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.
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 both Ada
83 and Ada 95. The SPARK 83
language is described in three reports:
· “SPARK — The SPADE Ada Kernel” [1]
· “SPARK 95 — The SPADE Ada 95 Kernel (Excluding RavenSPARK)” [2]
· “SPARK 95 — The SPADE Ada 95 Kernel (Including RavenSPARK)” [3]
The SPARK Examiner [4] 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 SPARK Examiner command line. The two files are:
1 The index file. The index file is described in [4] 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 [4] 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.
Advice on the contents of this document may be
obtained:
by phone +44
(0)1225 823829
by FAX +44
(0)1225 469006
by emailsparkinfo@praxis-his.com
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 packagespecification is included in the metafile 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 mayust
also have a file specification exactly one argumentthat
identifiesspecifies
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 |
|
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 |
|
*\.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 |
|
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_errors |
|
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 |
|
# |
Not allowed |
If a
character other than # has been used in the annotations for the code being
examined, then inform SPARKM Must be a single character. |
Option |
Syntax |
Default |
Multiple instances |
Description |
Index |
|
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 |
|
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 |
- |
False |
Ignored |
SPARKMake will not produce an index file if this option is specified. |
NoMetaFile |
- |
False |
Ignored |
SPARKMake will not produce a meta file if this option is specified. |
Path |
- |
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 |
|
|
Ignored |
Prints out help information |
Version |
|
|
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.
3.3
Root File
SpecificationArgument
If SPARKMake takes exactly
one argument
which specifiesfile is specified on the
command line then this which file is isto be 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 willsearch 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 producedwill 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: You must specify a root file
This error indicates that no
root file has been specified on the command line
!!! 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
Praxis High Integrity Systems Limited, 20 Manvers Street, Bath BA1 1PX, UK.
Copyright Praxis High Integrity Systems
Limited 20098. All rights reserved.
S.P0468.73.80
$CVSROOT/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.
Updates as a result of reviews
1 SPARK — The SPADE Ada Kernel, Praxis High Integrity Systems
2 SPARK 95 — The SPADE Ada 95 Kernel (Excluding RavenSPARK), Praxis High Integrity Systems
3 SPARK 95 — The SPADE Ada 95 Kernel (Including RavenSPARK), Praxis High Integrity Systems