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)