Actions
Command-Line Options » History » Revision 2
« Previous |
Revision 2/24
(diff)
| Next »
Andrei Tatarnikov, 05/23/2015 09:38 AM
MicroTESK Command-Line Options¶
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 |
| --output-dir <arg> | -d | Sets where to place generated files [works with -t] |
| --generate | -g | Generates test programs |
| --help | -h | Shows this message |
| --include <arg> | -i | Sets include files directories [works with -t] |
| --branch-exec-limit <arg> | -l | Sets the limit on control transfers to detect endless loops [works with -g] |
| --random-seed <arg> | -r | Sets seed for randomizer [works with -g] |
| --solver <arg> | -s | Sets constraint solver engine to be used [works with -g] |
| --translate | -t | Translates formal specifications |
| --verbose | -v | Enables printing diagnostic messages |
Updated by Andrei Tatarnikov over 9 years ago · 24 revisions