Invoking ConcurInterprocContents

Invoking ConcurInterproc

The executable (concurinterproc or concurinterproc.opt is invoked as follows:

  concurinterproc <options> <inputfile>

The input file should be a valid "Simple" program. The options are:

-debug <int>
debug level, from 0 (lowest) to 4 (highest). Default is 0.
-dot <filename>
activate DOT output onthe given file (depends on -debug option)
-margin <int>
right margin to use for display
-domain {box|polka|polkastrict|polkaeq|ppl|pplstrict|pplgrid|polkagrid}
abstract domain to use (default: polka). All domains supported by the Apron library can be specified:

box intervals
polka,ppl topologically closed convex polyhedra
polkastrict,pplstrict possibly non-closed convex polyhedra
polkaeq linear equalities
pplgrid linear congruences
polkagrid reduced product of linear congruences and Polka convex polyhedra

-cooperative <bool>
cooperative scheduling ? (default: false)
-compress <bool>
compress CFG ? (default: true)
-depth <int>
depth of recursive iterations (default 2, may only be more). See Fixpoint library documentation.
-guided <bool>
if true, guided analysis of Gopand and Reps (default: false). See Fixpoint
-widening <bool><int><int><int>
specifies usage of widening first heuristics, delay, frequency of widening, and nb. of descending steps (default: false 1 1 2). See Fixpoint
-display <('text'|'color'|'html)>
display style (default: color)
-thread <string>
project analysis results on the given thread
-print_auxvar <bool>
keep in analysis results frozen variables introduced by the method (default: true)
-print_conc <bool>
keep in analysis results variables and control points from other threads (default: true)
-analysis <('f'|'b')+>
sequence of forward and backward analyses to perform (default "f")

Invoking ConcurInterprocContents