Project

General

Profile

Command-Line Options » History » Version 13

Andrei Tatarnikov, 06/19/2015 02:59 PM

1 1 Andrei Tatarnikov
h1. MicroTESK Command-Line Options
2
3 3 Andrei Tatarnikov
_~By Andrei Tatarnikov~_
4
5 2 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.
6
7
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.
8
9
*Options:*
10
11 4 Andrei Tatarnikov
| Full name                   | Short name | Description |
12
| --help                      | -h         | Shows help message |
13
| --verbose                   | -v         | Enables printing diagnostic messages |
14
| --translate                 | -t         | Translates formal specifications |
15
| --generate                  | -g         | Generates test programs |
16
| --include <arg>             | -i         | Sets include files directories [works with --translate] |
17
| --output-dir <arg>          | -od        | Sets where to place generated files [works with --translate] |
18 13 Andrei Tatarnikov
| --extension-dir <arg>       | -ed        | Sets directory that stores user-defined Java code [works with --translate] |
19 4 Andrei Tatarnikov
| --random-seed <arg>         | -rs        | Sets seed for randomizer [works with --generate] |
20
| --solver <arg>              | -s         | Sets constraint solver engine to be used [works with --generate] |
21
| --branch-exec-limit <arg>   | -bel       | Sets the limit on control transfers to detect endless loops [works with --generate] |
22 11 Andrei Tatarnikov
| --solver-debug              | -sd        | Enables debug mode for SMT solvers [works with --generate] |
23
| --tarmac-log                | -tl        |        Saves simulator log in Tarmac format [works with --generate] |
24
| --arch-dirs <arg>           | -ad        | Home directories for tested architectures [works with --generate] |
25 12 Andrei Tatarnikov
| --rate-limit <arg>          | -rl        | Generation rate limit, causes error when broken [works with --generate] |
26 4 Andrei Tatarnikov
| --code-file-extension <arg> | -cfe       | The output file extension [works with --generate] |
27
| --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] |
28
| --data-file-extension <arg> | -dfe       | The data file extension [works with --generate] |
29
| --data-file-prefix <arg>    | -dfp       | The data file prefix [works with --generate] |
30
| --program-length-limit <arg>| -pll       | The maximum number of instructions in output programs [works with --generate] |
31 5 Andrei Tatarnikov
| --trace-length-limit <arg>  | -tll       | The maximum length of execution traces of output programs [works with --generate] |
32 6 Andrei Tatarnikov
| --comments-enabled          | -ce        | Enables printing comments; if not specified no comments are printed [works with --generate] |
33 7 Andrei Tatarnikov
| --comments-debug            | -cd        | Enables printing detailed comments; must be used together with --comments-enabled  [works with --generate] |
34 8 Andrei Tatarnikov
35
*Notes:*
36
37 9 Andrei Tatarnikov
Format of the <code>--arch-dirs</code> option argument is the following: 
38 8 Andrei Tatarnikov
39
<pre><code>--arch-dirs mips=arch/mips:arm=arch/arm:sparc=arch/sparc</code></pre>
40
41 10 Andrei Tatarnikov
# Entries are separated by <code>'':''</code>.
42 8 Andrei Tatarnikov
# Each entry has the following format: <code><architecture-name>=<path-to-the-architecture-directory></code>.
43
# If a path is relative, <code>MICROTESK_HOME</code> is used as a prefix.