Project

General

Profile

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 almost 9 years ago · 2 revisions