Project

General

Profile

Actions

Command-Line Options » History » Revision 4

« Previous | Revision 4/24 (diff) | Next »
Andrei Tatarnikov, 05/28/2015 11:43 AM


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
--help -h Shows help message
--verbose -v Enables printing diagnostic messages
--translate -t Translates formal specifications
--generate -g Generates test programs
--include <arg> -i Sets include files directories [works with --translate]
--output-dir <arg> -od Sets where to place generated files [works with --translate]
--random-seed <arg> -rs Sets seed for randomizer [works with --generate]
--solver <arg> -s Sets constraint solver engine to be used [works with --generate]
--branch-exec-limit <arg> -bel Sets the limit on control transfers to detect endless loops [works with --generate]
--code-file-extension <arg> -cfe The output file extension [works with --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) [works with --generate]
--data-file-extension <arg> -dfe The data file extension [works with --generate]
--data-file-prefix <arg> -dfp The data file prefix [works with --generate]
--program-length-limit <arg> -pll The maximum number of instructions in output programs [works with --generate]
--trace-length-limit <arg> -tll The maximum length of execution traces of output programs [works with --generate]

Updated by Andrei Tatarnikov almost 9 years ago · 4 revisions