Overview
The interactive engine provides a gdb
-like interface to Mopsa that allows executing an analysis step-by-step, adding breakpoints and inspecting the inferred invariants.
To start an interactive session, use the option -engine interactive
:
$ mopsa-c hello.c -engine=interactive
Welcome to Mopsa 1.0!
Type 'help' to get the list of commands.
mopsa >>
Type help
to display the list of available commands:
mopsa >> h
Available commands:
b[reak] <[file:]line> add a breakpoint at a line
b[reak] <function> add a breakpoint at a function
b[reak] @name add a named breakpoint (will break when the analysis executes an S_break name)
b[reak] #a[larm] break at the next alarm (and go back at the statement generating the alarm
c[ontinue] run until next breakpoint
n[ext] stop at next statement and skip function calls.
n[ext]i stop at next statement and skip nodes in the interpretation sub-tree
s[tep] step into function calls
s[tep]i step into interpretation sub-tree
f[inish] finish current function
b[ack]w[ard] go backward to the calling site
e[nable] h[hook] <h> enable a hook
d[isable] h[hook] <h> disable a hook
s[et] d[ebug] <d> set debug channels
u[nset] d[ebug] unset debug channels
s[et] script <file> store commands into a file
To be used in combination with load script <file>
u[nset] script do not store commands in file anymore
load script <file> reads script command from <file>
help print this message
The commands below support shell commands (`env | grep foo`, `mopsa_bt | tac`, ...):
p[rint] print the abstract state
p[rint] <vars> print the value of selected variables
For example, `p x,y:f,z:*` prints x in the current scope, y in the scope of f, and z in all scopes
p[rint] <vars> #<f>:<l> print the value of selected variables at the given program location
e[nv] print the current abstract environment
e[nv] <domain>,... print the current abstract environment of selected domains
state print the full abstract state (map from flow token to environment)
b[ack]t[race] print the current call stack
t[race] print the analysis trace
w[here] show current program point
i[info] a[larms] print the list of detected alarms
i[info] c[hecks] print the list of performed checks
i[info] b[reakpoints] print the list of registered breakpoints
i[info] t[okens] print the list of flow tokens
i[info] v[ariables] print the list of variables
i[info] c[on]t[e]x[t] print the flow-insensitive context
mopsa_bt shows the current backtrace of the analyzer