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.

For technical issues on the verifier, see our papers.


FreeSafeTy 0.1 (.tar.gz)


You need GLPK, ocaml-glpk and OMake to install FreeSafeTy. After expanding the downloaded archive, first replace the value of OCAMLGLPKPATH in OMakefile with the path of ocaml-glpk. Then, type omake in the directory. An executable file freesafety will be created.


To verify a program, execute ./freesafety


[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 p and q, and returns the appended list to a reference r

let rec app p q r = 
  if p = null then 
    r := q 
    (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)) 

For more samples, see test directory in the archive.

Command-line options

  --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


Copyright (C) 2008 Naoki Kobayashi and Kohei Suenaga. All rights reserved.