Skip to content

GitLab

Commit 88886e5f authored by Loïc Correnson's avatar Loïc Correnson
Browse files

[wp] linting files

parent a35d2118
Expand all Hide whitespace changes
Inline Side-by-side
.for_devel 0 → 100644
View file @ 88886e5f
This file activates the compilation of Frama-C in developer mode
- enable warnings and warn-error
- create .merlin file
- create links in ./share to plugin share directory for
the bin/frama-c* script
.gitattributes 0 → 100644
View file @ 88886e5f
Changelog merge=union
*.pdf binary
.gitignore 0 → 100644
View file @ 88886e5f
###########
# General #
###########
TAGS
*.cm*
*.o
*.a
*.annot
#ocamlyacc -v
*.output
*~
*_DEP
*.depend
\#*
.\#*
.DS_Store
*.tmp
*.s
#artifacts from execution
frama_c_journal.ml
/.frama-c/
/frama-c-*.tar.gz
/.merlin
/headers/hdrck
#build
configure
autom4te.cache
.log.autoconf
/.depend
/config.log
/config.status
/frama-c-*.tar.gz
/.log.autoconf
/.Makefile.user
/ocamlgraph/
*.check_mli_exists
.Makefile.plugin.generated
#tests
/tests/ptests_config
/tests/*/result/
/tests/*/result_*/
/tests/journal/intra.byte
/tests/misc/my_visitor_plugin/my_visitor.opt
/tests/misc/my_visitor.sav
/tests/*/*.opt
/tests/pdg/*.dot
/devel_tools/fc-time
/devel_tools/fc-memuse
#share
/share/Makefile.config
/share/Makefile.dynamic_config
/share/Makefile.kernel
/share/frama-c.rc
#created by create_share_link target
/share/.gitignore
/share/manuals/
#doc
/doc/manuals/
/doc/*/*.dot
/doc/*/*.aux
/doc/*/*.bbl
/doc/*/*.blg
/doc/*/*.cb*
/doc/*/*.ilg
/doc/*/*.ind
/doc/*/*.toc
/doc/*/*.lof
/doc/*/*.log
/doc/*/*.out
/doc/*/*.idx
/doc/*/*.fls
/doc/*/*.fdb_latexmk
/doc/*/*.synctex.gz
/doc/acsl/
/doc/aorai/frama-c-aorai-example.tgz
/doc/aorai/frama-c-aorai-example
/doc/aorai/main.pdf
/doc/aorai/basic_ya.tex
/doc/aorai/extended_ya.tex
/doc/code/print_api/*.html
/doc/code/print_api/*.dot
/doc/code/print_api/lexer.ml
/doc/code/print_api/grammar.mli
/doc/code/print_api/grammar.ml
/doc/code/print_api/dynamic_plugins.mli
/doc/code/print_api/_build/
/doc/code/studia
/doc/code/qed
/doc/code/wp
/doc/pdg/call-f.eps
/doc/pdg/call-f.fig
/doc/pdg/call-f.pdf
/doc/pdg/call-g.eps
/doc/pdg/call-g.fig
/doc/pdg/call-g.pdf
/doc/pdg/compil.ok
/doc/pdg/contents_motif.gif
/doc/pdg/ctrl-dpds.eps
/doc/pdg/ctrl-dpds.pdf
/doc/pdg/ex-goto.eps
/doc/pdg/ex-goto.pdf
/doc/pdg/exple-call.c
/doc/pdg/goto.eps
/doc/pdg/goto.pdf
/doc/pdg/index.html
/doc/pdg/logo-inria-sophia.eps
/doc/pdg/logo-inria-sophia.pdf
/doc/pdg/next_motif.gif
/doc/pdg/pdg-call.eps
/doc/pdg/pdg-call.pdf
/doc/pdg/pdg.css
/doc/pdg/pdg.dvi
/doc/pdg/pdg.haux
/doc/pdg/pdg.hind
/doc/pdg/pdg.html
/doc/pdg/pdg.htoc
/doc/pdg/pdg.image.tex
/doc/pdg/pdg.ps
/doc/pdg/pdg0*.html
/doc/pdg/pdg00*.png
/doc/pdg/previous_motif.gif
#lib
/lib/fc/
/lib/plugins/*.mli
/lib/plugins/*.ml
/lib/plugins/top/
/lib/plugins/gui/
/lib/plugins/top/
/lib/plugins/META.frama-c-*
/lib/plugins/.placeholders_ready
#plugins
/share/e-acsl/
/share/c2fc/
/src/plugins/*/configure
/src/plugins/*/.depend
/src/plugins/*/autom4te.cache/
/src/plugins/*/Makefile.plugin.generated
/src/plugins/*/doc/*/*.dot
/src/plugins/*/doc/*/*.aux
/src/plugins/*/doc/*/*.bbl
/src/plugins/*/doc/*/*.blg
/src/plugins/*/doc/*/*.cb*
/src/plugins/*/doc/*/*.ilg
/src/plugins/*/doc/*/*.ind
/src/plugins/*/doc/*/*.toc
/src/plugins/*/doc/*/*.lof
/src/plugins/*/doc/*/*.log
/src/plugins/*/doc/*/*.out
/src/plugins/*/doc/*/*.idx
Makefile.plugin.generated
# WP/Coq Generated file
.lia.cache
# generated ML files
/src/libraries/utils/json.ml
/src/kernel_internals/runtime/toplevel_boot.ml
/src/kernel_internals/runtime/config.ml
/src/kernel_internals/runtime/frama_c_config.ml
/src/kernel_internals/parsing/logic_lexer.ml
/src/kernel_internals/parsing/logic_parser.ml
/src/kernel_internals/parsing/logic_parser.mli
/src/kernel_internals/parsing/logic_preprocess.ml
/src/kernel_internals/parsing/clexer.ml
/src/kernel_internals/parsing/cparser.ml
/src/kernel_internals/parsing/cparser.mli
/src/plugins/value/domains/apron/apron_domain.ml
/src/kernel_services/ast_queries/json_compilation_database.ml
/src/libraries/stdlib/transitioning.ml
# generated tar.gz files
/doc/developer/hello.tar.gz
hello-*.tar.gz
#######################
# should remain empty #
#######################
.gitlab-ci.yml 0 → 100644
View file @ 88886e5f
stages:
- frama_c_and_plugins
- distrib_and_compatibility
frama-c-external:
stage: frama_c_and_plugins
script:
- ~oci/oci/bin/bf_client.native run --socket ~oci/data/oci-data/oci.socket --frama-c $CI_BUILD_REF --branch $CI_BUILD_REF_NAME frama-c-external --cppo 07d2bcee50670aecae7e094d92f68fd18314073a --ocamlgraph 9286b375c005d1d504a1def0c5986f54c7f12251 --url ocamlfind,git@git.frama-c.com:bobot/ocamlfind.git
tags:
except:
- tags
retry: 2
frama-c:
stage: frama_c_and_plugins
script:
- ~oci/oci/bin/bf_client.native run --socket ~oci/data/oci-data/oci.socket --frama-c $CI_BUILD_REF --branch $CI_BUILD_REF_NAME frama-c --cppo 07d2bcee50670aecae7e094d92f68fd18314073a --ocamlgraph 9286b375c005d1d504a1def0c5986f54c7f12251 --url ocamlfind,git@git.frama-c.com:bobot/ocamlfind.git
tags:
except:
- tags
retry: 2
frama-c-ocaml-4.03:
stage: distrib_and_compatibility
script:
- ~oci/oci/bin/bf_client.native run --socket ~oci/data/oci-data/oci.socket --ocaml 4.03 --camlp4 4.03 --frama-c $CI_BUILD_REF --branch $CI_BUILD_REF_NAME frama-c --cppo 07d2bcee50670aecae7e094d92f68fd18314073a --ocamlgraph 9286b375c005d1d504a1def0c5986f54c7f12251 --url ocamlfind,git@git.frama-c.com:bobot/ocamlfind.git
tags:
except:
- tags
retry: 2
frama-c-ocaml-4.04:
stage: distrib_and_compatibility
script:
- ~oci/oci/bin/bf_client.native run --socket ~oci/data/oci-data/oci.socket --ocaml 4.04 --camlp4 4.04 --lablgtk 4bbd5cf1990aa8b775cf247fbfe5be321e13cc61 --frama-c $CI_BUILD_REF --branch $CI_BUILD_REF_NAME frama-c --cppo 07d2bcee50670aecae7e094d92f68fd18314073a --ocamlgraph 9286b375c005d1d504a1def0c5986f54c7f12251 --url ocamlfind,git@git.frama-c.com:bobot/ocamlfind.git
tags:
except:
- tags
retry: 2
frama-c-ocaml-4.05:
stage: distrib_and_compatibility
script:
- ~oci/oci/bin/bf_client.native run --socket ~oci/data/oci-data/oci.socket --ocaml 4.05 --camlp4 4.05 --lablgtk 4bbd5cf1990aa8b775cf247fbfe5be321e13cc61 --camomile 3f4d657d50c17213f3338ca75efb30d728704df3 --frama-c $CI_BUILD_REF --branch $CI_BUILD_REF_NAME frama-c --cppo 07d2bcee50670aecae7e094d92f68fd18314073a --ocamlgraph 9286b375c005d1d504a1def0c5986f54c7f12251 --url ocamlfind,git@git.frama-c.com:bobot/ocamlfind.git
tags:
except:
- tags
retry: 2
allow_failure: true
frama-c-internal:
stage: distrib_and_compatibility
script:
- ~oci/oci/bin/bf_client.native run --socket ~oci/data/oci-data/oci.socket --frama-c $CI_BUILD_REF --branch $CI_BUILD_REF_NAME frama-c-internal --cppo 07d2bcee50670aecae7e094d92f68fd18314073a --ocamlgraph 9286b375c005d1d504a1def0c5986f54c7f12251 --url ocamlfind,git@git.frama-c.com:bobot/ocamlfind.git
tags:
only:
- master
- stable/silicium
except:
- tags
retry: 2
frama-c-distrib:
stage: distrib_and_compatibility
script:
- ~oci/oci/bin/bf_client.native run --socket ~oci/data/oci-data/oci.socket --frama-c $CI_BUILD_REF --branch $CI_BUILD_REF_NAME frama-c-distrib --cppo 07d2bcee50670aecae7e094d92f68fd18314073a --ocamlgraph 9286b375c005d1d504a1def0c5986f54c7f12251 --url ocamlfind,git@git.frama-c.com:bobot/ocamlfind.git
tags:
except:
- tags
retry: 2
Genassigns:
stage: frama_c_and_plugins
script:
- ~oci/oci/bin/bf_client.native run --socket ~oci/data/oci-data/oci.socket --frama-c $CI_BUILD_REF --branch $CI_BUILD_REF_NAME Genassigns --cppo 07d2bcee50670aecae7e094d92f68fd18314073a --ocamlgraph 9286b375c005d1d504a1def0c5986f54c7f12251 --url ocamlfind,git@git.frama-c.com:bobot/ocamlfind.git
tags:
except:
- tags
retry: 2
Mthread:
stage: frama_c_and_plugins
script:
- ~oci/oci/bin/bf_client.native run --socket ~oci/data/oci-data/oci.socket --frama-c $CI_BUILD_REF --branch $CI_BUILD_REF_NAME Mthread --cppo 07d2bcee50670aecae7e094d92f68fd18314073a --ocamlgraph 9286b375c005d1d504a1def0c5986f54c7f12251 --url ocamlfind,git@git.frama-c.com:bobot/ocamlfind.git
tags:
except:
- tags
retry: 2
a3export:
stage: frama_c_and_plugins
script:
- ~oci/oci/bin/bf_client.native run --socket ~oci/data/oci-data/oci.socket --frama-c $CI_BUILD_REF --branch $CI_BUILD_REF_NAME a3export --cppo 07d2bcee50670aecae7e094d92f68fd18314073a --ocamlgraph 9286b375c005d1d504a1def0c5986f54c7f12251 --url ocamlfind,git@git.frama-c.com:bobot/ocamlfind.git
tags:
except:
- tags
retry: 2
PathCrawler:
stage: frama_c_and_plugins
script:
- ~oci/oci/bin/bf_client.native run --socket ~oci/data/oci-data/oci.socket --frama-c $CI_BUILD_REF --branch $CI_BUILD_REF_NAME PathCrawler --cppo 07d2bcee50670aecae7e094d92f68fd18314073a --ocamlgraph 9286b375c005d1d504a1def0c5986f54c7f12251 --url ocamlfind,git@git.frama-c.com:bobot/ocamlfind.git
tags:
except:
- tags
retry: 2
Security:
stage: frama_c_and_plugins
script:
- ~oci/oci/bin/bf_client.native run --socket ~oci/data/oci-data/oci.socket --frama-c $CI_BUILD_REF --branch $CI_BUILD_REF_NAME Security --cppo 07d2bcee50670aecae7e094d92f68fd18314073a --ocamlgraph 9286b375c005d1d504a1def0c5986f54c7f12251 --url ocamlfind,git@git.frama-c.com:bobot/ocamlfind.git
tags:
except:
- tags
retry: 2
E-ACSL:
stage: frama_c_and_plugins
script:
- ~oci/oci/bin/bf_client.native run --socket ~oci/data/oci-data/oci.socket --frama-c $CI_BUILD_REF --branch $CI_BUILD_REF_NAME E-ACSL --cppo 07d2bcee50670aecae7e094d92f68fd18314073a --ocamlgraph 9286b375c005d1d504a1def0c5986f54c7f12251 --url ocamlfind,git@git.frama-c.com:bobot/ocamlfind.git
tags:
except:
- tags
allow_failure: true
retry: 2
context-from-precondition:
stage: frama_c_and_plugins
script:
- ~oci/oci/bin/bf_client.native run --socket ~oci/data/oci-data/oci.socket --frama-c $CI_BUILD_REF --branch $CI_BUILD_REF_NAME context-from-precondition --cppo 07d2bcee50670aecae7e094d92f68fd18314073a --ocamlgraph 9286b375c005d1d504a1def0c5986f54c7f12251 --url ocamlfind,git@git.frama-c.com:bobot/ocamlfind.git
tags:
except:
- tags
retry: 2
open-source-case-studies:
stage: frama_c_and_plugins
script:
- ~oci/oci/bin/bf_client.native run --socket ~oci/data/oci-data/oci.socket --frama-c $CI_BUILD_REF --url open-source-case-studies,git@git.frama-c.com:frama-c/open-source-case-studies.git --commit open-source-case-studies,master open-source-case-studies --cppo 07d2bcee50670aecae7e094d92f68fd18314073a --ocamlgraph 9286b375c005d1d504a1def0c5986f54c7f12251 --url ocamlfind,git@git.frama-c.com:bobot/ocamlfind.git
tags:
except:
- tags
when: manual
retry: 2
ACSL-importer:
stage: frama_c_and_plugins
script:
- ~oci/oci/bin/bf_client.native run --socket ~oci/data/oci-data/oci.socket --frama-c $CI_BUILD_REF --branch $CI_BUILD_REF_NAME ACSL-importer --cppo 07d2bcee50670aecae7e094d92f68fd18314073a --ocamlgraph 9286b375c005d1d504a1def0c5986f54c7f12251 --url ocamlfind,git@git.frama-c.com:bobot/ocamlfind.git
tags:
except:
- tags
retry: 2
Caveat-importer:
stage: frama_c_and_plugins
script:
- ~oci/oci/bin/bf_client.native run --socket ~oci/data/oci-data/oci.socket --frama-c $CI_BUILD_REF --branch $CI_BUILD_REF_NAME Caveat-importer --cppo 07d2bcee50670aecae7e094d92f68fd18314073a --ocamlgraph 9286b375c005d1d504a1def0c5986f54c7f12251 --url ocamlfind,git@git.frama-c.com:bobot/ocamlfind.git
tags:
except:
- tags
retry: 2
Volatile:
stage: frama_c_and_plugins
script:
- ~oci/oci/bin/bf_client.native run --socket ~oci/data/oci-data/oci.socket --frama-c $CI_BUILD_REF --branch $CI_BUILD_REF_NAME Volatile --cppo 07d2bcee50670aecae7e094d92f68fd18314073a --ocamlgraph 9286b375c005d1d504a1def0c5986f54c7f12251 --url ocamlfind,git@git.frama-c.com:bobot/ocamlfind.git
tags:
except:
- tags
retry: 2
.mailmap 0 → 100644
View file @ 88886e5f
#
# Fix email or name in commits. Used during pretty printing by git shortlog, blame, ...
# It can be used also for git log, git show, git whatchanged with
# git config --global log.mailmap true
#
Virgile Prevosto <virgile.prevosto@cea.fr> <virgile.prevosto@m4x.org>
Virgile Prevosto <virgile.prevosto@cea.fr>
<pascal.cuoq@cea.fr> <Pascal.CUOQ@cea.fr>
Muriel Roger <muriel.roger@cea.fr>
<julien.signoles@cea.fr> <signoles@ns61143.ovh.net>
<julien.signoles@cea.fr> <jsignole@is005030.intra.cea.fr>
<loic.correnson@cea.fr> <lcorrenson@gmail.com>
<loic.correnson@cea.fr> <loïc.correnson@cea.fr>
Géraud Canet <geraud.canet@cea.fr>
<mounir.assaf@cea.fr> <mounir.assaf@cea.Fr>
\ No newline at end of file
ALL_VERSIONS 0 → 100644
View file @ 88886e5f
Version number Date of release Notes
============== =============== =====
Sulfur-20171101 2017, November 28
Phosphorus-20170501 2017, May 29
Silicon-20161101 2016, December 2
Aluminium-20160502 2016, May 31
Aluminium-20160501 2016, May 30 Removed
Aluminium-rc1 2016, May 13 Not publicly released
Magnesium-20151002 2016, January 15
Magnesium-20151001 2015, October 27 Not publicly released
Sodium-20150201 2015, March 9
Neon-20140301 2014, May 7
Fluorine-20130601 2013, June 11 Bug fixed
Fluorine-20130501 2013, May 23 Bug fixed
Fluorine-20130401 2013, April 17
Oxygen-20120901 2012, September 19
Nitrogen-20111001 2011, October 10
Carbon-20110201 2011, February 7
Carbon-20101202-beta2 2010, December 17 Source only
Carbon-20101201-beta1 2010, December 14 Source only
Boron-20100401 2010, April 12
Beryllium-20090902 2009, September 23
Beryllium-20090901 2009, September 01
Beryllium-20090601-beta1 2009, June 23 Source only
Lithium-20081201 2008, Decembre 16
Lithium-20081002+beta1 2008, October 28
Lithium-20081001+alpha0 2008, October 03 Source only
Helium-20080701 2008, July 11
Hydrogen-20080502 2008, May 26 No cvs tag
Hydrogen-20080501 2008, May 05 Source only, No cvs tag
Hydrogen-20080302 2008, March 27 Binary only
Hydrogen-20080301 (Hydrogen) 2008, March 03 Source only
Changelog 0 → 100644
View file @ 88886e5f
This source diff could not be displayed because it is too large. You can view the blob instead.
Changelog_detailed.md 0 → 100644
View file @ 88886e5f
This file provides a detailed description of the main changes in the API
of Frama-C. It is intended for developers only. For a summary of all changes,
please refer to Changelog.
* Changes between Sodium and Magnesium
** Use of Value-based plug-ins:
In case your plug-in programmatically uses one of the following plug-ins
(even through Db):
Value, Metrics, Occurrence, From, Users, Constant_Propagation, Inout,
Impact, Pdg, Scope, Sparecode, Slicing
You must add the following line in your plug-in Makefile:
PLUGIN_DEPENDENCIES:=<plug-ins list>
For instance, if you depend on Value, Pdg and Slicing, you must write:
PLUGIN_DEPENDENCIES:=Value Pdg Slicing
** Callgraph Access
In Sodium, there were three different callgraph implementations:
- module Callgraph
- plug-in Syntactic_callgraph (based on Callgraph)
- plug-in Semantic_callgraph (based on Value to solve function pointers)
The first one was almost an internal Frama-C module and directly exposed its
internal datastructure based on Hashtbl, while the second and the third one
exported a few functions through module Db.
In Magnesium, these three modules and plug-ins are replaced by a single
plug-in: Callgraph. This plug-in exports an API for plug-in developers through
its interface Callgraph.mli (which is nowadays the recommended way, see
Plug-in Development Guide, Section 3.4). The script sodium2magnesium.sh
automatically converts the uses of Db.Syntactic_callgraph and
Db.Semantic_callgraph to the new API, but you have to add the following line
to your plug-in Makefile to get an access to the API:
PLUGIN_DEPENDENCIES:=Callgraph <possibly other dependencies>
* Changes between Oxygen and Fluorine
** Removal of rooted_code_annotation
The datatype Cil_types.rooted_code_annotation has been removed. It was used to
distinguish between annotations present in the original sources and
annotations generated by the plug-ins, and has never been really used.
All functions that were using Cil_types.rooted_code_annotation now use
directly Cil_types.code_annotation.
*** Removed identifiers
- Constructors Cil_types.User and Cil_types.AI
- Function Ast_info.is_trivial_rooted_assertion
(replaced by Ast_info.is_trivial_annotation)
- Function Ast_info.lift_annot_func (useless)
- Function Ast_info.lift_annot_list_func (useless)
- Function Ast_info.d_rooted_code_annotation (useless)
- Function Annotation.code_annotation_of_rooted (useless)
- Module Cil_datatype.Rooted_code_annotation (useless)
- Method vrooted_code_annotation in Visitor.frama_c_visitor (useless)
*** Distinction between user annotations and generated annotations
The origin of an annotation is now given by its emitter, which can be retrieved
via Annotations.fold_code_annot and Annotations.iter_code_annot. For instance,
the following Oxygen code
#+BEGIN_SRC ocaml
Annotations.iter_code_annot
(fun _ annot ->
match annot with
| User a -> f a
| AI(_,a) -> g a)
stmt
#+END_SRC
will be translated that way for Fluorine:
#+BEGIN_SRC ocaml
Annotations.iter_code_annot
(fun e annot ->
if Emitter.equal e Emitter.end_user then
f annot
else
g annot)
stmt
#+END_SRC
*** Visitor
vrooted_code_annotation could return a list of annotations,
while vcode_annotation must return a single annotation (however, if it is
trivial, i.e. assert \true, it will be discarded). Code visiting
vrooted_code_annotation and returning several annotations at once must thus
be rewritten (e.g. by taking care of registering the additional annotations
directly).
** Message categories
Debug keys is a feature added in Nitrogen to allow showing only specific debug
messages of a plug-in or the kernel. Related interface has changed in Fluorine.
See src/kernel/log.mli for more details.
*** Keys for feedback and result
keys are not restricted to debug, but can be used for feedback and result.
*** New datatype
Keys were plain strings. There is now a category type, which is a private
alias for string: each key must be registered before being used.
*** Sub-categories
There are subcategories, which are implicitly defined by using columns (':')
in the category name. For instance a:b:c denotes a sub-category c of b, itself
a subcategory of a. a and a:b do not need to be already registered before
registration of a:b:c. Enabling display of messages of a will also enable
a:b and a:b:c
*** New command line options
The option for enforcing a category of message was -plugin-debug-category.
It is now -plugin-msg-key. -plugin-msg-key-unset allows to remove some
previously enabled category (either directly or as a subcategory of an enabled
category), and its subcategory. For instance
-plugin-msg-key a -plugin-msg-unset a:b -plugin-msg-set a:b:c will enable
messages for a and a:b:c
-plugin-msg-key supports two special keys:
- help will display the list of existing categories
- * will enable all categories
INSTALL.md 0 → 100644
View file @ 88886e5f
# Installing Frama-C
## Table of Contents
- [Installing Frama-C](#installing-frama-c)
- [Table of Contents](#table-of-contents)
- [Recommended mode: OPAM](#recommended-mode-opam)
- [Installing OPAM](#installing-opam)
- [Installing Frama-C from OPAM](#installing-frama-c-from-opam)
- [Installing Custom Versions of Frama-C via OPAM](#installing-custom-versions-of-frama-c-via-opam)
- [Installing Frama-C on Windows (via Cygwin + OPAM)](#installing-frama-c-on-windows-via-cygwin--opam)
- [Installing Frama-C on Mac OS X](#installing-frama-c-on-mac-os-x)
- [Installing Frama-C via your Linux distribution (Debian/Ubuntu/Fedora)](#installing-frama-c-via-your-linux-distribution-debianubuntufedora)
- [Compiling from source](#compiling-from-source)
- [Quick Start](#quick-start)
- [Full Compilation Guide](#full-compilation-guide)
- [Available resources](#available-resources)
- [Executables: (in `/INSTALL_DIR/bin`)](#executables-in-install_dirbin)
- [Shared files: (in `/INSTALL_DIR/share/frama-c` and subdirectories)](#shared-files-in-install_dirshareframa-c-and-subdirectories)
- [Documentation files: (in `/INSTALL_DIR/share/frama-c/doc`)](#documentation-files-in-install_dirshareframa-cdoc)
- [Object files: (in `/INSTALL_DIR/lib/frama-c`)](#object-files-in-install_dirlibframa-c)
- [Plugin files: (in `/INSTALL_DIR/lib/frama-c/plugins`)](#plugin-files-in-install_dirlibframa-cplugins)
- [Man files: (in `/INSTALL_DIR/man/man1`)](#man-files-in-install_dirmanman1)
- [Installing Additional Plugins](#installing-additional-plugins)
- [HAVE FUN WITH FRAMA-C!](#have-fun-with-frama-c)
## Recommended mode: OPAM
The preferred method of installation for Frama-C is using
[OPAM](http://opam.ocaml.org/) (v1.2.2 or newer).
First you need to install OPAM, then you may install Frama-C using OPAM:
opam install frama-c
**Note:** make sure your OPAM version is >= 1.2.2.
Also, it is highly recommended that you install an external solver
for OPAM, such as `aspcud`, otherwise unexpected dependency errors
may occur during installation.
### Installing OPAM
Several Linux distributions already include an `opam` package.
OSX has OPAM through Homebrew.
A [Cygwin-based OPAM](https://fdopen.github.io/opam-repository-mingw/installation)
is available on Windows. It is less stable than it is for the other OSes, but should work.
If your system does not have an OPAM package >= 1.2.2 you can compile it from source,
or use the provided OPAM binaries available at:
http://opam.ocaml.org/doc/Install.html
### Installing Frama-C from OPAM
Tha Frama-C package in OPAM is called `frama-c`, which includes both the
command-line `frama-c` executable and the graphical interface `frama-c-gui`.
(Note: before version 16 Sulfur, there were two packages, `frama-c-base` and
`frama-c`, which were merged together.)
`frama-c` includes non-OCaml dependencies, such as Gtk and GMP. In most
systems, OPAM can take care of these external dependencies through
its `depext` plug-in: issuing the two commands
opam install depext
opam depext frama-c
will install the appropriate system packages (this of course requires
administrator rights on the system).
If your system is not supported by `depext`, you will need to install
Gtk, GtkSourceView, GnomeCanvas and GMP, including development libraries,
separately. If you do so, please consider providing the system name and list of
packages (e.g. via a [Github issue](https://github.com/Frama-C/Frama-C-snapshot/issues/new))
so that we can add it to the Frama-C `depext` package.
### Installing Custom Versions of Frama-C via OPAM
If you have a **non-standard** version of Frama-C available
(with proprietary extensions, custom plugins, etc.),
you can use OPAM to install Frama-C's dependencies and compile your
own sources directly: