Skip to content
Snippets Groups Projects
Select Git revision
  • master default protected
  • stable/zinc
  • 2699-wp-region-plugin-division-by-0-with-empty-region-node
  • stable/copper
  • stable/nickel
  • stable/cobalt
  • stable/iron
  • stable/manganese
  • stable/chromium
  • stable/vanadium
  • stable/titanium-backport
  • stable/titanium
  • stable/scandium
  • 30.0 protected
  • 30.0-beta protected
  • MIEL-2024-10 protected
  • 29.0 protected
  • 29.0-beta protected
  • 28.1 protected
  • 28.0 protected
  • MIEL-2023-10 protected
  • 28.0-beta protected
  • 27.1 protected
  • 27.0 protected
  • 27.0-beta protected
  • 26.1 protected
  • 26.0 protected
  • 26.0-beta protected
  • 25.0-r1 protected
  • pre-dune protected
  • 25.0 protected
  • 25.0-beta protected
  • 2022-03-23 protected
33 results
Compare
user avatar
Squashed commit of the following:
Titouan BOUETE-GIRAUD authored 
commit be323fb0
Merge: bb446348 931dd76e
Author: Loïc Correnson <loic.correnson@cea.fr>
Date:   Mon Nov 6 10:29:29 2023 +0000

    Merge branch 'feature/tests/framework' into 'master'

    E2E and Monkey Tests Framework

    See merge request frama-c/frama-c!4274

commit 931dd76e
Author: Damien IRIBERRY <damien.iriberry@artal.fr>
Date:   Mon Nov 6 10:29:28 2023 +0000

    E2E and Monkey Tests Framework

commit bb446348
Merge: d14e46bf edaa7275
Author: Virgile Prevosto <virgile.prevosto@m4x.org>
Date:   Mon Nov 6 11:13:12 2023 +0100

    Merge branch 'stable/nickel'

commit edaa7275
Merge: 3bf6baa2 89c591e1
Author: Virgile Prevosto <virgile.prevosto@cea.fr>
Date:   Mon Nov 6 10:06:17 2023 +0000

    Merge branch 'rma-master-patch-17294' into 'stable/nickel'

    Update acknowledgement for Roma Maliach-Auguste

    See merge request frama-c/frama-c!4392

commit 89c591e1
Author: Roma Maliach-Auguste <romain.maliach-auguste@cea.fr>
Date:   Fri Nov 3 19:39:10 2023 +0000

    Update acknowledgement for Roma Maliach-Auguste

commit d14e46bf
Merge: 81563c24 eee031c7
Author: Allan Blanchard <allan.blanchard@cea.fr>
Date:   Mon Nov 6 07:19:00 2023 +0000

    Merge branch 'feature/martin/tests/replace-dir-coverage-script-with-option' into 'master'

    Remove compute dir coverage script and use --tree for bisect html report instead

    See merge request frama-c/frama-c!4391

commit eee031c7
Author: Thibault Martin <thi.martin.pro@pm.me>
Date:   Tue Oct 31 16:33:38 2023 +0100

    Remove script and use --tree for bisect html report

commit 81563c24
Merge: 4f6897b4 0eaacb25
Author: Allan Blanchard <allan.blanchard@cea.fr>
Date:   Mon Oct 30 13:37:19 2023 +0000

    Merge branch 'bugfix/julien/userman-foreword' into 'master'

    [e-acsl] fix userman's foreword

    See merge request frama-c/frama-c!4385

commit 4f6897b4
Merge: 7ced1ed8 141d24d4
Author: Allan Blanchard <allan.blanchard@cea.fr>
Date:   Mon Oct 30 12:11:11 2023 +0000

    Merge branch 'feature/blanchard/ci/simpl-constrains' into 'master'

    [ci] reorganizes schedules and release pipelines

    See merge request frama-c/frama-c!4390

commit 141d24d4
Author: Allan Blanchard <allan.blanchard@cea.fr>
Date:   Fri Jun 16 17:13:31 2023 +0200

    [ci] reorganizes schedules and release pipelines

