FreeSafeTy

FreeSafeTy (Free is made Safe by Types) is a type-based memory usage verifier for C programs. FreeSafeTy can verify the following properties on memory usage.

• Lack of memory leak.
• Lack of double free.
• Lack of read/write to deallocated memory cell.

Download

Install

You need GLPK, ocaml-glpk and OMake to install FreeSafeTy. After expanding the downloaded archive, first add the path to glpk and ocaml-glpk to OCAMLFLAGS variable in allsrc/OMakefile. Then, type omake . An executable file freesafety will be created.

FreeSafeTy is distributed with CIL. In order to use cilly as a replacement of other C compiler (e.g., GCC). You need to manually configure $cilhome variable in CilConfig.pm.

Usage

To verify a program test.c, execute ./freesafety test.c. In the current implementation, it is not possible to verify each file in a project separately and then merge the result of each file. In order to verify a program which consists of several files, first generate a merged file using cilly --merge and then verify the generated file with freesafety. For more information on how to generate merged file, see CIL homepage.

If --outputLinearProg is specified and --noMinimize is not specified, and if a passed program is ill-typed, then the verifier produces a minimal subset of generated linear inequalites to "output.cplex" and a figurative description of those inequalities to "output.dot". You can view the file "output.dot" with dotty in Graphviz.

Sample

The archive comes with several test programs in test/small1/ directory. That directory includes

• a program that manipulates several data structures (e.g., linked lists, binary trees and doubly-linked list).
• preprocessed Linux device drivers.(Though contained in a directory named *small*, those device drivers are pretty large :-)

  --fstdebug                        dump debugging info
  --measureTime                     measure time consumption of each phase
  --noMinimize                      do not minimize unsatisfiable inequalities
  --displaySolution                 display a solution of linear inequalities
  --outputLinearProg                output linear inequalities
  --noSCC                           do not perform SCC optimization in constraint reduction
  --noZeroOne                       do not perform zero-one optimization in constraint reduction
  --printInferredTypes              print inferred types.
  --dumpIntermFile                  dumps intermediate files
  -help                             Display this list of options
  --help                            Display this list of options