FreeSafeTy (Free is made Safe by Types) is a type-based verifier for safe memory deallocation. FreeSafeTy can verify the following properties on memory usage.
You need GLPK, ocaml-glpk and OMake to install
FreeSafeTy. After expanding the downloaded archive, first replace the
OMakefile with the
path of ocaml-glpk. Then, type
omake in the
directory. An executable file
freesafety will be created.
To verify a program
[program] ::= let rec [fundefs] in [stmt] | [stmt] [fundefs] ::= [fundef] | [fundef] and [fundefs] [fundef] ::= f x1 x2 ... xn = [stmt] [stmt] ::= skip (do nothing) | x := y (assign y to x) | free x (deallocate x) | [stmt];[stmt] (sequential execution) | let x = null in [stmt] (bind x to null) | let x = y in [stmt] (bind x to y) | let x = !y in [stmt] (bind x to the content of y) | let x = malloc() in [stmt] (allocate a size 2 cell and bind x to it) | let x = y + 1 in [stmt] (pointer arithmetics) | if x = null then [stmt] else [stmt] (branch with x = null) | if * then [stmt] else [stmt] (nondeterministic branch) | f x1 x2 ... xn (function call) | assert(x = y) (asserts x = y, used to pass obligations/capabilities between x and y) | assert(x = !y) (asserts x = !y, obligations/capabilities are passed between x and !y) | assert(x = y + 1) (asserts x = y + 1, obligations/capabilities are passed between x and y + 1)
The following program appends two linked lists
and returns the appended list to a reference
let rec app p q r = if p = null then r := q else (r := p; (let nextp = p + 1 in let next = !nextp in app next q nextp; assert(next = !nextp); assert(nextp = p + 1)); assert(p = !r)) in skip
For more samples, see
test directory in the archive.
--debugGenConstr dump behaviour of constraint generating function --noMinimize do not minimize unsatisfiable inequalities --displaySolution display a solution of linear inequalities --outputLinearProg output linear inequalities -help Display this list of options --help Display this list of options