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