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")
