Search GODI:
FREE SOFTWARE ON CAMLCITY.ORG
Modular C static analyser
Frama-C stands for FRAmework for Modular Analysis of C. It provides a generic framework (based on the CIL library) for building static analyzers for C programs. It features an annotation language, called ACSL, in which it is possible possible to express the formal properties that the code under analysis is expected to meet. Current analyzers include: - an abstract interpreter - WP-based verifiers - a code slicer - an impact analysis tool
| Version: | 20080701 |
| Homepage: | http://frama-c.cea.fr/ |
| Maintainer: | Virgile Prevosto <virgile.prevosto@m4x.org> |
| Files: |
bin/frama-c bin/frama-c-gui bin/frama-c.byte share/frama-c/builtin.c share/frama-c/builtin.h share/frama-c/fluctuat.h share/frama-c/jessie/prolog.c share/frama-c/jessie/prolog.h share/frama-c/libc.c share/frama-c/libc.h share/frama-c/machine.h share/frama-c/malloc.c share/frama-c/manuals/acsl-implementation.pdf share/frama-c/manuals/frama-c-architecture.pdf share/frama-c/manuals/frama-c-manual-en.pdf share/frama-c/manuals/frama-c-manual.pdf share/frama-c/manuals/plugin-dev.pdf share/frama-c/math.c share/frama-c/math.h share/frama-c/why/hoare.why share/frama-c/why/low-level.why share/frama-c/why/test.why |
| Built from sources: |
frama-c-Helium-20080701 |