commit 7ced1ed8
Merge: 25fb48d3 d26fe9df
Author: Thibault Martin <thi.martin.pro@pm.me>
Date:   Fri Oct 27 13:22:22 2023 +0000

    Merge branch 'feature/eva/simplify-widen-hints' into 'master'

    [Eva] Changes the signature of the widening in most cvalue modules

    See merge request frama-c/frama-c!4384

commit 25fb48d3
Merge: 9ac7e685 4b3f48e5
Author: Allan Blanchard <allan.blanchard@cea.fr>
Date:   Fri Oct 27 11:49:16 2023 +0000

    Merge branch 'feature/dev/make-distrib-help' into 'master'

    [dev] make-distrib options

    See merge request frama-c/frama-c!4373

commit 3bf6baa2
Author: David Bühler <david.buhler@cea.fr>
Date:   Fri Oct 27 13:34:56 2023 +0200

    Updates Changelog for MR !4259.

commit d26fe9df
Author: David Bühler <david.buhler@cea.fr>
Date:   Thu Oct 26 10:19:41 2023 +0200

    [Eva] Offsetmap and lmap: [widen] takes hints as optional named arguments.

commit d3a404d1
Author: David Bühler <david.buhler@cea.fr>
Date:   Wed Oct 25 19:30:04 2023 +0200

    [Eva] Fval: uses sets of float as widen_hint instead of logic_real.

    Removes module Fc_float.Widen_hint, and uses Datatype.Float.Set instead.

commit 793cb8a9
Author: David Bühler <david.buhler@cea.fr>
Date:   Wed Oct 25 17:58:29 2023 +0200

    [Eva] Computes widening thresholds according to bases validity in Locations.

commit b0b5ce92
Author: David Bühler <david.buhler@cea.fr>
Date:   Wed Oct 25 16:08:49 2023 +0200

    [Eva] Changes the signature of the widening in most cvalue modules.

    - In int_interval, int_val, ival, locations and cvalue: [widen] now takes
      optional named arguments [size] and [hint].
    - Updates Offsetmap functor accordingly.
    - Removes types [numerical_widen_hint] and [size_widen_hint]:
      modules only declare one [widen_hint] type.
    - Removes module Ival.Widen_hints, and uses Integer.Set directly instead.

commit 57de6adf
Author: David Bühler <david.buhler@cea.fr>
Date:   Wed Oct 25 16:14:12 2023 +0200

    [Eva] Uses Integer.Set instead of Ival.Widen_Hints in widen files.

commit 16a111a5
Author: David Bühler <david.buhler@cea.fr>
Date:   Wed Oct 25 16:00:55 2023 +0200

    [Eva] Removes widening from lattice types.

commit 9ac7e685
Merge: ce374b15 c12f874e
Author: Andre Maroneze <andre.maroneze@cea.fr>
Date:   Thu Oct 26 19:31:52 2023 +0000

    Merge branch 'merge-stable-nickel' into 'master'

    merge stable/nickel into master and update VERSION

    See merge request frama-c/frama-c!4382

commit c12f874e
Author: Andre Maroneze <andre.maroneze@cea.fr>
Date:   Thu Oct 26 20:56:58 2023 +0200

    update version for dev branch

commit 009f9602
Merge: ce374b15 22713a7c
Author: Andre Maroneze <andre.maroneze@cea.fr>
Date:   Thu Oct 26 20:54:59 2023 +0200

    Merge stable/nickel into master

commit 22713a7c
Author: Andre Maroneze <andre.maroneze@cea.fr>
Date:   Thu Oct 26 16:02:33 2023 +0200

    [release] add main changes for 28.0

commit 0eaacb25
Author: Allan Blanchard <allan.blanchard@cea.fr>
Date:   Thu Oct 26 15:49:23 2023 +0200

    [e-acsl/doc] on clean, remove eacslversion

