OnWorks favicon

goto-cc - Online in the Cloud

Run goto-cc in OnWorks free hosting provider over Ubuntu Online, Fedora Online, Windows online emulator or MAC OS online emulator

This is the command goto-cc that can be run in the OnWorks free hosting provider using one of our multiple free online workstations such as Ubuntu Online, Fedora Online, Windows online emulator or MAC OS online emulator



cbmc - Bounded Model Checker for C/C++ and Java programs


cbmc [--property property-id] file.c ...

cbmc [--show-properties] file.c ...

cbmc [--all-properties] file.c ...

goto-cc [-I include-path] [-c] file.c [-o outfile.o]

goto-instrument infile outfile

Only the most useful options are listed here; see below for the remainder.


cbmc generates traces that demonstrate how an assertion can be violated, or proves that
the assertion cannot be violated within a given number of loop iterations. CBMC can read
source-code directly, or a goto-binary generated by goto-cc. Java programs are given as
class files. Without any further options, cbmc checks all properties (automatically
generated or user-specified) found in the program. If any of the properties can be
violated, a counterexample is printed and the analysis is aborted. The analysis can be
restricted to a particular property with the --property option. The verification result
for all properties can be obtained by means of the --all-properties option.

goto-cc reads source code, and generates a goto-binary. Its command-line interface is
designed to mimic that of gcc(1). Note in particular that goto-cc distinguishes between
compiling and linking phases, just as gcc does. cbmc expects a goto-binary for which
linking has been completed.

goto-instrument reads a goto-binary, performs a given program transformation, and then
writes the resulting program as goto-binary on disc.

The usual flow is to (1) translate source into a goto-binary using goto-cc, then (2)
perform instrumentation with goto-instrument, and finally (3) perform the analysis with


FRONTEND OPTIONS (cbmc and goto-cc)
-I path
Set include path (C/C++)

-D macro
Define preprocessor macro (C/C++)

Stop after preprocessing

Show symbol table

Show goto program

ARCHITECTURAL OPTIONS (cbmc and goto-cc)
cbmc by default uses architectural settings that match those of the machine cbmc is
executed on, i.e., the settings below are only needed when verifying software that is
meant to run on a different architecture or OS. goto-cc generates a goto-binary for a
particular architecture, i.e., the architecture cannot be changed after the goto-binary is

--16, --32, --64
Set width of int

--LP64, --ILP64, --LLP64, --ILP32, --LP32
Set width of int, long and pointers

Allow little-endian word-byte conversions

Allow big-endian word-byte conversions

Make "char" unsigned by default

--arch Set target architecture

--os Set target operating system

Don't set up an architecture

Disable built-in abstract C library

--round-to-nearest, --round-to-plus-inf, --round-to-minus-inf, --round-to-zero
IEEE floating point rounding mode to use when the program begins (default is round
to nearest). The program under verification can override this setting, e.g., with

PROGRAM INSTRUMENTATION OPTIONS (cbmc and goto-instrument)
Both cbmc and goto-instrument can generate assertions that catch specific common errors,
as listed below.

Enable array bounds checks

Enable division by zero checks

Enable pointer checks

Enable arithmetic over- and underflow checks for signed integer arithmetic

Enable arithmetic over- and underflow checks for unsigned integer arithmetic

Check floating-point computations for NaN

Ignore user-provided assertions

Ignore user-provided assumptions

--error-label label
Check that the given label is unreachable

goto-instrument supports further, more complex, program transformations.

Makes reads from volatile variables non-deterministic

--isr function
Instruments an interrupt service routine with the given name

--mmio Instruments memory-mapped I/O

Variables with static lifetime are initialized non-deterministically

Output ANSI-C source code instead of a goto binary.

Report status of all properties

Only show properties

Show the loops in the program

Check which assertions are reachable

--function name
Set main function name

--property id
Only check specific property with given identifier

Only show program expression

--depth nr
Limit search depth

--unwind nr
Unwind loops nr times

--unwindset L:B,...
Unwind loop L with a bound of B (use --show-loops to get the loop IDs)

Show the verification conditions

Remove assignments unrelated to property

Do not generate unwinding assertions

Do not simplify identifiers

Generate CNF in DIMACS format for use by external SAT solvers

Beautify the counterexample (greedy heuristic)

--smt1 Output subgoals in SMT1 syntax (experimental)

--smt2 Output subgoals in SMT2 syntax (experimental)

Use Boolector (experimental)

Use MathSAT (experimental)

--cvc Use CVC3 (experimental)

Use Yices (experimental)

--z3 Use Z3 (experimental)

Use refinement procedure (experimental)

--outfile filename
Output formula to given file

Never turn arrays into uninterpreted functions

Always turn arrays into uninterpreted functions


All tools honor the TMPDIR environment variable when generating temporary files and
directories. Furthermore note that the preprocessor used by CBMC will use environment
variables to locate header files. GOTO-CC aims to accept all environment variables that
GCC does.


2001-2014, Daniel Kroening, Edmund Clarke

Use goto-cc online using onworks.net services

Free Servers & Workstations

Download Windows & Linux apps

  • 1
    fre:ac - free audio converter
    fre:ac - free audio converter
    fre:ac is a free audio converter and CD
    ripper for various formats and encoders.
    It features MP3, MP4/M4A, WMA, Ogg
    Vorbis, FLAC, AAC, and Bonk format
    support, ...
    Download fre:ac - free audio converter
  • 2
    Matplotlib is a comprehensive library
    for creating static, animated, and
    interactive visualizations in Python.
    Matplotlib makes easy things easy and
    hard thing...
    Download Matplotlib
  • 3
    Write your chatbot logic once and
    connect it to one of the available
    messaging services, including Amazon
    Alexa, Facebook Messenger, Slack,
    Telegram or even yo...
    Download BotMan
  • 4
    Joplin is a free and open source
    note-taking and to-do application that
    can handle a large number of notes in
    Markdown format, organize them into
    notebooks and...
    Download Joplin
  • 5
    gerbv  a Gerber (RS-274X) viewer
    gerbv � a Gerber (RS-274X) viewer
    Gerbv is an open source Gerber file
    (RS-274X only) viewer. Gerbv lets you
    load several files on top of each other,
    do measurements on the displayed image,
    etc. ...
    Download gerbv � a Gerber (RS-274X) viewer
  • 6
    I/O performance Analysis Tool.
    Audience: Developers, Information
    Technology, Science/Research, System
    Administrators. User interface: Win32
    (MS Windows). Progr...
    Download Iometer
  • More »

Linux commands