MicroTESK Command-Line Options

By Andrei Tatarnikov

MicroTESK works in two modes: specification translation and test generation, which are enabled with the --translate (used by default) and --generate keys correspondingly. In addition, the --help key prints information on the command-line format.

The --translate and --generate keys are inserted into the command-line by compile.sh/compile.bat and generate.sh/generate.bat scripts correspondingly. Other options should be specified explicitly to customize the behavior of MicroTESK.

Options:

Full name Short name Description Requires
--help -h Shows help message
--verbose -v Enables printing diagnostic messages
--translate -t Translates formal specifications
--generate -g Generates test programs
--output-dir <arg> -od Sets where to place generated files
--include <arg> -i Sets include files directories --translate
--extension-dir <arg> -ed Sets directory that stores user-defined Java code --translate
--random-seed <arg> -rs Sets seed for randomizer --generate
--solver <arg> -s Sets constraint solver engine to be used --generate
--branch-exec-limit <arg> -bel Sets the limit on control transfers to detect endless loops --generate
--solver-debug -sd Enables debug mode for SMT solvers --generate
--tarmac-log -tl Saves simulator log in Tarmac format --generate
--self-checks -sc Inserts self-checking code into test programs --generate
--arch-dirs <arg> -ad Home directories for tested architectures --generate
--rate-limit <arg> -rl Generation rate limit, causes error when broken --generate
--code-file-extension <arg> -cfe The output file extension --generate
--code-file-prefix <arg> -cfp The output file prefix (file names are as follows prefix_xxxx.ext, where xxxx is a 4-digit decimal number) --generate
--data-file-extension <arg> -dfe The data file extension --generate
--data-file-prefix <arg> -dfp The data file prefix --generate
--exception-file-prefix <arg> -efp The exception handler file prefix --generate
--program-length-limit <arg> -pll The maximum number of instructions in output programs --generate
--trace-length-limit <arg> -tll The maximum length of execution traces of output programs --generate
--comments-enabled -ce Enables printing comments; if not specified no comments are printed --generate
--comments-debug -cd Enables printing detailed comments; must be used together with --comments-enabled --generate

Notes:

Format of the --arch-dirs option argument is the following:

--arch-dirs mips=arch/mips:arm=arch/arm:sparc=arch/sparc
  1. Entries are separated by ':'.
  2. Each entry has the following format: <architecture-name>=<path-to-the-architecture-directory>.
  3. If a path is relative, MICROTESK_HOME is used as a prefix.