commit ce374b15
Merge: 101a5fb8 d2126607
Author: Thibault Martin <thi.martin.pro@pm.me>
Date:   Thu Oct 26 13:27:13 2023 +0000

    Merge branch 'feature/blanchard/ci/manuals' into 'master'

    [ci] improved manuals target

    Closes #1323

    See merge request frama-c/frama-c!4383

commit 758ba4a5
Author: Allan Blanchard <allan.blanchard@cea.fr>
Date:   Thu Oct 26 15:21:40 2023 +0200

    [e-acsl/doc] fix Frama-C version

commit 021b2939
Author: Julien Signoles <julien.signoles@cea.fr>
Date:   Thu Oct 26 15:02:16 2023 +0200

    [e-acsl] fix userman's foreword

commit 078bff52
Author: Allan Blanchard <allan.blanchard@cea.fr>
Date:   Thu Oct 26 15:21:40 2023 +0200

    [e-acsl/doc] fix Frama-C version

commit 2e448107
Author: Julien Signoles <julien.signoles@cea.fr>
Date:   Thu Oct 26 15:02:16 2023 +0200

    [e-acsl] fix userman's foreword

commit 858647e8
Author: Andre Maroneze <andre.maroneze@cea.fr>
Date:   Thu Oct 26 14:56:33 2023 +0200

    [doc] fix typos in a few manuals

commit 9ad4f685
Merge: 1beda363 9d9faf75
Author: Andre Maroneze <andre.maroneze@cea.fr>
Date:   Thu Oct 26 07:39:55 2023 +0000

    Merge branch 'prepare-release-update-version' into 'stable/nickel'

    Prepare release update version

    See merge request frama-c/frama-c!4381

commit d2126607
Author: Allan Blanchard <allan.blanchard@cea.fr>
Date:   Thu Oct 26 09:34:42 2023 +0200

    [ci] improved manuals target
    - executed nightly (allowed to fail)
    - excuted on changes

commit 9d9faf75
Author: Andre Maroneze <andre.maroneze@cea.fr>
Date:   Thu Oct 26 09:06:25 2023 +0200

    [dev] fix usage of 'dev' after a beta release

commit 3e889241
Author: Andre Maroneze <andre.maroneze@cea.fr>
Date:   Wed Oct 25 22:51:09 2023 +0200

    update copyright year in forgotten files

commit 0aaf54b1
Author: Andre Maroneze <andre.maroneze@cea.fr>
Date:   Wed Oct 25 22:43:18 2023 +0200

    update version for 28.0~beta

commit 1e4612c5
Author: Andre Maroneze <andre.maroneze@cea.fr>
Date:   Wed Oct 25 16:11:17 2023 +0200

    [dev] extend set-version.sh and update release manual

commit 101a5fb8
Merge: 7129e55b 7afe0cc2
Author: Thibault Martin <thi.martin.pro@pm.me>
Date:   Wed Oct 25 15:44:19 2023 +0000

    Merge branch 'feature/eva/clean-abstract-interp' into 'master'

    [Eva] Removes unused code from Abstract_interp

    See merge request frama-c/frama-c!4379

commit 7afe0cc2
Author: David Bühler <david.buhler@cea.fr>
Date:   Wed Oct 25 15:08:16 2023 +0200

    [Eva] Removes unused module [Bool] from Abstract_interp.

commit 8467dbcb
Author: David Bühler <david.buhler@cea.fr>
Date:   Wed Oct 25 14:19:01 2023 +0200

    [Eva] Removes unused functors from abstract_interp.

commit 1305bbfb
Author: David Bühler <david.buhler@cea.fr>
Date:   Wed Oct 25 14:53:42 2023 +0200

    [Eva] Garbled mix origin: removes use of Abstract_interp.Make_Lattice_Base.

    Defines datatype and lattice of LocationLattice in origin.ml.

commit 21641125
Author: Andre Maroneze <andre.maroneze@cea.fr>
Date:   Wed Oct 25 16:00:28 2023 +0200

    [doc] avoid references to specific Frama-C versions

