Project

General

Profile

Actions
History

Wiki »

Command-Line Options

MicroTESK works in two main modes:

  • model compilation (--translate);
  • test program generation (--generate).

NOTE: The --translate and --generate keys are inserted into the command line by compile.sh (or compile.bat) and generate.sh (or generate.bat) correspondingly.

Other options should be specified explicitly:

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
--tracer-log -tl Enables generation of Tracer logs for simulation --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.

Updated by Alexander Kamkin almost 5 years ago · 24 revisions