SPARK

SPARKMake

 

 

 

 

 

 

 

 

 

 

 

SPARKMake

Issue: 1.18

Status: Definitive

12th October 2010

 

DOCTYPE:Praxis title:varchar=title reference:varchar=reference status:varchar=status issue:varchar=issue date:varchar=date projectname:varchar=DocumentSet

Issue 1.15, Draft, 15th January 2010

000_000 SPARKMake

 

 

 

Originator

 

 

SPARK Team

 

 

 

Approver

 

 

SPARK Team Line Manager

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 



Copyright

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

1          Overview

2          General description

2.1      Limitations

3          Using SPARKMake

3.1      Syntax

3.2      Command-options

3.3      Root File Specification

3.4      Error messages

Document Control and References

File under

Changes history

Changes forecast

Document references

 

 

 


1                       Overview

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.

2                       General description

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.

2.1               Limitations

1         Each file must contain exactly one compilation unit.

2         Path names must not contain spaces.

3                       Using SPARKMake

3.1               Syntax

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               Command-options

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.

3.2.2           Regular expressions

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

-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 | 2005

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.

3.2.4           Output File Options

 

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.

3.3               Root File Specification

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.

3.4               Error messages

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.

File under

svn/userdocs/SPARKMake_UM.doc

Changes history

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.

Changes forecast

Updates as a result of reviews

Document references

1               SPARK83 — The SPADE Ada83 Kernel, Altran Praxis

2               SPARK — The SPADE Ada Kernel (Including RavenSPARK), Altran Praxis

3               Examiner User Manual, Altran Praxis