Login or Register to Ask a Question and Join Our Community

Linux and UNIX Man Pages

Linux & Unix Commands - Search Man Pages

sparksimp(1) [debian man page]

sparksimp(1)															      sparksimp(1)

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,  Ver-
       sion 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)

Check Out this Related Man Page

spadesimp(1)															      spadesimp(1)

NAME

       spadesimp - simplifies SPARK verification conditions

SYNOPSIS

       spadesimp [OPTIONS] [UNIT]

DESCRIPTION

       The  Simplifier	for  SPARK, spadesimp, analyses verification conditions generated by the Examiner for SPARK and attempts to discharge them
       automatically. For each vcg file read, the Simplifier will produce a siv (simplified vcs) file and an optional slg (simplifier log) file.

       This manual page only summarises the spadesimp command-line flags, please refer to the full Simplifier 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.

       -help  Displays command line help.

       -version
	      Displays version information.

       -nolog Do not generate a simplification log file.

       -log=file_spec
	      Specify filename for the simplification log file.

       -nowrap
	      Do not line wrap output files.

       -verbose
	      Display attempted simplification strategies.

       -nouserrules
	      Do not use user rules.

       -plain Adopt a plain output style (e.g. no dates or version numbers).

       -typecheck
	      Only typecheck the input files.

       -norenum
	      Do not renumber hypotheses and conclusions in siv files.

       -nosimplification=RANGES, -nostandardisation=RANGES,  -norule_substitution=RANGES,  -nocontradiction_hunt=RANGES,  -nosubstitution_elimina-
       tion=RANGES, -noexpression_reduction=RANGES
	      Adjust  strategy for different VCs. RANGES can be a comma separated list of ranges. Each range can be either a single VC number or a
	      simple range of the form VC-VC.

       -complexity_limit=LIMIT
	      (Limit in range 10 .. 200)

       -depth_limit=LIMIT
	      (Limit in range 1 .. 10)

       -inference_limit=LIMIT
	      (Limit in range 10 .. 400)

SEE ALSO

       spark(1), sparksimp(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, Ver-
       sion 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						      spadesimp(1)
Man Page