Skip to content

Usage

Jump to bottom
Daniel Dietsch edited this page Dec 13, 2023 · 12 revisions

Build and Usage

Please note that Ultimate and its associated tools are continuously evolving as part of ongoing research. Consequently, (a) they may contain bugs, and (b) the user interfaces may be quite unfriendly. If your purpose is to explore and experiment with our diverse tools, we recommend using our web interface.

For those seeking a relatively recent version of Ultimate, we suggest checking out the latest release.

If you specifically require building Ultimate from source, please follow the instructions provided here.

Feel free to reach out with any questions by opening an issue or sending an email 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.

Ultimate ships with binaries of several SMT solvers. To make sure that they can be used successfully, make sure that the directory releasescripts/default/adds is on your PATH when running Ultimate.

Build Prerequisites

  • Java JDK (11) - 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 components.

  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. For example,

    • Procedure Inlining, Large Block Encoding, Automizer, Witness Printer
    • Automata Script interpreter and a graphical visualization of its output After selecting the source button, a dialog appears that asks you to compose your toolchain from existing plugins. We recommend that you do not compose a toolchain by yourself but press the "XML Toolchain" button and use 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