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.
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
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
To verify a program
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
and then verify the generated file with
more information on how to generate merged file, see CIL homepage.
--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.
The archive comes with several test programs in
directory. That directory includes
Among those test programs,
*.i files are preprocessed
ones, so that can be given as an argument of
--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
Any comments, questions and bug reports are welcome.