Spa (simple program analyzer) is a simple (and naive) static analysis tool. It has been developed to support a course on abstract interpretation. The focus is on simplicity and modularity, at the expense of efficiency. Build requirements -------------------------------------------------------------------------------- - OCaml 4.01 or later http://caml.inria.fr/ocaml/ - Menhir http://gallium.inria.fr/~fpottier/menhir/ - GNU make http://www.gnu.org/software/make/ Build instructions -------------------------------------------------------------------------------- Simply run `make' to build the tool. This generates a byte-code executable with debugging information (spa.d.byte). You may also build a faster native-code executable (with assertions and bound checking disabled) with `make spa.native'. The makefile has two additional useful targets. The `doc' target generates the documentation. The `test' target builds an executable that performs unit tests (runtests.d.byte) and then runs it. Input format -------------------------------------------------------------------------------- The tool analyzes automata-based programs (also called program automata). These are finite-state automata equipped with integer variables, and whose transitions are labeled by commands. Commands are either assignments (e.g., x := y+z), or guards (e.g., x < 3*y), or the no-op instruction skip. Some examples are available in the examples sub-directory. Tool invocation -------------------------------------------------------------------------------- The tool reads the input program automaton from the standard input or from the specified input file (if any). Then, it performs either a forward analysis from the initial location, or a backward analysis from the final location. The `-help' option displays the available options.