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

A run of Ultimate is defined by three components.

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

  2. The toolchain. For example,

    • CACSL2BoogieTranslator, ProcedureInliner, RCFGBuilder, TraceAbstraction, WitnessPrinter
    • AutomataScriptInterpreter, GUI

    Toolchains are usually defined in XML files. If you use a release version, you can find the most important examples in the config/ directory. Our repository contains many more examples in trunk/examples/toolchains.

  3. The preferences. These are either defined by an .epf file or within the respective user interface.

Command line interface

Ultimate can be used from the command line. For this, you need to have a Java JRE 11 installed and either your PATH contains the folder where the Ultimate binary resides or this folder is your working directory. The most important options are

$ ./Ultimate --help
usage: Ultimate [OPTIONS] -tc <FILE> -i <FILE> [<FILE> ...]
-tc,--toolchain <FILE>
      Specify the path to an Ultimate toolchain file. Depending on the
      toolchain, you may have more options.
-i,--input <FILE>
-s,--settings <FILE>
-h,--help
--version
--experimental
      Also show experimental options (even if they do not have a description).
# ...

If you provide a toolchain and an input file, you get additional options available for this combination by using the --help option. For example, ./Ultimate -tc config/AutomizerReach.xml -s config/svcomp-Reach-64bit-Automizer_Bitvector.epf --help provides you with many different options, e.g., for the C to Boogie translation:

# ...
--cacsl2boogietranslator.check.unreachability.of.reach_error.function <arg>
      Check if every call to reach_error is unreachable. This is used for the ReachSafety category
      of SV-COMP. Note: If a function reach_error is defined, it is automatically overridden. This
      option can either be true or false. The default value is true.
--cacsl2boogietranslator.entry.function <arg>
      Specify the entry function of the program. Use an empty string for library mode (i.e.,
      assume all globals are non-deterministic and verify each function in isolation). <arg> is a
      single line of text. The default value is main.
--cacsl2boogietranslator.check.assertions.from.assert.h <arg>
      Check if the assertions from assert.h (currently supported: assert, static_assert,
      _Static_assert, __assert_fail, __assert_func) never fail. This option can either be true or
      false. The default value is false.
--cacsl2boogietranslator.sv-comp.memtrack.compatibility.mode <arg>
      Report UNKNOWN instead of UNSAFE if not all allocated memory was freed at the end of the
      main procedure. Rationale: at the SV-COMP we have to check if the program lost track of
      allocated memory. If this is set to false we are unsound (at SV-COMP) in cases where not all
      memory is freed but pointers to that memory are live at the end of the main procedure. This
      option can either be true or false. The default value is false.
--cacsl2boogietranslator.overapproximate.operations.on.floating.types <arg>
      Overapproximate all operations on floats (including plus, minus, multiplication,
      conversions, etc.) by havoc. The resulting analysis will be fast and sound, but the result
      is UNKNOWN if such an operation occurs in a counterexample. This option can either be true
      or false. The default value is false.
--cacsl2boogietranslator.let.fesetround.change.the.rounding.mode <arg>
      If enabled, fesetround can change the current rounding mode. If disabled, fesetround does
      nothing and always returns non-zero (no success). This option can either be true or false.
      The default value is true.
--cacsl2boogietranslator.initial.rounding.mode <arg>
      Use the specified rounding mode as initial float rounding mode. <arg> is a pre-defined
      value. Valid choices for <arg> are "FE_DOWNWARD", "FE_TONEAREST", "FE_TOWARDZERO",
      "FE_UPWARD". The default value is FE_TONEAREST.
--cacsl2boogietranslator.use.constant.arrays <arg>
      Use SMT constant arrays for default initialization of variables. This option can either be
      true or false. The default value is false.
--cacsl2boogietranslator.use.store.chains <arg>
      Only for benchmarking -- do not use This option can either be true or false. The default
      value is false.
--cacsl2boogietranslator.adapt.memory.model.on.pointer.casts.if.necessary <arg>
      When a pointer to a value with a small type (e.g. char) is cast to a larger pointer type
      (e.g. int*), and the memory model resolution is larger than the values's pointed to type
      size (for char: 1 Byte), the memory model is unsound. When this setting is on we attempt to
      detect this case, and automatically set the memory model to a higher resolution. This option
      can either be true or false. The default value is false.
--cacsl2boogietranslator.string.overapproximation.threshold <arg>
      String literals that require this number of bytes or more are overapproximated, i.e.,
      Ultimate assumes that the string can contain arbitrary bytes. <arg> is a string representing
      an integer. The default value is 9.
# ...

If you use --help --experimental you get even more options.

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.

  • You can configure your preferences by either using the dialogs in "Settings > Preferences", or by pressing the "Load settings" button and select a .epf file from the config/ or trunk/examples/settings folder.
  • You select the input files by pressing the "Open Source" button.
  • 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 config/ or from the trunk/examples/toolchains 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