Command-Line Options » History » Revision 18
Revision 17 (Andrei Tatarnikov, 08/05/2015 03:59 PM) → Revision 18/24 (Alexander Kamkin, 04/05/2017 11:22 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:*
table=.
{font-style:italic; font-weight:bold; background:#ddd}.
| 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 <code>--arch-dirs</code> option argument is the following:
<pre><code>--arch-dirs mips=arch/mips:arm=arch/arm:sparc=arch/sparc</code></pre>
# Entries are separated by <code>'':''</code>.
# Each entry has the following format: <code><architecture-name>=<path-to-the-architecture-directory></code>.
# If a path is relative, <code>MICROTESK_HOME</code> is used as a prefix.