source: CIVL/doc/manual/part-tools.tex@ 924c81b

\part{Tools}
\label{part:tools}

\chapter{Introduction}

\section{Symbolic execution}

\section{Tool overview}

Current tools allow one to \emph{run} a CIVL program using random
choice to resolve nondeterministic choices; \emph{verify} a program
using model checking to explore all states of the program;
\emph{replay} a trace if an error is found.

The properties checked are assertion violations, division by zero,
illegal pointer accesses, etc.

The available tools and options are summarized by the \texttt{civl
  help} command:

\begin{verbatim}
Usage: civl <command> <options> filename ...
Commands:
  verify : verify program filename
  run : run program filename
  help : print this message
  replay : replay trace for program filename
  parse : show result of preprocessing and parsing filename
  preprocess : show result of preprocessing filename
Options:
  -debug or -debug=BOOLEAN (default: false)
    debug mode: print very detailed information
  -echo or -echo=BOOLEAN (default: false)
    print the command line
  -errorBound=INTEGER (default: 1)
    stop after finding this many errors
  -guided or -guided=BOOLEAN
    user guided simulation; applies only to run, ignored
    for all other commands
  -id=INTEGER (default: 0)
    ID number of trace to replay
  -inputKEY=VALUE
    initialize input variable KEY to VALUE
  -maxdepth=INTEGER (default: 2147483647)
    bound on search depth
  -min or -min=BOOLEAN (default: false)
    search for minimal counterexample
  -por=STRING (default: std)
    partial order reduction (por) choices:
    std (standard por) or scp (scoped por)
  -random or -random=BOOLEAN
    select enabled transitions randomly; default for run,
    ignored for all other commands
  -saveStates or -saveStates=BOOLEAN (default: true)
    save states during depth-first search
  -seed=STRING
    set the random seed; applies only to run
  -showModel or -showModel=BOOLEAN (default: false)
    print the model
  -showProverQueries or -showProverQueries=BOOLEAN (default: false)
    print theorem prover queries only
  -showQueries or -showQueries=BOOLEAN (default: false)
    print all queries
  -showSavedStates or -showSavedStates=BOOLEAN (default: false)
    print saved states only
  -showStates or -showStates=BOOLEAN (default: false)
    print all states
  -showTransitions or -showTransitions=BOOLEAN (default: false)
    print transitions
  -simplify or -simplify=BOOLEAN (default: true)
    simplify states?
  -solve or -solve=BOOLEAN (default: false)
    try to solve for concrete counterexample
  -states=STRING (default: immutable)
    state implementation: immutable, transient, persistent
  -sysIncludePath=STRING
    set the system include path
  -trace=STRING
    filename of trace to replay
  -userIncludePath=STRING
    set the user include path
  -verbose or -verbose=BOOLEAN (default: false)
    verbose mode
\end{verbatim}

\chapter{Running a CIVL-C program}

\chapter{Model Checking}

\chapter{Replaying counter-examples}

\chapter{C/MPI Programs}


\chapter{Transitions}
In CIVL, a transition stands for the execution of a number of statements of a certain process from one state, and the execution of each statement is considered as one step. A transition has the following form in the output, where sid and sid' are the identifiers for the source and the target states, pid is the identifier of the process that this transition belongs to, and step 0,1 ... are the steps contained in the transitions.

\begin{verbatim}
State sid, proc pid: 
  step 0;
  step 1;
  ...
--> State sid'
\end{verbatim}

A step of a transition has the following form in the CIVL output, where src and dst is the source and destination location of the statement executed in the step, file is the file that contains the source code of the statement, location and text are the location and summary of text of the statement in the source file.

\begin{verbatim}
  src->dst: statement at file:location "text";
\end{verbatim}

For example, the following is a transition from state 0 to state 1, containing 6 steps. File names are renamed with short names and the mapping of short names and the original files is presented in output as well.

\begin{verbatim}
File name list:
f0      : atomicBlockedResume.cvl

State 0, proc 0: 
  0->1: x = 1 at f0:3.0-9 "int x = 1";
  1->2: y = 0 at f0:4.0-9 "int y = 0";
  2->3: z = 0 at f0:5.0-9 "int z = 0";
  3->6: sum = 0 at f0:6.0-11 "int sum = 0";
  6->8: $spawn foo(1) at f0:22.4-17 "$spawn foo(1)";
  8->10: $spawn foo(2) at f0:23.4-17 "$spawn foo(2)";
--> State 1
\end{verbatim}

To make use of this feature, one needs to specify the option ``-showTransitions'' when running CIVL.