commit 1beda363
Merge: b0770ad3 4bf59c78
Author: Andre Maroneze <andre.maroneze@cea.fr>
Date:   Wed Oct 25 13:18:01 2023 +0000

    Merge branch 'fix/blanchard/dev/set-version-update' into 'stable/nickel'

    [dev] extend set-version.sh for build script

    See merge request frama-c/frama-c!4366

commit 7129e55b
Author: Andre Maroneze <andre.maroneze@cea.fr>
Date:   Wed Oct 25 08:31:25 2023 +0000

    Reset default branch

commit b0770ad3
Author: Andre Maroneze <andre.maroneze@cea.fr>
Date:   Wed Oct 25 08:31:25 2023 +0000

    Change default branch

commit 5049d6b9
Author: Andre Maroneze <andre.maroneze@cea.fr>
Date:   Wed Oct 25 08:27:09 2023 +0000

    Reset default branch

commit 91cba9d8
Author: Andre Maroneze <andre.maroneze@cea.fr>
Date:   Wed Oct 25 08:27:08 2023 +0000

    Change default branch

commit 66662ebd
Merge: 2670b181 ce91403b
Author: Allan Blanchard <allan.blanchard@cea.fr>
Date:   Wed Oct 25 06:55:19 2023 +0000

    Merge branch 'fix/wp/strategies' into 'master'

    [wp] fix non-terminating strategies

    See merge request frama-c/frama-c!4376

commit 2670b181
Merge: 2fe33b18 3ec37752
Author: Loïc Correnson <loic.correnson@cea.fr>
Date:   Tue Oct 24 19:05:03 2023 +0000

    Merge branch 'jan/fix/issue2666' into 'master'

    [alias] correctly expose Abstract_state including graph

    See merge request frama-c/frama-c!4375

commit 3ec37752
Author: Loïc Correnson <loic.correnson@cea.fr>
Date:   Tue Oct 24 20:31:06 2023 +0200

    [alias] expose vertex id as int

commit ce91403b
Author: Loïc Correnson <loic.correnson@cea.fr>
Date:   Mon Oct 23 17:53:17 2023 +0200

    [wp] test for logical patterns

commit 0b07515d
Author: Loïc Correnson <loic.correnson@cea.fr>
Date:   Mon Oct 23 17:42:08 2023 +0200

    [wp] logical patterns

commit 2fe33b18
Merge: a1c78b46 a4fc83c5
Author: Allan Blanchard <allan.blanchard@cea.fr>
Date:   Mon Oct 23 15:06:25 2023 +0000

    Merge branch 'fix/macOS-args' into 'master'

    [ivette] Fix/mac os args

    See merge request frama-c/frama-c!4368

commit 078669fa
Author: Loïc Correnson <loic.correnson@cea.fr>
Date:   Mon Oct 23 16:55:21 2023 +0200

    [wp] split conjunctions only when looking in hyps

commit 75d3f505
Author: Jan Rochel <jan.rochel@cea.fr>
Date:   Mon Oct 23 16:08:39 2023 +0200

    [alias] correctly expose Abstract_state including graph

commit 1a11dfa8
Author: Loïc Correnson <loic.correnson@cea.fr>
Date:   Mon Oct 23 16:17:24 2023 +0200

    [wp] test for fixed non-terminating strategy

commit 679edcaf
Author: Loïc Correnson <loic.correnson@cea.fr>
Date:   Mon Oct 23 16:08:58 2023 +0200

    [wp] progressing check after tactic

commit 49439a79
Author: Loïc Correnson <loic.correnson@cea.fr>
Date:   Mon Oct 23 15:43:47 2023 +0200

    [wp] limit depth of exploration with strategies

commit 4b3f48e5
Author: Loïc Correnson <loic.correnson@cea.fr>
Date:   Mon Oct 23 14:39:02 2023 +0200

    [dev] remove --version

