---
name: "spark"
section: "1"
platform: "linux"
package: "spark"
version: "2012.0.deb-11+b2"
release: "Debian 9 (Stretch)"
platforms: ["linux"]
url: "https://new.carta.tech/spark"
---

# spark(1)

examines SPARK programs and generates verification conditions

## NAME

spark - examines SPARK programs and generates verification conditions

## SYNOPSIS

**spark**  \[OPTIONS\] \[ FILE\_LIST or @METAFILE  \]

## DESCRIPTION

The Examiner for SPARK, **spark**, analyses the given source files for errors and violations of the SPARK subset and (optionally) generates verification conditions and dead path conjectures necessary for proof of absence of run-time exceptions and partial correctness.

This manual page only summarises the **spark** command-line flags, please refer to the full Examiner manual for further information.

## OPTIONS

These options do not quite follow the usual GNU command line syntax. All options start with a single dash instead of the usual two and they can also be abbreviated, as long as the abbreviation is unique. For example FC**-help**F\[0\] can be abbreviated to FC**-he**F\[0\] but not FC**-h**F\[0\] as this clashes with FC**-html**F\[0\].

- FC**-source\_extension=**F\[0\]*file\_type*

  Specifies source file extension (Default 'ada')

- FC**-noindex\_file**F\[0\], FC**-index\_file=**F\[0\]*file\_spec*

  Specifies the index file. By default no index file is used.

- FC**-nowarning\_file**F\[0\], FC**-warning\_file=**F\[0\]*file\_spec*

  Specifies the warning control file. By default no warning control file is used.

- FC**-noconfig\_file**F\[0\], FC**-config\_file=**F\[0\]*file\_spec*

  Specifies the Examiner configuration file. By default no configuration file is used.

- FC**-noswitch**F\[0\]

  Ignore the FCspark.swF\[0\] file, if it exists.

- FC**-nolistings**F\[0\], FC**-listing\_extension=**F\[0\]*file\_type*

  By default all listing files have the 'lst' extension. These options can be used to disable listing file generation or to change the default extension.

- FC**-noreport\_file**F\[0\], FC**-report\_file=**F\[0\]*file\_spec*

  By default the report will be named 'SPARK.REP'. These options can be used to change the default name or to disable report generation.

- FC**-html**F\[0\], FC**-html=**F\[0\]*dir\_spec*

  Generate HTML listings and report file.

- FC**-output\_directory=**F\[0\]*dir\_spec*

  Generate report, listing and proof files in the specified directory.

- FC**-plain\_output**F\[0\]

  No dates, line or error numbers will appear in the output files.

- FC**-language=**F\[0\]*L*

  This can be one of 83, 95 (the default) or 2005.

- FC**-profile=**F\[0\]*P*

  Choose between the sequential (the default) or ravenscar language profile.

- FC**-noduration**F\[0\]

  Do not predefine FCStandard.DurationF\[0\].

- FC**-syntax\_check**F\[0\]

  Perform syntax check only. No semantic checks.

- FC**-flow\_analysis=**F\[0\]*TYPE*

  Choose between FCinformationF\[0\] or FCdataF\[0\].

- FC**-policy=**F\[0\]*TYPE*

  Select FCsecurityF\[0\] or FCsafetyF\[0\] policy for flow analysis.

- FC**-vcg**F\[0\]

  Generate VCs.

- FC**-dpc**F\[0\]

  Generate DPCs.

- FC**-rules=**F\[0\]*CHOICE*

  Select policy for generation of composite constant proof rules. Can be one of none (the default), lazy, keen or all.

- FC**-annotation\_character=**F\[0\]*CHAR*

  Select alternative annotation character. The default is '#'.

- FC**-noecho**F\[0\]

  Suppress screen output.

- FC**-nosli**F\[0\]

  Don't generate SLI files.

- FC**-sparklib**F\[0\]

  Use the standard SPARK library.

- FC**-nostatistics**F\[0\], FC**-statistics**F\[0\]

  Append Examiner table usage statistics to the report file. By default we don't do this.

- FC**-fdl\_identifiers=**F\[0\]*OPTION*

  Control treatment of FDL identifiers when found in SPARK source. Can be one of 'reject' (the default) or 'accept' or \<string\>.

- FC**-version**F\[0\]

  Print Examiner banner and statistics and then exit.

- FC**-help**F\[0\]

  Print command line summary and options.

- FC**-original\_flow\_errors**F\[0\]

  Print information flow errors in original, less compact, format.

- FC**-error\_explanations=**F\[0\]*SETTING*

  Print explanations after error messages. Settings can be off (the default), first\_occurrence or every\_occurrence.

- FC**-justification\_option=**F\[0\]*TYPE*

  Select policy for justification of errors. Values can be full (the default), brief or ignore.

- FC**-casing**F\[0\], FC**-casing=**F\[0\]*CHOICE*

  Check casing for identifier references and check casing of package FCStandardF\[0\] identifiers. It is also possible to specify i or s to check for only one of these.

## SEE ALSO

[sparksimp(1)](/sparksimp/1.md), [spadesimp(1)](/spadesimp/1.md), [zombiescope(1)](/zombiescope/1.md), [victor(1)](/victor/1.md), [pogs(1)](/pogs/1.md)

[sparkformat(1)](/sparkformat/1.md), [sparkmake(1)](/sparkmake/1.md)

## AUTHOR

This manual page was written by Florian Schanda \<FCflorian.schanda@altran-praxis.comF\[0\]\> for the *Debian GNU/Linux* system (but may be used by others). Permission is granted to copy, distribute and/or modify this document under the terms of the GNU Free Documentation License, Version 1.3 or any later version published by the Free Software Foundation; with no Invariant Sections, no Front-Cover Texts and no Back-Cover Texts.