• The public website (local)
• The blog
• Dev tools :
  • old BTS
  • new BTS
  • kernel metrics(make metrics)
  • browse SVN
  • dev mailing list
  • Gforge Frama-C page
• User manual
  • The user manual : pdf version (cd userman; make)
  • French version of value (cd value; make)
• ACSL: ANSI C Specification Language
  • Reference manual (cd speclang; make) (.pdf),
  • Implemented features (cd speclang; make) (.pdf),
  • Tutorial (cd speclang; make acsl-mini-tutorial.pdf) (.pdf),
• Software Architecture (pdf) (cd architecture; make)
• Plugin Development Guide (pdf) (cd developer; make) (local pdf version)
• Source Documentation (make doc for the whole documentation or make html for generating only the kernel documentation)
• Dependencies Graph (.ps, .dot, or .svg) (make dots)
• Some plugins:
  • occurrence (doc web)
  • metrics
  • syntactic_callgraph
  • value (doc web)
  • rte
  • from
  • inout
  • users
  • constant_propagation (doc web)
  • semantic_callgraph
  • impact (doc web)
  • pdg (rapport cd pdg; make)
  • scope (rapport cd scope; make) (doc web)
  • sparecode (doc web)
  • slicing (rapport cd slicing; make) (doc web)
  • mthread
  • security_slicing
  • wp (WHY library) (spec : cd wp/Spec; make) (informal notes : cd wp/Notes; make) (implementation : cd wp/Implem; make) (modélisation COQ) (metrics : make Wp_metrics))
  • cxx
  • Jessie
  • aorai (pdf manual) (doc web)
• Other links and documentations:
  • Techniques for the Verification of Real-World C Programs
  • Wikipedia(en)
  • Correct sorting with Frama-C : an online presentation of a proof of a bubbleSort function.