Project

General

Profile

Command-Line Options » History » Revision 13

Revision 12 (Andrei Tatarnikov, 06/15/2015 04:26 PM) → Revision 13/24 (Andrei Tatarnikov, 06/19/2015 02:59 PM)

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:* 

 | 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] | 
 | --extension-dir <arg>         | -ed          | Sets directory that stores user-defined Java code [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] | 
 | --solver-debug                | -sd          | Enables debug mode for SMT solvers [works with --generate] | 
 | --tarmac-log                  | -tl          |          Saves simulator log in Tarmac format [works with --generate] | 
 | --arch-dirs <arg>             | -ad          | Home directories for tested architectures [works with --generate] | 
 | --rate-limit <arg>            | -rl          | Generation rate limit, causes error when broken [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] | 

 *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.