Toy implementation of a separation logic based program analysis
Switch branches/tags
Nothing to show
Clone or download
Fetching latest commit…
Cannot retrieve the latest commit at this time.
Permalink
Failed to load latest commit information.
docs/.svn
my_examples
test
LICENCE
Makefile
OcamlMakefile
README
TODO
analysis.ml
config.ml
error.ml
genlinenum.ml
gensym.ml
global.ml
heapstuff.ml
heapstuffold.ml
lexer.mll
main.ml
parser.mly
parsetree.ml
symbexec.ml
trans.ml
utils.ml

README

Toy implementation of a separation logic based static analysis tool. 

See my_examples for syntax of program files and precondition file names.

Usage: 

mini-invader -f <file-name> -p <precondition-file-name>