commit 293ae307
Author: Loïc Correnson <loic.correnson@cea.fr>
Date:   Mon Oct 23 12:21:21 2023 +0200

    [dev] make-distrib options

commit a1c78b46
Merge: 624a6667 095954d9
Author: Allan Blanchard <allan.blanchard@cea.fr>
Date:   Thu Oct 19 14:33:41 2023 +0000

    Merge branch 'feature/blanchard/wp/default-spec' into 'master'

    WP populate spec

    Closes #1303

    See merge request frama-c/frama-c!4362

commit 624a6667
Merge: 7dd5bd76 a4c723c6
Author: Allan Blanchard <allan.blanchard@cea.fr>
Date:   Thu Oct 19 14:07:53 2023 +0000

    Merge branch 'feature/martin/doc/1310-document-properly-the-behavior-of-the-default-spec-generator' into 'master'

    Resolve "Document properly the behavior of the default spec generator"

    Closes #1310

    See merge request frama-c/frama-c!4339

commit 095954d9
Author: Allan Blanchard <allan.blanchard@cea.fr>
Date:   Thu Oct 19 15:58:45 2023 +0200

    [wp] ChangeLog

commit 29c8f325
Author: Allan Blanchard <allan.blanchard@cea.fr>
Date:   Thu Oct 19 15:20:05 2023 +0200

    [wp] fix test after rebase

commit a4c723c6
Author: Thibault Martin <thi.martin.pro@pm.me>
Date:   Thu Oct 19 15:11:05 2023 +0200

    [doc] Add details about warnings + minors changes

commit 7b749a3f
Author: Allan Blanchard <allan.blanchard@cea.fr>
Date:   Thu Oct 19 14:05:33 2023 +0200

    [wp/doc] Add generated and verified clauses to the manual

commit 3d892e48
Author: Allan Blanchard <allan.blanchard@cea.fr>
Date:   Thu Oct 19 11:27:37 2023 +0200

    [wp] warn on missing default assigns

commit 118721ad
Author: Allan Blanchard <allan.blanchard@cea.fr>
Date:   Thu Oct 19 10:32:31 2023 +0200

    [wp] changes strategy for callees assigns

commit 205cc850
Author: Allan Blanchard <allan.blanchard@cea.fr>
Date:   Wed Oct 18 10:39:45 2023 +0200

    [wp] lint

commit bf3fcc8e
Author: Allan Blanchard <allan.blanchard@cea.fr>
Date:   Fri Oct 13 16:58:25 2023 +0200

    [wp] update oracles

commit 14293eab
Author: Allan Blanchard <allan.blanchard@cea.fr>
Date:   Fri Oct 13 16:58:11 2023 +0200

    [wp] add spec populate for API calls

commit 15d6aa28
Author: Allan Blanchard <allan.blanchard@cea.fr>
Date:   Thu Oct 12 14:27:42 2023 +0200

    [wp] temporarily disabled stmtcompiler test

commit fcd4fe75
Author: Allan Blanchard <allan.blanchard@cea.fr>
Date:   Thu Oct 12 14:27:20 2023 +0200

    [wp] update test

commit c75a5946
Author: Loïc Correnson <loic.correnson@cea.fr>
Date:   Thu Oct 12 10:51:57 2023 +0200

    [wp] reformat cfg status

commit 5cfa60c8
Author: Loïc Correnson <loic.correnson@cea.fr>
Date:   Thu Oct 12 10:37:52 2023 +0200

    [wp] update test

commit c1701ced
Author: Loïc Correnson <loic.correnson@cea.fr>
Date:   Thu Oct 12 10:25:51 2023 +0200

    [wp] update test

commit 0552c3c2
Author: Allan Blanchard <allan.blanchard@cea.fr>
Date:   Wed Oct 11 14:32:55 2023 +0200

    [wp] remove options related to terminates generation

commit d1abe35d
Author: Thibault Martin <thi.martin.pro@pm.me>
Date:   Tue Aug 8 16:35:13 2023 +0200

    Update WP oracles

