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.

For technical issues on the verifier, see our papers.

Download

FreeSafeTy 0.2 (.tar.gz)

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

Among those test programs, *.i files are preprocessed ones, so that can be given as an argument of freesafety command.

Command-line options

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

Papers

Older version

Contact

Any comments, questions and bug reports are welcome.


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