xenial (1) sparksimp.1.gz

NAME

       sparksimp - analyses all generated SPARK proof artifacts (in parallel)

SYNOPSIS

       sparksimp [OPTIONS] [-sargs SIMPLIFIER_OPTIONS] [-zargs ZOMBIESCOPE_OPTIONS] [-vargs VICTOR_OPTIONS]

DESCRIPTION

       sparksimp,  analyses  all verification conditions and dead path conjectures generated by the Examiner for
       SPARK and attempts to discharge them using the Simplifier, ZombieScope and ViCToR. If requested, this can
       be done in parallel.

       This  manual  page  only  summarises the sparksimp command-line flags, please refer to the full SPARKSimp
       manual for further information.

OPTIONS

       These options do not quite follow the usual GNU command line syntax as options start with a  single  dash
       instead of the usual two.

       -a     Processes all files, even if their time-stamp indicated that they have been previously analysed.

       -v     Displays version information.

       -V     Verbose output.

       -n     Dry run — this prints only the list of files to analyse and then stops.

       -ns    Do not run the Simplifier.

       -nz    Do not run ZombieScope.

       -victor
              Run  ViCToR/Alt-Ergo  on  VCs left unproven by Simplifier.  If -ns is specified then this will run
              ViCToR on all VCs.

       -t, -r Sort vcg file by size and analyse the largest ones first. If -r is specified as well  analyse  the
              smallest ones first.

       -l     Log spadesimp and zombiescope output for each unit analysed to UNIT.log and UNIT.zsl respectively.

       -e     Echo all output to the screen; this option cannot be used in conjunction with -p.

       -p=N   Use N concurrent processes.

       -x=PATH
              Specifies an alternative Simplifier executable.

       -z=PATH
              Specifies an alternative ZombieScope executable.

       -sargs OPTIONS, -zargs OPTIONS, -vargs OPTIONS
              Any  options  following  one of these will be passed to directly to the Simplifier, ZombieScope or
              ViCToR respectively. Please see their manual pages or documentation for more information.

SEE ALSO

       spark(1), spadesimp(1), zombiescope(1), victor(1), pogs(1)

       sparkformat(1), sparkmake(1)

AUTHOR

       This manual page was written  by  Florian  Schanda  <florian.schanda@altran-praxis.com>  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.

                                                  22 March 2011                                     sparksimp(1)