commit 05358a06
Author: Thibault Martin <thi.martin.pro@pm.me>
Date:   Tue Aug 8 15:30:00 2023 +0200

    Update aorai oracles

commit 85b4cf27
Author: Allan Blanchard <allan.blanchard@cea.fr>
Date:   Thu Sep 28 14:37:49 2023 +0200

    [wp] use kernel default spec populate
    - deprecate parameters related to populate
    - do not populate when finding missing terminates

commit 770ec85b
Author: Allan Blanchard <allan.blanchard@cea.fr>
Date:   Wed Oct 11 13:51:36 2023 +0200

    [wp] fix WP target for main function

commit 9055efa3
Author: Allan Blanchard <allan.blanchard@cea.fr>
Date:   Thu Oct 19 14:43:36 2023 +0200

    [doc] typos

commit f156a6c5
Author: Thibault Martin <thi.martin.pro@pm.me>
Date:   Tue Oct 17 10:01:10 2023 +0200

    [doc] Details about combining clauses from behaviors

commit 550dd458
Author: Thibault Martin <thi.martin.pro@pm.me>
Date:   Mon Oct 9 15:02:34 2023 +0200

    [doc] Describe populate_spec modes in userman

commit eef7f40c
Author: Thibault Martin <thi.martin.pro@pm.me>
Date:   Mon Oct 9 14:56:50 2023 +0200

    [doc] Add tables in devman for custom mode example

commit 7f46efab
Author: Thibault Martin <thi.martin.pro@pm.me>
Date:   Mon Oct 9 14:52:06 2023 +0200

    [doc] Fix mode description in populate_spec

commit 96b4427e
Author: Thibault Martin <thi.martin.pro@pm.me>
Date:   Mon Oct 9 10:09:51 2023 +0200

    [doc] devman: rewrite / fix typo

commit 827ea463
Author: Thibault Martin <thi.martin.pro@pm.me>
Date:   Wed Oct 4 14:27:00 2023 +0200

    [doc] populate_funspec now can take an optionnal location

commit 89b2eba7
Author: Thibault Martin <thi.martin.pro@pm.me>
Date:   Tue Oct 3 16:57:19 2023 +0200

    [doc] Fix some typos, indent code

commit e32b56f3
Author: Thibault Martin <thi.martin.pro@pm.me>
Date:   Tue Oct 3 16:12:05 2023 +0200

    [tests] Fix and update Populate_spec example

commit f9ca7016
Author: Thibault Martin <thi.martin.pro@pm.me>
Date:   Tue Oct 3 11:45:30 2023 +0200

    [doc] Populate_spec explanation for plug-in developpers

commit 7dd5bd76
Merge: 517cc90b 5b924bea
Author: Allan Blanchard <allan.blanchard@cea.fr>
Date:   Thu Oct 19 12:20:43 2023 +0000

    Merge branch 'fix/martin/kernel/do-not-add-empty-default-behavior' into 'master'

    Add the newly created behavior only if it is not empty

    See merge request frama-c/frama-c!4370

commit 5b924bea
Author: Thibault Martin <thi.martin.pro@pm.me>
Date:   Wed Oct 18 10:18:26 2023 +0200

    Update test oracles

commit bbec67ab
Author: Thibault Martin <thi.martin.pro@pm.me>
Date:   Tue Oct 17 14:17:32 2023 +0200

    Add the new behavior only if it is not empty

commit a4fc83c5
Author: Loïc Correnson <loic.correnson@cea.fr>
Date:   Mon Oct 16 15:36:14 2023 +0200

    [ivette] fix macOS script

commit 4bf59c78
Author: Allan Blanchard <allan.blanchard@cea.fr>
Date:   Mon Oct 16 10:26:41 2023 +0200

    [doc] release manual
    - update what the set-version script does

