Skip to content

Usage

Jump to bottom
alexandernutz edited this page Apr 22, 2019 · 12 revisions

Build and Usage

Please be aware that Ultimate and the associated tools are all ongoing research, and thus (a) may contain bugs, and (b) have quite unfriendly user interfaces. If you only want to play around with our various tools, we recommend you visit our web interface.

If you only want to use a fairly recent Ultimate version, you should first try the latest release.

If you really need to build Ultimate, use the instructions here.

If you have any questions, do not hesitate and open an issue or write a mail to one of the tool authors.

Building Ultimate

Ultimate can be build on Windows and Linux with the same build process. MacOS should work, but has currently no build support. If you really need a macOS version, contact Daniel.

Note that for most purposes, you also need binaries of CVC4, Mathsat and Z3 in your path.

Build Prerequisites

  • Java JDK (1.8) - note: Java JRE is not sufficient
  • Maven (>3.0)
  • A bash shell (Windows 10 provides one with WSL/LXSS, but you can also use Cygwin)
  • zip (for creation of zip archives to work, not necessary for build itself)

Build

  • Checkout Ultimate to ultimate/
  • cd ultimate/releaseScripts/default
  • ./makeFresh.sh

Now you can find *.zip files and folders for the main Ultimate tools (in their Linux and Windows version) in the current folder.

Usage

Commandline

Instructions coming soon

Developer GUI

Ultimate has a graphical user interface which can be used by Ultimate developers. For users we recommend the command line interface or the web interface.

In Eclipse this developer GUI is called Debug-E4.product. Please follow the Download and Installation in order to start it.

A run of Ultimate is defined by three "things".

  1. The actual input file(s) which can be e.g.,

    You select the input files by pressing the "Open Source" button.

  2. The toolchain. E.g.,

    • Procedure Inlining, Large Block Encoding, Automizer, Witness Printer
    • Automata Script interpreter and a graphical visualization of its output After selecting the source button the you get a dialog that asks you to compose your toolchain from existing plugins. We recommand that you do not compose a toolchain by yourself but press the "XML Toolchain" button and take one of the toolchains from the trunk/examples/toolchains folder.

  3. The preferences. In "Settings > Preferences" you can configure each plugin. Alternatively you can load a preference file by pressing the "Load settings" button and select a .epf file from the trunk/examples/settings folder.

DeltaDebugger CLI

The DeltaDebugger interface for Ultimate allows you to reduce a C input file such that Ultimate exhibits the same behavior on the reduced file. This is useful for tracking down some errors in Ultimate and produce minimal examples.

  1. We assume that you built Ultimate and use Linux as platform.
  2. After executing ./makeFresh.sh, switch to the directory DeltaDebugger-linux.
  3. Hint: We provide a small wrapper script, run-ultimate.sh, to launch Ultimate without using Ultimate.ini and the Ultimate binary.
    • cp ../adds/run-ultimate.sh .
    • You can modify this script to, e.g., change the memory usage.
  4. Executing the DeltaDebugger is similar to the normal command line interface:
    ./run-ultimate.sh -tc <toolchainfile> -s <settingsfile> -i <inputfile>
    If you are interested in debugging C translation errors, consider using the CheckedCTranslation.xml toolchain (syntax checker, c translation, boogie preprocessor).
    You should also pipe the output to a file (./run-ultimate.sh ... > reduced.log) s.t. you can extract the reduced program with this command:
    sed -n -e '/------------------------------------/,$p' reduced-log.log | awk '!x[$0]++'

Additionally, you may want to use one of the following command line switches:

  • --deltadebugger.look.for.result.of.type <arg>
    Specify the name of a type that represents an Ultimate result (i.e., some class implementing IResult with this name). The delta debugger searchs for the presence of this result.
    Valid choices for <arg> are "ExceptionOrErrorResult", "SyntaxErrorResult", "UnsupportedSyntaxResult", "TypeErrorResult", "CounterExampleResult", "AllSpecificationsHoldResult", "SyntaxCheckerSyntaxErrorResult".
    The default value is "ExceptionOrErrorResult".
  • --deltadebugger.result.short.description.prefix <arg>
    The provided string must be the prefix of the short description of one of the results that are interesting. Use the empty string if all results of this type are interesting.
    The default value is "".
  • --deltadebugger.result.long.description.prefix <arg>
    The provided string must be the prefix of the long description (normally written in the second line) of one of the results that are interesting. Use the empty string if all results of this type are interesting.
    The default value is "".
  • --deltadebugger.ignore.reduction.with.results.of.type <arg>
    If a reduction produces a result of this type, the delta debugger assumes that this reduction is not interesting.
    Valid choices for <arg> are "ExceptionOrErrorResult", "SyntaxErrorResult", "UnsupportedSyntaxResult", "TypeErrorResult", "CounterExampleResult", "AllSpecificationsHoldResult", "SyntaxCheckerSyntaxErrorResult".
    The default value is "".
  • --core.toolchain.timeout.in.seconds <arg>
    Specify the time in seconds after which Ultimate will terminate due to a timeout. The value has to be larger or equal to 0. A value of 0 disables the timeout.
    The default value is 0.
Clone this wiki locally