Command-Line Options » History » Revision 4
Revision 3 (Andrei Tatarnikov, 05/23/2015 09:40 AM) → Revision 4/24 (Andrei Tatarnikov, 05/28/2015 11:43 AM)
h1. 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 --output-dir <arg> | -h -d | Shows help message Sets where to place generated files [works with -t] | | --verbose --generate | -v -g | Enables printing diagnostic messages Generates test programs | | --translate --help | -t -h | Translates formal specifications Shows this message | | --generate | -g | Generates test programs | | --include <arg> | -i | Sets include files directories [works with --translate] -t] | | --output-dir --branch-exec-limit <arg> | -od -l | Sets where the limit on control transfers to place generated files detect endless loops [works with --translate] -g] | | --random-seed <arg> | -r | -rs | Sets seed for randomizer [works with --generate] -g] | | --solver <arg> | -s | Sets constraint solver engine to be used [works with --generate] -g] | | --branch-exec-limit <arg> --translate | -bel -t | Sets the limit on control transfers to detect endless loops [works with --generate] Translates formal specifications | | --code-file-extension <arg> --verbose | -cfe -v | 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] Enables printing diagnostic messages |