Login or Register to Ask a Question and Join Our Community

Linux and UNIX Man Pages

Linux & Unix Commands - Search Man Pages

spadesimp(1) [debian 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)

Check Out this Related Man Page

GRMIC(1)								GNU								  GRMIC(1)

NAME

       grmic - Generate stubs for Remote Method Invocation

SYNOPSIS

       grmic [OPTION] ... class ...

DESCRIPTION

       grmic is a utility included with "libgcj" which generates stubs for remote objects.

       Note that this program isn't yet fully compatible with the JDK grmic.  Some options, such as -classpath, are recognized but currently
       ignored.  We have left these options undocumented for now.

       Long options can also be given with a GNU-style leading --.  For instance, --help is accepted.

OPTIONS

       -keep
       -keepgenerated
	   By default, grmic deletes intermediate files.  Either of these options causes it not to delete such files.

       -v1.1
	   Cause grmic to create stubs and skeletons for the 1.1 protocol version.

       -vcompat
	   Cause grmic to create stubs and skeletons compatible with both the 1.1 and 1.2 protocol versions.  This is the default.

       -v1.2
	   Cause grmic to create stubs and skeletons for the 1.2 protocol version.

       -nocompile
	   Don't compile the generated files.

       -verbose
	   Print information about what grmic is doing.

       -d directory
	   Put output files in directory.  By default the files are put in the current working directory.

       -help
	   Print a help message, then exit.

       -version
	   Print version information, then exit.

SEE ALSO

COPYRIGHT

       Copyright (c) 2001, 2002, 2003, 2004, 2005, 2006, 2007, 2008 Free Software Foundation, Inc.

       Permission is granted to copy, distribute and/or modify this document under the terms of the GNU Free Documentation License, Version 1.2 or
       any later version published by the Free Software Foundation; with no Invariant Sections, the Front-Cover Texts being (a) (see below), and
       with the Back-Cover Texts being (b) (see below).  A copy of the license is included in the man page gfdl(7).

       (a) The FSF's Front-Cover Text is:

	    A GNU Manual

       (b) The FSF's Back-Cover Text is:

	    You have freedom to copy and modify this GNU Manual, like GNU
	    software.  Copies published by the Free Software Foundation raise
	    funds for GNU development.

gcc-4.5 							    2010-07-05								  GRMIC(1)
Man Page