commit 477d5b5e
Author: Allan Blanchard <allan.blanchard@cea.fr>
Date:   Mon Oct 16 10:24:20 2023 +0200

    [dev] extend set-version.sh
    - also update Frama-C build script
6a763469
History
user avatar 6a763469
History
Name Last commit Last update
.gitlab
bin
dev
doc
headers
ivette
lib/plugins
licenses
man
nix
releases
share
src
tests
tools
.git-blame-ignore-revs
.gitattributes
.gitignore
.gitlab-ci.yml
.mailmap
.ocp-indent
ALL_VERSIONS
CLA.md
CLA.pdf
CONTRIBUTING.md
Changelog
Changelog_detailed.md
INSTALL.md
LICENSE
Makefile
README.md
TCA.md
VERSION
VERSION_CODENAME
configurator.ml
dune
dune-project
opam
reference-configuration.md
README.md

Frama-C

Frama-C is a platform dedicated to the analysis of source code written in C.

A Collaborative Platform

Frama-C gathers several analysis techniques in a single collaborative platform, consisting of a kernel providing a core set of features (e.g., a normalized AST for C programs) plus a set of analyzers, called plug-ins. Plug-ins can build upon results computed by other plug-ins in the platform.

Thanks to this approach, Frama-C provides sophisticated tools, including:

  • an analyzer based on abstract interpretation, aimed at verifying the absence of run-time errors (Eva);
  • a program proof framework based on weakest precondition calculus (WP);
  • a program slicer (Slicing);
  • a tool for verification of temporal (LTL) properties (Aoraï);
  • a runtime verification tool (E-ACSL);
  • several tools for code base exploration and dependency analysis (From, Impact, Metrics, Occurrence, Scope, etc.).

These plug-ins share a common language and can exchange information via ACSL (ANSI/ISO C Specification Language) properties. Plug-ins can also collaborate via their APIs.

Installation

Frama-C is available through opam, the OCaml package manager. If you have it, simply run:

opam install frama-c

or, for opam versions less than 2.1.0:

opam install depext # handles external (non-OCaml) dependencies
opam depext frama-c --install

Frama-C is developed mainly in Linux, often tested in macOS (via Homebrew), and occasionally tested on Windows (via the Windows Subsystem for Linux).

For detailed installation instructions and troubleshooting, see INSTALL.md.

Development branch

To install the development branch of Frama-C (updated nightly):

opam pin add frama-c --dev-repo

This command will pin the development version of Frama-C and try to install it. If installation fails due to missing external dependencies, try using the same commands from the Installation section to get the external dependencies and then install Frama-C.

Distribution packages

Some Linux distributions have a frama-c package, kindly provided by distribution packagers. Note that they may not correspond to the latest Frama-C release.

Usage

Frama-C can be run from the command-line, or via its graphical interface.

Simple usage

The recommended usage for simple files is one of the following lines:

frama-c file.c -<plugin> [options]
frama-c-gui file.c

Where -<plugin> is one of the several Frama-C plug-ins, e.g. -eva, or -wp, or -metrics, etc. Plug-ins can also be run directly from the GUI.

To list all plug-ins, run:

frama-c -plugins

Each plug-in has a help command (-<plugin>-help or -<plugin>-h) that describes its own options.

Finally, the list of options governing the behavior of Frama-C's kernel itself is available through

frama-c -kernel-help

Complex scenarios

For more complex usage scenarios (lots of files and directories, with several preprocessing directives), we recommend splitting Frama-C's usage in two parts:

  1. Parsing the input files and saving the result to a file;
  2. Loading the parsing results and then running the analyses or the GUI.

Parsing typically involves giving extra arguments to the C preprocessor, so the -cpp-extra-args option is often useful, as in the example below:

frama-c *.c *.h -cpp-extra-args="-D<define> -I<include>" -save parsed.sav

The results are then loaded into Frama-C for further analyses or for inspection via the GUI:

frama-c -load parsed.sav -<plugin> [options]
frama-c-gui -load parsed.sav -<plugin> [options]

Further reference