Command-Line Options » History » Revision 20
« Previous |
Revision 20/24
(diff)
| Next »
Alexander Kamkin, 04/05/2017 11:35 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 | 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- Entries are separated by
'':''. - Each entry has the following format:
<architecture-name>=<path-to-the-architecture-directory>. - If a path is relative,
MICROTESK_HOMEis used as a prefix.
Updated by Alexander Kamkin over 7 years ago · 24 revisions