Actions
Command-Line Options » History » Revision 8
« Previous |
Revision 8/24
(diff)
| Next »
Andrei Tatarnikov, 06/03/2015 03:28 PM
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] |
| --comments-enabled | -ce | Enables printing comments; if not specified no comments are printed [works with --generate] |
| --comments-debug | -cd | Enables printing detailed comments; must be used together with --comments-enabled [works with --generate] |
| --solver-debug | -sd | Enables debug mode for SMT solvers [works with --generate] |
| --arch-dirs <arg> | -ad | Home directories for tested architectures [works with --generate] |
Notes:
Format of the --arch-dirs option:
--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 Andrei Tatarnikov over 9 years ago · 24 revisions