.git-blame-ignore-revs

+0d64e4bf54395541f410a389be094baf47b7861a
+0fc9094d8a7133f76295955a661fc24f51d276fd
+12caab47125da12c1aaa7a8b5b3af26e5b40fcf6
+166796b37aa9c0bd19da353e62a65dc98d25470b
+1cec870fb83b726a1362a41ef8ebfa71423fc7d8
+2467fec178efe269231972f68e7f2c08fdec122c
+2f10c9d25fc4ca48edce8248a799d1e6164e8a69
+2f69c7d664a5f2069fbb56e392d5a6d4378b75af
+3b6d99bd1c08434fed8f4bb3d6d66a051785980d
+41c3d54cdbb85152a8192c396c7506cd078e3f2f
+4691c9c7b01d6985a36d23166145c137935f28b8
+524e43b632d3f4a6f4ab14393878365e9bf33d37
+54bb4ac66f3e3794d31b8ca9c05b728074dddd0f
+677941ae40e72728ffdb8493fb171d36fe38d239
+705b7c9a8683a2c0314176cccf9afe626be1f13a
+75d9c2de0e8475bb26ea4e21c25525bbcf395bb6
+791ce7463b6891e74fff844ecf53ec398f119c8d
+7a0c12c6d4e02ef72a29267037a61a9efbd4dd87
+7da89554af46f144c8dc6c24abed036d8974eae8
+83f089114760ca1856b06bde724a74efc84b81d6
+89b69ec2c93c9d456f262c04a4cabb7c9ec9d3fe
+91d9f893d08da68a3540da569db954e12106e156
+a194cc7610116743c882a0381c1443ea0b4543e1
+abe63e6907843943f998e1fbd42215fb99fd09ee
+bdb7c0c96007d10e0d0ef64a7de394ed0432acd1
+d36f20d0632d3fabefb48d9d75781a6c59851c15
+dbfeaee3e71ea4b36aa42d7a4e9dd3f54a9696d8
+dda0510ea1384860c002b26bc4986eae1dc60cc8
+e1b60790e0e28fbbd63f20413da3833a1870cc6e
+51657544aea02e55761c6e12b0ec315f9047d5d5
+dc99367c8f4a95d53ec7ce6187892b91fbfd4c1f
+0e05285bd47c752f57c190683608527599fa5afb
+a767fdcb7adda81a5ef192733ef7c62fd56b30e2
+4130bab7a8b59d0c94a22d792b2a7d5a26d3484d
+237d1bc71eb5efb7c5f32a097aacb90f90e0ff73
+6cc1a6f2036b75c6b2451518ffbfbe025eb1a1f8
+1b7754fe7325a59ddbba62842a4bd907b0af6036
+aef808e15e4dcc02dcee7004add8530083d33474
+220072cecdcc0b0b8292c40d93e793b3219b506f
+6ead6d862f1960e6baca64d335b811c954cf8430
+7955ef2039b2010cc30b88da7a47d4f07e298042
+8353ff71c9958169cf27c589b678f183cca63a9c
+fe98b40c209dbe13fdc2069e26c42d4062fda3f0
+de07f8c573ed830b65b5cb343dae4ee7c2c3743d

.gitattributes

+################
+# MERGE: union #
+################
+
+.git-blame-ignore-revs merge=union
+Changelog merge=union
+
+################
+# DISTRIBUTION #
+################
+
+/doc/** export-ignore
+
+##################################################
+# BINARY/CHECK-SYNTAX/INDENT/EOL-EOF: set/-unset #
+##################################################
+
+# note: "binary" is a built-in macro that also
+#       unsets the "text" and "diff" attributes
+
+# note: set "check-eoleof" and "check-utf8" by default to all files
+* check-eoleof check-utf8
+
+# note: unset "-check-eoleof" and "-check-utf8" for "binary"
+*.ico binary -check-eoleof -check-utf8
+*.icns binary -check-eoleof -check-utf8
+
+*.eps binary -check-eoleof -check-utf8
+*.ps  binary -check-eoleof -check-utf8
+*.gif binary -check-eoleof -check-utf8
+*.jpg binary -check-eoleof -check-utf8
+*.png binary -check-eoleof -check-utf8
+*.svg binary -check-eoleof -check-utf8
+
+*.odg binary -check-eoleof -check-utf8
+*.pdf binary -check-eoleof -check-utf8
+
+*.eot binary -check-eoleof -check-utf8
+*.woff binary -check-eoleof -check-utf8
+
+###########################################
+# CHECK-SYNTAX/INDENT/EOL-EOF: set/-unset #
+###########################################
+
+## Set "check-syntax" and "check-indent"
+
+# note: "check-syntax" includes already "check-eoleof"
+*.ml  check-syntax check-indent -check-eoleof
+*.mli check-syntax check-indent -check-eoleof
+*.py  check-indent
+*.c   check-indent
+*.h   check-indent
+
+## Unset "-check-indent"
+
+# Unchecked C files
+
+tests/**/*.[ch] -check-indent
+src/plugins/*/tests/**/*.[ch] -check-indent
+
+doc/aorai/**/*.[ch]  -check-indent
+doc/developer/**/*.[ch] -check-indent
+doc/eva/**/*.[ch] -check-indent
+doc/rte/**/*.[ch] -check-indent
+share/**/*.[ch] -check-indent
+
+src/plugins/wp/doc/**/*.[ch] -check-indent
+src/plugins/e-acsl/doc/**/*.[ch] -check-indent
+src/plugins/e-acsl/examples/**/*.[ch] -check-indent
+
+# Don't check it because it takes too much time
+src/plugins/e-acsl/contrib/libdlmalloc/dlmalloc.[ch] -check-indent
+
+# Unchecked python files
+
+share/analysis-scripts/benchmark_database.py -check-indent
+share/analysis-scripts/summary.py -check-indent
+share/analysis-scripts/results_display.py -check-indent
+src/plugins/e-acsl/examples/ensuresec/**/*.py -check-indent
+
+## Unset "-check-eoleof"
+
+*.dot -check-eoleof
+
+/tests/misc/commands_file.t/comments_and_newlines.txt -check-eoleof
+/tests/spec/unfinished-oneline-acsl-comment.i -check-eoleof
+/doc/developer/check_api/run.oracle -check-eoleof
+
+## Unset "-check-utf8"
+
+## Unset all: "-check-syntax -check-indent -check-eoleof -check-utf8"
+
+#########################
+# HEADER_SPEC: CEA_LGPL #
+#########################
+
+dune-project header_spec=CEA_LGPL
+dune header_spec=CEA_LGPL
+dune-workspace.* header_spec=CEA_LGPL
+
+config* header_spec=CEA_LGPL
+
+makefile* header_spec=CEA_LGPL
+Make* header_spec=CEA_LGPL
+*.mk header_spec=CEA_LGPL
+
+*.c header_spec=CEA_LGPL
+*.h header_spec=CEA_LGPL
+
+*.htm header_spec=CEA_LGPL
+*.html header_spec=CEA_LGPL
+
+*.js header_spec=CEA_LGPL
+
+*.ml header_spec=CEA_LGPL
+*.mli header_spec=CEA_LGPL
+*.mll header_spec=CEA_LGPL
+*.mly header_spec=CEA_LGPL
+
+*.pl header_spec=CEA_LGPL
+
+*.py header_spec=CEA_LGPL
+
+*.rc header_spec=CEA_LGPL
+
+*.sh header_spec=CEA_LGPL
+*.zsh header_spec=CEA_LGPL
+
+*.css header_spec=CEA_LGPL
+
+*.ts header_spec=CEA_LGPL
+*.tsx header_spec=CEA_LGPL
+
+########################
+# HEADER_SPEC: .ignore #
+########################
+
+.gitattributes header_spec=.ignore
+.gitignore header_spec=.ignore
+.gitkeep header_spec=.ignore
+.git-blame-ignore-revs header_spec=.ignore
+
+.merlin header_spec=.ignore
+
+Changelog header_spec=.ignore
+opam header_spec=.ignore
+
+README* header_spec=.ignore
+*.README* header_spec=.ignore
+
+*.dot header_spec=.ignore
+*.fig header_spec=.ignore
+
+*.eps header_spec=.ignore
+*.ps header_spec=.ignore
+
+*.gif header_spec=.ignore
+*.ico header_spec=.ignore
+*.jpg header_spec=.ignore
+*.jpeg header_spec=.ignore
+*.png header_spec=.ignore
+*.svg header_spec=.ignore
+
+*.nix header_spec=.ignore
+/nix/*.patch header_spec=.ignore
+
+*.md header_spec=.ignore
+*.opam header_spec=.ignore
+
+*.pdf header_spec=.ignore
+
+.tex header_spec=.ignore
+*.sty header_spec=.ignore
+*.bib header_spec=.ignore
+
+*.odoc header_spec=.ignore
+
+/.gitlab-ci.yml header_spec=.ignore
+/.mailmap header_spec=.ignore
+/.ocp-indent header_spec=.ignore
+/LICENSE header_spec=.ignore
+/VERSION header_spec=.ignore
+/VERSION_CODENAME header_spec=.ignore
+
+/dev/docker/*.sh header_spec=.ignore
+/dev/docker/Dockerfile header_spec=.ignore
+
+/doc/CC-BY-SA-4.0 header_spec=.ignore
+/doc/CHANGES.obfuscator header_spec=.ignore
+/doc/LICENSE header_spec=.ignore
+/doc/MakeLaTeXModern header_spec=.ignore
+/doc/developer/dune-workspace.bench header_spec=.ignore
+/doc/developer/examples/**/* header_spec=.ignore
+/doc/developer/tutorial/**/* header_spec=.ignore
+/doc/qualification/testing header_spec=.ignore
+/doc/release/periodic-elements.txt header_spec=.ignore
+/doc/eva/watchpoints header_spec=.ignore
+/doc/scope/M.v header_spec=.ignore
+
+/doc/aorai/example/example* header_spec=.ignore
+/doc/frama-c-book.* header_spec=.ignore
+/doc/*.hva header_spec=.ignore
+
+/doc/eva/examples/parametrizing/*.log header_spec=.ignore
+/doc/**/make* header_spec=.ignore
+/doc/**/TODO header_spec=.ignore
+/doc/**/*.bnf header_spec=.ignore
+/doc/**/*.c header_spec=.ignore
+/doc/**/*.graphml header_spec=.ignore
+/doc/**/*.h header_spec=.ignore
+/doc/**/*.html header_spec=.ignore
+/doc/**/*.lua header_spec=.ignore
+/doc/*/*/**/*.ml header_spec=.ignore
+/doc/**/*.mli header_spec=.ignore
+/doc/**/*.mll header_spec=.ignore
+/doc/**/*.oracle header_spec=.ignore
+/doc/**/*.tex header_spec=.ignore
+/doc/*/*/**/*.txt header_spec=.ignore
+/doc/**/*.sh header_spec=.ignore
+
+/headers/open-source/* header_spec=.ignore
+/headers/closed-source/* header_spec=.ignore
+
+/licenses/* header_spec=.ignore
+
+/man/frama-c.1 header_spec=.ignore
+
+/nix/external-plugins.txt header_spec=.ignore
+/nix/ocaml-versions.txt header_spec=.ignore
+/nix/frama-c-public/known_hosts header_spec=.ignore
+/nix/sources.json header_spec=.ignore
+
+/tools/ptests/tests/**/* header_spec=.ignore
+
+/share/framac.vim header_spec=.ignore
+/share/analysis-scripts/readme-graph.graphml header_spec=.ignore
+/share/compliance/*.json header_spec=.ignore
+/share/machdeps/.machdep_*.validated header_spec=.ignore
+/share/machdeps/machdep-schema.yaml header_spec=.ignore
+/share/machdeps/machdep_*.yaml header_spec=.ignore
+/tests/**/* header_spec=.ignore
+
+#######################
+# HEADER_SPEC: others #
+#######################
+
+/doc/aorai/Makefile header_spec=AORAI_LGPL
+
+/share/analysis-scripts/fc-estimate-difficulty.mk header_spec=.ignore
+/share/analysis-scripts/fced-lin.Dockerfile header_spec=.ignore
+/share/analysis-scripts/fced-win.Dockerfile header_spec=.ignore
+/share/analysis-scripts/fced-test/a.c header_spec=.ignore
+/share/analysis-scripts/fced-test/a.h header_spec=.ignore
+/share/analysis-scripts/flamegraph.pl header_spec=CDDL
+/share/emacs/acsl.el header_spec=CEA_PR_LGPL
+/share/libc/argz.h header_spec=CEA_FSF_LGPL
+/share/libc/argz.c header_spec=CEA_FSF_LGPL
+
+/src/kernel_internals/parsing/clexer.mli header_spec=CIL
+/src/kernel_internals/parsing/clexer.mll header_spec=CIL
+/src/kernel_internals/parsing/cparser.mly header_spec=CIL
+/src/kernel_internals/parsing/errorloc.ml header_spec=CIL
+/src/kernel_internals/parsing/errorloc.mli header_spec=CIL
+/src/kernel_internals/parsing/lexerhack.ml header_spec=CIL
+/src/kernel_internals/parsing/lexerhack.mli header_spec=CIL
+/src/kernel_internals/parsing/logic_lexer.mli header_spec=CEA_INRIA_LGPL
+/src/kernel_internals/parsing/logic_lexer.mll header_spec=CEA_INRIA_LGPL
+/src/kernel_internals/parsing/logic_parser.mly header_spec=CEA_INRIA_LGPL
+/src/kernel_internals/parsing/logic_preprocess.mli header_spec=CEA_INRIA_LGPL
+/src/kernel_internals/parsing/logic_preprocess.mll header_spec=CEA_INRIA_LGPL
+/src/kernel_internals/runtime/machdeps.ml header_spec=CIL
+/src/kernel_internals/runtime/machdeps.mli header_spec=CIL
+/src/kernel_internals/typing/alpha.ml header_spec=CIL
+/src/kernel_internals/typing/alpha.mli header_spec=CIL
+/src/kernel_internals/typing/cabs2cil.ml header_spec=CIL
+/src/kernel_internals/typing/cabs2cil.mli header_spec=CIL
+/src/kernel_internals/typing/cfg.ml header_spec=CIL
+/src/kernel_internals/typing/cfg.mli header_spec=CIL
+/src/kernel_internals/typing/frontc.ml header_spec=CIL
+/src/kernel_internals/typing/frontc.mli header_spec=CIL
+/src/kernel_internals/typing/logic_builtin.ml header_spec=CEA_INRIA_LGPL
+/src/kernel_internals/typing/logic_builtin.mli header_spec=CEA_INRIA_LGPL
+/src/kernel_internals/typing/mergecil.ml header_spec=CIL
+/src/kernel_internals/typing/mergecil.mli header_spec=CIL
+/src/kernel_internals/typing/oneret.ml header_spec=CIL
+/src/kernel_internals/typing/oneret.mli header_spec=CIL
+/src/kernel_internals/typing/rmtmps.ml header_spec=CIL
+/src/kernel_internals/typing/rmtmps.mli header_spec=CIL
+/src/kernel_internals/typing/translate_lightweight.ml header_spec=CEA_INRIA_LGPL
+/src/kernel_internals/typing/translate_lightweight.mli header_spec=CEA_INRIA_LGPL
+/src/kernel_services/analysis/dataflows.ml header_spec=CIL
+/src/kernel_services/analysis/dataflows.mli header_spec=CIL
+/src/kernel_services/ast_data/cil_types.mli header_spec=CIL
+/src/kernel_services/ast_data/cil_types.ml header_spec=CIL
+/src/kernel_services/ast_printing/cprint.ml header_spec=CIL
+/src/kernel_services/ast_printing/cprint.mli header_spec=CIL
+/src/kernel_services/ast_printing/logic_print.ml header_spec=CEA_INRIA_LGPL
+/src/kernel_services/ast_printing/logic_print.mli header_spec=CEA_INRIA_LGPL
+/src/kernel_services/ast_queries/cil.ml header_spec=CIL
+/src/kernel_services/ast_queries/cil.mli header_spec=CIL
+/src/kernel_services/ast_queries/cil_builtins.ml header_spec=CIL
+/src/kernel_services/ast_queries/cil_builtins.mli header_spec=CIL
+/src/kernel_services/ast_queries/cil_const.ml header_spec=CIL
+/src/kernel_services/ast_queries/cil_const.mli header_spec=CIL
+/src/kernel_services/ast_queries/logic_const.ml header_spec=CEA_INRIA_LGPL
+/src/kernel_services/ast_queries/logic_const.mli header_spec=CEA_INRIA_LGPL
+/src/kernel_services/ast_queries/logic_env.ml header_spec=CEA_INRIA_LGPL
+/src/kernel_services/ast_queries/logic_env.mli header_spec=CEA_INRIA_LGPL
+/src/kernel_services/ast_queries/logic_typing.ml header_spec=CEA_INRIA_LGPL
+/src/kernel_services/ast_queries/logic_typing.mli header_spec=CEA_INRIA_LGPL
+/src/kernel_services/ast_queries/logic_utils.ml header_spec=CEA_INRIA_LGPL
+/src/kernel_services/ast_queries/logic_utils.mli header_spec=CEA_INRIA_LGPL
+/src/kernel_services/parsetree/cabs.ml header_spec=CIL
+/src/kernel_services/parsetree/cabshelper.ml header_spec=CIL
+/src/kernel_services/parsetree/cabshelper.mli header_spec=CIL
+/src/kernel_services/parsetree/logic_ptree.ml header_spec=CEA_INRIA_LGPL
+/src/kernel_services/visitors/cabsvisit.ml header_spec=CIL
+/src/kernel_services/visitors/cabsvisit.mli header_spec=CIL
+/src/kernel_services/visitors/visitor_behavior.ml header_spec=CEA_INRIA_LGPL
+/src/kernel_services/visitors/visitor_behavior.mli header_spec=CEA_INRIA_LGPL
+
+/src/libraries/datatype/unmarshal.ml header_spec=INRIA_BSD
+/src/libraries/datatype/unmarshal.mli header_spec=INRIA_BSD
+/src/libraries/datatype/tests/unmarshal_hashtbl_test.ml header_spec=INRIA_BSD
+/src/libraries/datatype/tests/unmarshal_test.ml header_spec=INRIA_BSD
+/src/libraries/project/state_topological.ml header_spec=MODIFIED_OCAMLGRAPH
+/src/libraries/project/state_topological.mli header_spec=MODIFIED_OCAMLGRAPH
+/src/libraries/utils/cilconfig.ml header_spec=CIL
+/src/libraries/utils/cilconfig.mli header_spec=CIL
+/src/libraries/utils/escape.ml header_spec=CIL
+/src/libraries/utils/escape.mli header_spec=CIL
+/src/libraries/utils/hptmap.ml header_spec=MODIFIED_MENHIR
+/src/libraries/utils/hptmap.mli header_spec=MODIFIED_MENHIR
+/src/libraries/utils/hptmap_sig.ml header_spec=MODIFIED_MENHIR
+/src/libraries/utils/rangemap.ml header_spec=OCAML_STDLIB
+/src/libraries/utils/rangemap.mli header_spec=OCAML_STDLIB
+/src/libraries/utils/utf8_logic.ml header_spec=CEA_INRIA_LGPL
+/src/libraries/utils/utf8_logic.mli header_spec=CEA_INRIA_LGPL
+
+/tools/lint/UTF8.ml header_spec=MODIFIED_CAMOMILE
+
+#########################
+# HEADER_SPEC: CEA_LGPL #
+#########################
+
+/bin/frama-c* header_spec=CEA_LGPL
+
+/headers/headache_config.txt header_spec=CEA_LGPL
+
+/share/autocomplete_frama-c header_spec=CEA_LGPL
+/share/emacs/frama-c-*.el header_spec=CEA_LGPL
+/share/_frama-c header_spec=CEA_LGPL
+
+/src/kernel_internals/runtime/system_config.ml.in header_spec=CEA_LGPL

.gitignore

+###########
+# General #
+###########
+
+TAGS
+*~
+\#*
+.\#*
+.DS_Store
+*.tmp
+
+#artifacts from execution
+/.frama-c/
+/.merlin
+/bin/ivette
+.ivette
+
+#build
+/_opam/
+/frama-c*.tar.gz
+/distributed
+_build
+*.install
+*.coverage
+_coverage
+_bisect
+
+# This file is generated (on need) during configure
+/src/plugins/dune
+
+#lint
+/.lint/
+
+#tests
+
+/.wp-cache
+/tests/**/result*/
+/tests/**/oracle*/dune
+
+/src/plugins/*/tests/**/result*/
+/src/plugins/*/tests/**/oracle*/dune
+
+/tests/crowbar/*constfold
+/tests/crowbar/integer_bb_pretty
+/tests/crowbar/mutable
+/tests/crowbar/output-*
+/tests/crowbar/test_ghost_cfg
+
+/.test-errors.log
+
+#share
+#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/aorai-example.tar.gz
+/doc/aorai/aorai-example/
+/doc/aorai/frama-c-aorai-example.tar.gz
+/doc/aorai/frama-c-aorai-example
+/doc/aorai/main.pdf
+/doc/aorai/ya_file.tex
+/doc/aorai/basic_ya.tex
+/doc/aorai/extended_ya.tex
+/doc/aorai/ya_variables.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/doxygen
+
+/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/exple-call.c
+/doc/pdg/index.html
+/doc/pdg/logo-inria-sophia.eps
+/doc/pdg/logo-inria-sophia.pdf
+/doc/pdg/next_motif.gif
+/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
+
+/doc/server/
+
+#plugins
+/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
+
+# WP/Coq Generated file
+.lia.cache
+
+# analysis-scripts
+share/analysis-scripts/build
+share/analysis-scripts/fced-dist
+share/analysis-scripts/fced-dist-prepare*
+share/analysis-scripts/fc-estimate-difficulty.*spec
+share/analysis-scripts/fc-estimate-difficulty
+share/analysis-scripts/fc-estimate-difficulty.exe
+share/analysis-scripts/libc_metrics.json
+
+# generated tar.gz files
+
+/doc/developer/hello.tar.gz
+hello-*.tar.gz
+
+# Nix
+
+# When a nix-build is executed it generates
+/result*
+
+#######################
+# should remain empty #
+#######################

.gitlab-ci.yml

+################################################################################
+### STAGES
+
+stages:
+  - prepare
+  - build
+  - tests
+  - distrib
+  - compatibility
+  - release
+  - publish
+
+################################################################################
+### DEFAULT JOB PARAMETERS
+
+default:
+  interruptible: true
+  tags: [ nix-v2 ]
+
+################################################################################
+### VARIABLES
+
+variables:
+  DEFAULT: "master"
+  OCAML: "4.14"
+  OPAM_OPTS: "--with-test --with-doc"
+  NODE: "22"
+  PUBLISH: "no"
+  RELEASE: "no"
+
+################################################################################
+### ONLY/EXCEPT TEMPLATES
+
+.build_template: &manual_when_not_special_pipeline
+  except:
+    refs:
+      - schedules
+    variables:
+      - $RELEASE == "yes"
+  when: manual
+
+.build_template: &when_release
+  only:
+    variables:
+      - $RELEASE == "yes"
+
+.build_template: &when_schedules
+  only:
+    refs:
+      - schedules
+
+.build_template: &when_publish
+  only:
+    variables:
+      - $PUBLISH == "yes"
+
+################################################################################
+### IVETTE SETUP TEMPLATE
+
+.build_template: &ivette_setup
+  image: "ocaml/opam:ubuntu-lts-ocaml-$OCAML"
+  before_script:
+    # Prepare
+    - sudo apt update
+    # TS
+    - sudo apt install -y xvfb curl unzip libnss3 libasound2-plugins
+    - sudo curl -o- https://raw.githubusercontent.com/nvm-sh/nvm/v0.39.7/install.sh | bash
+    - export NVM_DIR="$HOME/.nvm"
+    - . "$NVM_DIR/nvm.sh"
+    - nvm install $NODE
+    - nvm use node $NODE
+    - corepack enable
+    # Opam
+    - opam switch create --empty .
+    - eval $(opam env --switch=. --set-switch)
+    - opam pin . -n -k path
+    - opam depext frama-c
+    - opam install headache
+    - opam install --jobs 2 --deps-only .
+    # Build Frama-C API
+    - dune build -j2 @install
+    - make -C ivette api
+
+################################################################################
+### PREPARE
+
+check-makefile:
+  stage: prepare
+  script:
+    - ./nix/shell-checkers.sh "make --warn-undefined-variables help > /dev/null 2> errors && [[ "$(cat errors)" == "" ]]"
+
+check-no-old-frama-c:
+  stage: prepare
+  script:
+    - (! git merge-base --is-ancestor a1e186c68a6418a53b3dc06237f49e8dcbf75f4a HEAD)
+    - git merge-base --is-ancestor a35d2118fe6999dddce9e1847eff626fae9cc37c HEAD
+
+.build_template: &do_not_stop_pipeline_template
+  stage: prepare
+  interruptible: false
+  script:
+    - echo "This pipeline won't be interrupted"
+
+unstoppable-pipeline:
+  <<: *do_not_stop_pipeline_template
+  only:
+    variables:
+      - $DEFAULT == $CI_COMMIT_BRANCH
+
+do-not-stop-pipeline:
+  <<: *do_not_stop_pipeline_template
+  when: manual
+  except:
+    variables:
+      - $DEFAULT == $CI_COMMIT_BRANCH
+
+check-publish:
+  stage: prepare
+  script: >
+    [[ "$RELEASE" == "no" ]] &&
+    [[ "$DEFAULT" == "$CI_COMMIT_BRANCH" ]] &&
+    [[ "$DEFAULT" == "master" ]]
+  <<: *when_publish
+
+check-release:
+  stage: prepare
+  script:
+    - ./nix/frama-c-public/check-release.sh
+  <<: *when_release
+
+# Observed: when several shell with same dependencies are started, deadlock may
+#           occur when building these dependencies. We build these dependencies
+#           before running the rest of the pipeline to avoid that.
+prepare-shell-checkers:
+  stage: prepare
+  script:
+    - ./nix/shell-checkers.sh "true"
+
+prepare-wp-cache:
+  stage: prepare
+  script:
+    - ./nix/wp-cache.nix.sh
+  artifacts:
+    paths:
+      - ./nix/wp-cache.nix
+
+################################################################################
+### BUILD
+
+frama-c:
+  stage: build
+  script:
+    - ./nix/build-proxy.sh frama-c
+  artifacts:
+    when: on_failure
+    paths:
+      - commits.nix
+      - results.log
+    expire_in: 1 day
+
+ivette:
+  stage: build
+  <<: *ivette_setup
+  script:
+    - make -C ivette check-lint
+    - make -C ivette dist
+  tags:
+    - docker
+
+################################################################################
+### TESTS
+
+.build_template: &coverage_artifacts
+  artifacts:
+    name: coverage-$CI_JOB_NAME
+    paths:
+      - _bisect/*.tar.xz
+    expire_in: 24h
+
+.build_template: &coverage
+  variables:
+    OUT: "_bisect"
+  <<: *coverage_artifacts
+
+e-acsl-tests:
+  stage: tests
+  script:
+    - ./nix/build-proxy.sh e-acsl-tests
+  <<: *coverage
+
+.build_template: &eva_template
+  stage: tests
+  script:
+    - ./nix/build-proxy.sh eva-$CONFIG-tests
+  <<: *coverage_artifacts
+  # Do not add OUT here, the parallel rule in Eva domains overload variables
+
+eva-default-tests:
+  variables:
+    CONFIG: "default"
+    OUT:    "_bisect"
+  <<: *eva_template
+
+.build_template: &eva_domains
+  parallel:
+    matrix:
+      - OUT: "_bisect"
+        CONFIG: [
+          "apron",
+          "bitwise",
+          "equality",
+          "gauges",
+          "multidim",
+          "octagon",
+          "symblocs"
+        ]
+
+eva-domains:
+  <<: *eva_template
+  <<: *eva_domains
+
+kernel-tests:
+  stage: tests
+  script:
+    - ./nix/build-proxy.sh kernel-tests
+  <<: *coverage
+
+plugins-tests:
+  stage: tests
+  script:
+    - ./nix/build-proxy.sh plugins-tests
+  <<: *coverage
+
+wp-tests:
+  stage: tests
+  script:
+    - ./nix/build-proxy.sh wp-tests
+  <<: *coverage
+
+ivette-tests:
+  stage: tests
+  when: manual
+  <<: *ivette_setup
+  script:
+    - make -C ivette dist
+    - cd ivette
+    - xvfb-run --auto-servernum -e /dev/stdout -s "-screen 0 1920x1080x24 -ac -nolisten tcp -nolisten unix" dune exec -- yarn playwright test --headed
+  artifacts:
+    paths:
+      - ivette/tests/test-results
+      - ivette/screenshots
+    when: always
+    expire_in: 1 day
+  tags:
+    - docker
+
+external-plugins:
+  stage: tests
+  script:
+    - ./nix/external-plugin-ci.sh $PLUGIN
+  parallel:
+    matrix:
+      - PLUGIN: [
+          "acsl-importer",
+          "caveat-importer",
+          "context-from-precondition",
+          "frama-clang",
+          "genassigns",
+          "meta",
+          "minimal",
+          "pathcrawler",
+          "security",
+          "volatile"
+        ]
+
+################################################################################
+### DISTRIB
+
+# API documentation
+
+api-doc:
+  stage: distrib
+  variables:
+    OUT: "api"
+  script:
+    - ./nix/build-proxy.sh api-doc
+  artifacts:
+    paths:
+      - api/frama-c-api.tar.gz
+      - api/frama-c-server-api.tar.gz
+    expire_in: 7 days
+
+api-json-doc:
+  stage: distrib
+  variables:
+    OUT: "api"
+  script:
+    - ./nix/build-proxy.sh api-json-doc
+  artifacts:
+    paths:
+      - api/frama-c-api-json.tar.gz
+    expire_in: 7 days
+
+# Build distribution tarball
+
+build-distrib-tarball:
+  stage: distrib
+  variables:
+    OPEN_SOURCE: "yes"
+    CI_LINK: "yes"
+    HDRCK: "frama-c-hdrck"
+  script:
+    - ./nix/shell-checkers.sh "./dev/make-distrib.sh"
+  artifacts:
+    paths:
+      - ./*.tar.gz
+    expire_in: 1 week
+
+# Build ivette apps
+
+.build_template: &ivette_linux_build_template
+  stage: distrib
+  <<: *ivette_setup
+  script:
+    - make -C ivette dist-linux
+    - mv ivette/dist/Ivette-arm64.AppImage ./frama-c-ivette-linux-ARM64.AppImage
+    - mv ivette/dist/Ivette-x86_64.AppImage ./frama-c-ivette-linux-x86-64.AppImage
+  artifacts:
+    paths:
+      - ./*.AppImage
+  tags:
+    - docker
+
+build-ivette-linux-packages:
+  <<: *ivette_linux_build_template
+  <<: *manual_when_not_special_pipeline
+
+build-ivette-linux-packages-release:
+  <<: *ivette_linux_build_template
+  <<: *when_release
+
+.build_template: &ivette_macos_build_template
+  stage: distrib
+  script:
+    # TS
+    - export NVM_DIR="$HOME/.nvm"
+    - . "$NVM_DIR/nvm.sh"
+    - nvm install $NODE
+    - nvm use $NODE
+    - corepack enable
+    # Opam
+    - opam switch create --empty .
+    - eval $(opam env --switch=. --set-switch)
+    - opam pin . -n -k path
+    - opam install headache -y
+    - opam install --jobs 2 --deps-only . -y
+    # Build Frama-C API
+    - dune build -j2 @install
+    - make -C ivette api
+    # Build Ivette
+    - make -C ivette dist-macOS
+    - mv ivette/dist/Ivette-universal.dmg ./frama-c-ivette-macos-universal.dmg
+  artifacts:
+    paths:
+      - ./*.dmg
+  tags:
+    - macos-arm
+
+build-ivette-macos-packages:
+  <<: *ivette_macos_build_template
+  <<: *manual_when_not_special_pipeline
+
+build-ivette-macos-packages-release:
+  <<: *ivette_macos_build_template
+  <<: *when_release
+
+# Coverage
+
+coverage:
+  stage: distrib
+  variables:
+    BISECT_DIR: "_bisect"
+  script:
+    - ./nix/shell-checkers.sh "./nix/coverage.sh"
+  coverage: '/Coverage: \d+\.\d+\%/'
+  artifacts:
+    reports:
+      coverage_report:
+        coverage_format: cobertura
+        path: report.xml
+    expire_in: 1 week
+
+# Check files header
+
+header-check:
+  stage: distrib
+  script:
+    - ./nix/shell-checkers.sh "make -f share/Makefile.headers check-headers"
+
+# Lint files
+
+lint:
+  stage: distrib
+  script:
+    - ./nix/shell-checkers.sh "make -f share/Makefile.linting check-lint LINTCK_EXTRA=-s"
+
+# Manuals
+
+.build_template: &manuals_build_template
+  stage: distrib
+  variables:
+    OUT: "manuals"
+  script:
+    - ./nix/build-proxy.sh manuals
+
+.build_template: &manuals_artifacts_template
+  artifacts:
+    paths:
+      - manuals/*.pdf
+      - manuals/*.tar.gz
+      - manuals/*.txt
+    expire_in: 7 days # Note: the LAST artifact of the ref is always kept
+
+manuals:
+  <<: *manuals_build_template
+
+manuals-artifacts:
+  <<: *manuals_build_template
+  <<: *manuals_artifacts_template
+  <<: *manual_when_not_special_pipeline
+
+manuals-nightly:
+  <<: *manuals_build_template
+  <<: *manuals_artifacts_template
+  <<: *when_publish
+
+manuals-for-release:
+  <<: *manuals_build_template
+  <<: *manuals_artifacts_template
+  <<: *when_release
+
+# Release artifacts
+
+release-content:
+  stage: distrib
+  script:
+    - ./nix/shell-checkers.sh "./dev/build-release.sh"
+  needs:
+    - api-doc
+    - build-distrib-tarball
+    - build-ivette-linux-packages-release
+    - build-ivette-macos-packages-release
+    - manuals-for-release
+  artifacts:
+    paths:
+      - website
+      - wiki
+      - opam-repository
+      - release-data.json
+  <<: *when_release
+
+################################################################################
+### COMPATIBILITY
+
+# Internalized plugins tests
+
+.build_template: &internal_template
+  stage: compatibility
+  script:
+    - ./nix/internal-tests.sh
+
+internal:
+  <<: *internal_template
+  when: manual
+  except:
+    - schedules
+
+internal-nightly:
+  <<: *internal_template
+  # The Opam target may affect this job
+  timeout: 2h
+  only:
+    - schedules
+
+# Linux ARM & MacOS
+
+.build_template: &additional_arch_template
+  stage: compatibility
+  script:
+    - opam update
+    - opam switch create --empty .
+    - eval $(opam env --switch=. --set-switch)
+    # Note: we use this to get an exact version corresponding to a minor version
+    - opam pin add ocaml $(grep $OCAML nix/ocaml-versions.txt) -n
+    - opam install . --deps-only --with-test -y
+    - dune build @install
+    - dune exec -- frama-c-ptests tests src/plugins/*/tests
+    - dune build @ptests_config
+  timeout: 2h
+  tags:
+    - ${ARCH}
+
+additional-arch:
+  <<: *additional_arch_template
+  <<: *manual_when_not_special_pipeline
+  parallel:
+    matrix:
+      - ARCH: [linux-arm, macos-x86, macos-arm]
+
+additional-arch-nightly:
+  <<: *additional_arch_template
+  <<: *when_publish
+  parallel:
+    matrix:
+      - ARCH: [linux-arm, macos-x86, macos-arm]
+
+additional-arch-release:
+  <<: *additional_arch_template
+  <<: *when_release
+  parallel:
+    matrix:
+      - ARCH: [linux-arm, macos-x86, macos-arm]
+
+# OCaml versions
+
+.build_template: &ocaml_always_additional_versions_template
+  parallel:
+    matrix:
+      - OCAML: ["5.3"]
+
+# Uncomment this block when there are intermediate versions to check manually
+# Beware that some targets may fail if the target job does not provide the
+# version (for example Opam provide version N but Nix does not)
+.build_template: &ocaml_manual_additional_versions_template
+  parallel:
+    matrix:
+      - OCAML: ["5.1", "5.2"]
+  when: manual
+
+.build_template: &ocaml_versions_template
+  stage: compatibility
+  script:
+    - ./nix/build-proxy.sh default-config-tests
+
+ocaml-versions:
+  <<: *ocaml_versions_template
+  <<: *ocaml_always_additional_versions_template
+  # in schedules, each OCAML is tested in its own complete pipeline
+  except:
+    - schedules
+
+# Uncomment this section when there are additional versions of OCaml to test
+ocaml-versions-more:
+  <<: *ocaml_versions_template
+  <<: *ocaml_manual_additional_versions_template
+
+ocaml-versions-nightly:
+  <<: *ocaml_versions_template
+  <<: *ocaml_always_additional_versions_template
+  # in publish schedule, we still check additional versions of OCaml
+  <<: *when_publish
+
+# Opam pin
+
+.build_template: &opam_pin_template
+  stage: compatibility
+  image: 'ocaml/opam:ubuntu-20.04-ocaml-$OCAML'
+  script:
+    - sudo ln -f /usr/bin/opam-2.1 /usr/bin/opam
+    - opam init --reinit -ni
+    - sudo apt update
+    - opam pin . -n -k path
+    - opam install --jobs 2 frama-c $OPAM_OPTS
+    - frama-c --plugins
+  tags:
+    - docker
+
+opam-pin:
+  <<: *opam_pin_template
+  <<: *manual_when_not_special_pipeline
+
+opam-pin-manual:
+  <<: *opam_pin_template
+  <<: *ocaml_manual_additional_versions_template
+
+opam-pin-nightly:
+  <<: *opam_pin_template
+  <<: *when_schedules
+
+opam-pin-release:
+  <<: *opam_pin_template
+  <<: *when_release
+
+.build_template: &opam_pin_minimal_template
+  stage: compatibility
+  image: 'ocaml/opam:ubuntu-20.04-ocaml-$OCAML'
+  variables:
+    OPAMDOWNLOADJOBS: "1"
+    OPAMERRLOGLEN: "0"
+    OPAMSOLVERTIMEOUT: "500"
+    OPAMPRECISETRACKING: "1"
+  script:
+    - sudo ln -f /usr/bin/opam-2.1 /usr/bin/opam
+    - opam --version
+    - opam init --reinit -ni
+    - sudo apt update
+    - export OPAMCRITERIA="-removed,-count[avoid-version,changed],-count[version-lag,request],-count[version-lag,changed],-count[missing-depexts,changed],-changed"
+    - export OPAMFIXUPCRITERIA="-removed,-count[avoid-version,changed],-count[version-lag,request],-count[version-lag,changed],-count[missing-depexts,changed],-changed"
+    - export OPAMUPGRADECRITERIA="-removed,-count[avoid-version,changed],-count[version-lag,request],-count[version-lag,changed],-count[missing-depexts,changed],-changed"
+    - opam pin . -n -k path
+    - opam update --depexts
+    - opam depext --jobs 2 frama-c
+    - export OPAMCRITERIA="+removed,+count[version-lag,solution]"
+    - export OPAMFIXUPCRITERIA="+removed,+count[version-lag,solution]"
+    - export OPAMUPGRADECRITERIA="+removed,+count[version-lag,solution]"
+    - export OPAMEXTERNALSOLVER="builtin-0install"
+    - opam update --depexts
+    - opam reinstall --jobs 2 frama-c
+    - frama-c --plugins
+  timeout: 2h
+  tags:
+    - docker
+
+opam-pin-minimal:
+  <<: *opam_pin_minimal_template
+  <<: *manual_when_not_special_pipeline
+
+opam-pin-minimal-nightly:
+  <<: *opam_pin_minimal_template
+  <<: *when_schedules
+
+opam-pin-minimal-release:
+  <<: *opam_pin_minimal_template
+  <<: *when_release
+
+# Distrib
+
+.build_template: &src_distrib_tests_template
+  stage: compatibility
+  variables:
+    DIR: "extracted"
+  script:
+    - mkdir $DIR && tar -xzf frama-c.tar.gz --strip-components 1 -C ./extracted
+    - ./nix/build-proxy.sh src-distrib-tests
+  # The Opam target may affect this job
+  timeout: 2h
+
+src-distrib-tests:
+  <<: *src_distrib_tests_template
+  <<: *manual_when_not_special_pipeline
+
+src-distrib-tests-scheduled:
+  <<: *src_distrib_tests_template
+  <<: *when_schedules
+
+src-distrib-tests-release:
+  <<: *src_distrib_tests_template
+  <<: *when_release
+
+################################################################################
+### RELEASE
+
+.build_template: &prepare_ssh_template
+  before_script:
+    - export GIT_SSH=$PWD/nix/frama-c-public/ssh.sh
+
+release-branch:
+  stage: release
+  variables:
+    REPOSITORY: "frama-c"
+  <<: *prepare_ssh_template
+  script:
+    - (! git merge-base --is-ancestor a1e186c68a6418a53b3dc06237f49e8dcbf75f4a origin/$CI_COMMIT_BRANCH)
+    - BRANCH="$CI_COMMIT_BRANCH" nix-shell -p coreutils openssh --run './nix/frama-c-public/publish-branch.sh'
+    # Note: BRANCH must be defined here, since we cannot *evaluate* a variable in 'variables'
+  <<: *when_release
+  when: manual
+  interruptible: false
+
+release-create:
+  stage: release
+  <<: *prepare_ssh_template
+  script:
+    - nix-shell -p git git-lfs coreutils openssh curl --run './nix/frama-c-public/publish-release.sh'
+  needs:
+    - release-branch
+    - release-content
+  <<: *when_release
+  when: manual
+  interruptible: false
+
+release-opam:
+  stage: release
+  <<: *prepare_ssh_template
+  script:
+    - nix-shell -p git git-lfs coreutils openssh --run './nix/frama-c-public/publish-opam.sh'
+  <<: *when_release
+  interruptible: false
+
+release-website:
+  stage: release
+  <<: *prepare_ssh_template
+  script:
+    - nix-shell -p git git-lfs coreutils openssh --run './nix/frama-c-public/publish-website.sh'
+  <<: *when_release
+  interruptible: false
+
+release-wiki:
+  stage: release
+  <<: *prepare_ssh_template
+  script:
+    - nix-shell -p git git-lfs coreutils openssh --run './nix/frama-c-public/publish-wiki.sh'
+  <<: *when_release
+  interruptible: false
+
+################################################################################
+### PUBLISH
+
+# publish stage is used to push the current master branch of Frama-C and
+# associated plugins from the internal frama-c group to the public pub group.
+#
+# For that, it uses the 'frama-c to frama-c-public' publish key. Thus, to publish
+# a new plugin (while keeping its main repository internal), you can add a new
+# target to this stage, adapting the script for MetAcsl or Frama-Clang to your
+# own plugin.
+#
+# You must also activate the publish key on both frama-c/my_plugin
+# and pub/my_plugin repositories (the former should be read-only, the latter
+# must provide write access to the publish key).
+# Do not forget to trigger the target only on schedules, so that all public
+# repositories stay synchronized.
+
+publish-frama-c:
+  stage: publish
+  variables:
+    BRANCH: "master"
+    REPOSITORY: "frama-c"
+  <<: *prepare_ssh_template
+  script:
+    - (! git merge-base --is-ancestor a1e186c68a6418a53b3dc06237f49e8dcbf75f4a origin/master)
+    -  nix-shell -p coreutils openssh --run './nix/frama-c-public/publish-branch.sh'
+  <<: *when_publish
+  interruptible: false
+
+publish-fclang:
+  stage: publish
+  variables:
+    BRANCH: "master"
+    REPOSITORY: "frama-clang"
+  <<: *prepare_ssh_template
+  script:
+    - nix-shell -p coreutils openssh --run './nix/frama-c-public/publish-branch.sh'
+  <<: *when_publish
+  interruptible: false
+
+publish-meta:
+  stage: publish
+  variables:
+    BRANCH: "master"
+    REPOSITORY: "meta"
+  <<: *prepare_ssh_template
+  script:
+    - nix-shell -p coreutils openssh --run './nix/frama-c-public/publish-branch.sh'
+  <<: *when_publish
+  interruptible: false
+
+publish-frama-c-api:
+  stage: publish
+  <<: *prepare_ssh_template
+  script:
+    - nix-shell -p coreutils openssh --run './nix/frama-c-public/publish-api.sh'
+  only:
+    variables:
+      - $PUBLISH == "yes"
+  interruptible: false

.gitlab/issue_templates/bug_report.md

+<!--
+Thank you for submitting an issue to the Frama-C team.
+We propose the following template to ease the process.
+Please directly edit it inline to provide the required information.
+
+Before submitting the issue, please verify:
+- the issue has not yet been reported on [Gitlab](https://git.frama-c.com/pub/frama-c/issues);
+- you installed Frama-C as prescribed in the [instructions](INSTALL.md).
+
+If the issue applies to a specific Frama-C plug-in, please prefix the title
+by the plug-in name: [Eva], [WP], [E-ACSL]…
+-->
+
+### Steps to reproduce the issue
+
+<!--
+Please indicate here steps to follow to get a [minimal, complete, and verifiable example](https://stackoverflow.com/help/mcve) which reproduces the issue.
+-->
+
+### Expected behaviour
+
+<!--
+Please explain here what is the expected behaviour.
+-->
+
+### Actual behaviour
+
+<!--
+Please explain here what is the actual (faulty) behaviour.
+-->
+
+### Contextual information
+
+- Frama-C installation mode: *Opam, Homebrew, package from distribution, from source, ...*
+- Frama-C version: *Frama-C version* (as reported by `frama-c -version`)
+- Plug-in used: *Plug-in used*
+- OS name: *OS name*
+- OS version: *OS version*
+
+### Additional information (optional)
+
+<!--
+You may add here any information deemed relevant with regard to this issue,
+and tell us if you already tried some workarounds or have some ideas to solve this issue.
+-->

.gitlab/merge_request_templates/external_contribution.md

+Thank you for submitting a merge request to the Frama-C team.
+We propose the following template to ease the process.
+Please directly edit it inline to provide the required information.
+
+Before submitting the merge request, please confirm (by adding a X in the [ ]):
+
+- [ ] you contributed to Frama-C as prescribed in the [instructions](CONTRIBUTING.md).
+- [ ] if the size of the PR requires it, you have signed the
+  [Contributor Licensing Agreement](CLA.md)

.gitlab/merge_request_templates/merge-request.md

+<!-- Please use the syntax frama-c/frama-c, else it might close unrelated
+     public issues
+-->
+Close frama-c/frama-c#NNNN
+
+## Description
+
+Your description here
+
+## Companion MRs
+
+No external plug-in impacted
+
+<!--
+- Plugin: link to MR
+-->
+
+## Tasks
+
+- [ ] API documentation is up-to-date, or no need to update
+- [ ] Manuals are up-to-date (and the CI manuals target has been run), or no
+      need to update (including ACSL manual)
+- [ ] Opam dependencies versions are up-to-date (and CI Opam targets have been
+      run), or no changes
+
+## Proposed Changelog Entry
+
+<!-- Only if needed. The list of changes that warrant a Changelog entry is not completely fixed, but includes at least
+  - Bug fix on pub/frama-c (use `##nnnn` to refer to the issue)
+  - Modification that is visible to the end-user
+  - API change, notably function deprecation
+
+   See [Changelog](https://git.frama-c.com/frama-c/frama-c/-/blob/master/Changelog) for how to format an entry. 
+-->

.mailmap

+#
+# 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>

.ocp-indent

+normal

ACKNOWLEDGEMENTS.md

+# Acknowledgements
+
+The development of Frama-C has been fuelled by many collaborative projects,
+notably at French and European level. Below is a list of the most important
+ones
+
+## European projects
+
+- [SecOPERA](https://www.secopera.eu) (2023-2025)
+- [Medsecurance](https://www.medsecurance.org/) (2023-2025)
+- [EnsureSec](https://www.ensuresec.eu/index.html) (2020-2022)
+- [Sparta](https://www.sparta.eu/) (2019-2022)
+- [Decoder](https://www.decoder-project.eu) (2019-2022)
+- [Vessedia](https://cordis.europa.eu/project/id/731453) (2017-2020)
+- [Stance](https://cordis.europa.eu/project/id/317753) (2012-2016)
+
+## French projects
+
+### ANR
+
+- [OptiTrust](https://anr.fr/Projet-ANR-22-CE25-0017) (2022-2026)
+- [CoMeMov](https://anr.fr/Project-ANR-22-CE25-0018) (2022-2025)
+- [U3CAT](https://www.frama-c.com/u3cat/) (2009-2012)
+- [Device-Soft](https://anr.fr/Project-ANR-09-CARN-0006) (2009-2011)
+- [CAT](https://anr.fr/Projet-ANR-05-RNTL-0003) (2006-2009)
+
+### PEPR
+
+- [SecurEval](https://www.pepr-secureval.com/) (2022-2027)
+
+### Others
+
+- [LEIA](https://list.cea.fr/fr/21-septembre-2021-leia-automatise-lanalyse-logicielle-pour-garantir-la-securite-des-objets-connectes/) (2021-2022)
+- [INGOPCS](https://www.s2opc.com/ingopcs/) (2016-2018)
+- [Hi-Lite](https://www.open-do.org/projects/hi-lite/index.html) (2010-2013)

CLA.md

+---
+geometry:
+- top=15mm
+- bottom=15mm
+- margin=10mm
+---
+Contributor Agreement
+=====================
+
+Thank you for your interest in contributing to Frama-C, distributed by
+the Commissariat à l'Energie Atomique et aux Energies Alternatives
+(\"We\" or \"Us\").
+
+The purpose of this Contributor Non-Exclusive License Agreement
+(\"Agreement\") is to clarify and document the rights granted by
+contributors to Us. To make this document effective and get started,
+please sign the Contributor License Agreement.
+
+Please read this document carefully before signing and keep a copy for
+your records.
+
+**1. DEFINITIONS**
+
+**\"You\" (/"Your")** means the Individual Copyright owner or Entity as
+defined hereunder who submits a Contribution to Us. If You are an
+employee and submit the Contribution as part of your employment, You
+represent that you have the authority and/or required authorization in
+binding the Entity to this Agreement, and to sign this version of this
+document. In such case "You" (/"Yours") shall refer to such Entity.
+
+**\"Documentation\"** means any non-software portion of a Contribution.
+
+**"Entity"** shall mean the copyright owner or legal entity (including
+but not limited to any institution, company, corporation, partnership,
+government agency or university) authorized by the copyright owner that
+is making this Agreement with Us and all other entities that control,
+are controlled by, or are under common control with that entity are
+considered to be a single Contributor. For the purposes of this
+definition, \"control\" means (i) the power, direct or indirect, to
+cause the direction or management of such entity, whether by contract or
+otherwise, or (ii) ownership of fifty percent (50%) or more of the
+outstanding shares, or (iii) beneficial ownership of such entity.
+
+**\"Contribution\"** means any original work of authorship (software
+and/or documentation) including any modifications or additions to an
+existing work, Submitted by You to Us, in which You own the Copyright.
+
+**\"Copyright\"** means all rights protecting works of authorship owned
+or controlled by You, including copyright, moral and neighboring rights,
+as appropriate, for the full term of their existence including any
+extensions by You.
+
+**\"Submit\"** means any form of physical, electronic, or written
+communication sent to Us, including but not limited to electronic
+mailing, source code control systems, and issue tracking systems that
+are managed by, or on behalf of, Us, but excluding communication that is
+clearly designated in writing by You as \"Not a Contribution.\"
+
+\"**Work**\" means any software or documentation made available by Us to
+third parties. Any Contribution You Submit may be included in the
+Material.
+
+**2. GRANT OF LICENSE**
+
+> **2.1 Grant of Copyright License.**
+
+Subject to the terms and conditions of this Agreement, You hereby grant
+to Us a worldwide, royalty-free, no-charge, non-exclusive, perpetual and
+irrevocable Copyright license, with the right to transfer an unlimited
+number of non-exclusive licenses or to grant non-exclusive sublicenses
+to third parties, to use the Contribution by all means, including but
+not limited to, the right to :
+
+-   Publish the Contribution in original or modified form ;
+
+-   Modify the Contribution, prepare derivative works based upon or
+    containing the Contribution and combine the Contribution with other
+    works;
+
+-   Reproduce the Contribution in original or modified form;
+
+-   Distribute, make the Contribution available to the public, display
+    and publicly perform the Contribution in original or modified form
+    under the terms of any license approved by Us.
+
+> **2.2 Moral Rights**
+
+Moral Rights remain unaffected to the extent they are recognized and not
+waivable by applicable law. Notwithstanding, You may add your name in
+the header of the source code files of Your Contribution and We will
+respect this attribution when using Your Contribution.
+
+**3. GRANT OF PATENT LICENSE**
+
+Subject to the terms and conditions of this Agreement, You hereby grant
+to Us a perpetual, worldwide, non-exclusive, no-charge, royalty-free,
+irrevocable patent license, with the right to transfer an unlimited
+number of non-exclusive licenses or to grant sublicenses to third
+parties, to make, have made, use, offer to sell, sell, import, and
+otherwise transfer the Contribution, where such license applies only to
+those patent claims licensable by You that are necessarily infringed by
+Your Contribution(s) alone or by combination of Your Contribution(s)
+with the Work to which such Contribution(s) was submitted.
+
+This license applies to all patents owned or controlled by You, whether
+already acquired or hereafter acquired, that would be infringed by
+making, having made, using, selling, offering for sale, importing or
+otherwise transferring of Your Contribution(s) alone or by combination
+of Your Contribution(s) with the Material.
+
+You furthermore agree to notify Us of any patents that you know or come
+to know which are likely infringed by the Contribution and/or are not
+licensable by You.
+
+If any entity institutes patent litigation against You or any other
+entity alleging that the Contribution, or the Work with which it has
+been combined, constitutes direct or contributory patent infringement,
+then any patent licenses granted to that entity under this Agreement for
+that Contribution or Material shall terminate as of the date such
+litigation is filed.
+
+If the litigation is withdrawn or otherwise settled, then any patent
+licenses granted to that entity under this agreement shall be reinstated
+as of the date the litigation was settled or withdrawn.
+
+**4. REPRESENTATIONS**
+
+a\. If You are entering this Agreement as an individual, You represent
+that You are legally entitled to grant the licenses set forth in
+Sections 2 and 3. If Your employer(s) has rights to intellectual
+property that You create, such as your Contributions, You represent that
+You have received permission to make Contributions on behalf of that
+employer and that Your employer has waived such rights for Your
+Contributions to the Work.
+
+b\. If You are entering this Agreement on behalf of an Entity, You
+represent that You are legally entitled to grant the licenses set forth
+in Sections 2 and 3 and that each employee of the Entity that submits
+Contributions is authorized to submit such Contributions on behalf of
+the Entity.
+
+In any case, You represent that:
+
+i\. The Contribution is Your original creation. If You do not, entirely
+or partially, own the Copyright in work of authorship comprising a
+Contribution, please contact Us before Submitting such Contribution.
+
+ii\. to the extent that Your Contribution is computer code, it includes
+complete details of any third-party license or other restriction
+(including, but not limited to, related patents and trademarks) of which
+You are personally aware and which are associated with any part of Your
+Contributions.
+
+iii\. to the extent that Your Contribution is computer code, it contains
+no viruses, Trojan horses, backdoors, malicious code or other program
+that would allow anyone, including Us, to gain access to a computer or
+network other than what is fully documented and disclosed by Us.
+
+**5. DISCLAIMER OF WARRANTIES**
+
+Except as set forth in section 4, the contribution is provided \"as
+is\". More particularly, all express or implied warranties including,
+without limitation, any implied warranty of merchantability, fitness for
+a particular purpose and non-infringement are expressly disclaimed by
+You to Us and by Us to You. To the extent that any such warranties
+cannot be disclaimed, such warranty is limited in duration to the
+minimum period permitted by law.
+
+**6. CONSEQUENTIAL, APPROXIMATION OF DISCLAIMER AND DAMAGE WAIVER**
+
+To the maximum extent permitted by applicable law, in no event will You
+or Us be liable for any loss of profits, loss of anticipated savings,
+loss of data, indirect, special, incidental, consequential and exemplary
+damages arising out of this Agreement regardless of the legal or
+equitable theory (contract, tort or otherwise) upon which the claim is
+based.
+
+If the disclaimer and damage waiver mentioned in section 5 and section 6
+cannot be given legal effect under applicable local law, reviewing
+courts shall apply local law that most closely approximates an absolute
+waiver of all civil liability in connection with the contribution.
+
+**7. TERM**
+
+This Agreement shall come into effect upon Your acceptance of the terms
+and conditions.
+
+In the event of a termination of this Agreement Sections 5, 6 and 8
+shall survive such termination and shall remain in full force
+thereafter. For the avoidance of doubt, Contributions that are already
+licensed under a free and open source license at the date of the
+termination shall remain in full force after the termination of this
+Agreement.
+
+**8. MISCELLANEOUS**
+
+8.1 You are not expected to provide support for Your Contributions,
+except to the extent You desire to provide support. You may provide
+support for free, for a fee, or not at all. Unless required by
+applicable law or agreed to in writing, You provide Your Contributions
+on an \"as is\" basis, without warranties or conditions of any kind,
+either express or implied, including, without limitation, any warranties
+or conditions of title, non-infringement, merchantability, or fitness
+for a particular purpose.
+
+8.2 This Agreement and all disputes, claims, actions, suits or other
+proceedings arising out of this agreement or relating in any way to it
+shall be governed by the laws of France excluding its private
+international law provisions.
+
+8.3 This Agreement sets out the entire agreement between You and Us for
+Your Contributions to Us and overrides all other agreements or
+understandings.
+
+8.4 If any provision of this Agreement is found void and unenforceable,
+such provision will be replaced to the extent possible with a provision
+that comes closest to the meaning of the original provision and that is
+enforceable. The terms and conditions set forth in this Agreement shall
+apply notwithstanding any failure of essential purpose of this Agreement
+or any limited remedy to the maximum extent possible under law.
+
+8.5 You agree to notify Us of any facts or circumstances of which you
+become aware that would make this Agreement inaccurate in any respect.
+
+**Signature**
+
+- Full Name:
+- Entity (if applicable):
+- Country/Town:
+- (optional) Full address:
+- Email:
+- Gitlab login:
+- Date:
+- Signature:

CONTRIBUTING.md

+Contributing to Frama-C
+=======================
+
+We always welcome technical as well as non-technical contributions from the
+community.
+There are several ways to participate in the Frama-C project:
+
+- Asking questions and discussing at
+  [StackOverflow](https://stackoverflow.com/tags/frama-c) and through
+  the
+  [Frama-C-discuss mailing list](https://groupes.renater.fr/sympa/info/frama-c-discuss);
+
+- Reporting bugs via
+  [Gitlab issues](https://git.frama-c.com/pub/frama-c/issues);
+
+- [Submitting bug fixes, improvements and features](#submitting-bug-fixes-improvements-and-features)
+  via Gitlab merge requests;
+
+- [Developing external plug-ins](#developing-external-plug-ins)
+  and sharing it with us through a Gitlab merge request;
+
+- [Joining the Frama-C team](https://frama-c.com/html/jobs.html) (as an intern, a PhD
+  student, a postdoctoral researcher, or a research engineer).
+
+We give below some guidelines in order to ease the submission of a merge request
+and optimize its integration with the Frama-C existing codebase.
+
+
+Submitting bug fixes, improvements, and features
+================================================
+
+External contributions can be proposed via the
+public Frama-C gitlab [repository](https://git.frama-c.com/pub/frama-c),
+by following the recommended workflow in git development:
+fork the frama-c repository, develop in a dedicated branch
+and submit a merge request.
+
+Note: these steps assume that you have an account in Frama-C's Gitlab instance.
+This can be done by signing in via Github (which, in turn, requires a Github
+account; if you do not have a Github account, please contact us by e-mail).
+
+The detailed steps to submit a contribution to Frama-C are:
+
+1. If you plan to make a significant contribution to Frama-C, please
+  [open an issue](https://git.frama-c.com/pub/frama-c/issues/new)
+  describing your ideas, to discuss it with the Frama-C development team.
+
+2. [Fork the public Frama-C repository](https://git.frama-c.com/pub/frama-c/-/forks/new)
+  (choosing your Gitlab account as a destination);
+
+3. Clone the forked Frama-C repository on your computer;
+
+4. Create and switch to a dedicated branch. We suggest the following
+   naming convention:
+   - `fix/short-description` for bug fixes (correcting an incorrect
+     behavior);
+   - `feature/short-description` for features (adding a new behavior).
+
+5. Locally make your contribution by adding/editing/deleting files and following
+  the [coding conventions](#coding-conventions);
+
+6. (Optional) Locally add non-regression test cases to the appropriate
+  subdirectory in `./tests/` or `./src/plugins/<plugin>/tests/`.
+  Consult the [plug-in developer manual](https://frama-c.com/download/frama-c-plugin-development-guide.pdf)
+  for details on how to run tests inside Frama-C.
+  You can also provide the non-regression test case in the Gitlab issue
+  discussion and we will integrate it.
+
+7. Check for unexpected changes.
+  Use the command `make check-lint`
+  in your terminal from the Frama-C root directory to detect trailing spaces,
+  tabulations or incorrect indentation (ocp-indent = 1.8.1, camomile,
+  clang-format and black (Python linter) are needed), and `make lint` to fix
+  problems if any.
+
+  Use the command `make check-headers` in your terminal from the Frama-C root
+  directory to detect incorrect file licenses (the `headache` opam package is
+  needed), and `make headers` to fix them.
+
+8. Locally run the test framework of Frama-C by typing
+  `make default-tests`
+  in your terminal (you should be in the Frama-C root directory).
+
+9. Locally add (if needed) and commit your contribution.
+
+10. Push your contribution to Gitlab.
+
+11. [Make a Gitlab merge request](https://git.frama-c.com/pub/frama-c/merge_requests).
+  The target should remain as repository `pub/frama-c` and branch `master`
+  while the source should be your personal project and your chosen branch
+  name.
+
+12. If needed (i.e. it is your first non-trivial contribution in the sense of
+  [this document](TCA.md)), please do not forget to fill and sign the
+  [Contributor Licence Agreement](CLA.pdf) and send us the signed version at
+  `cla AT frama-c DOT com`.
+
+For convenience, we recall the typical `git` commands to be used through these steps:
+```shell
+git clone https://git.frama-c.com/<username>/frama-c.git
+git checkout -b <branch-name>
+git diff --check
+git add <file1 file2 ...>
+git commit -m "<Commit message>"
+git push origin <branch-name>
+```
+where:
+
+- `<username>` is your Gitlab username;
+- `<branch-name>` is your chosen branch name;
+- `<file1 file2 ...>` are the files to add to the commit;
+- `<Commit message>` is your commit message.
+
+
+Developing external plug-ins
+============================
+
+Frama-C is a modular platform for which it is possible to develop external
+plug-ins as documented in the
+[Plug-In development guide](https://frama-c.com/download/frama-c-plugin-development-guide.pdf).
+Such plug-ins normally do not require changes to the Frama-C source code and can
+be developed completely independently, for instance in a separate Git
+repository.
+
+However, to make it easier for your users to compile and use your plug-in, even
+as newer releases are made available, we recommend the following workflow:
+
+1. Write your external plug-in as indicated in the
+  [Plug-In development guide](https://frama-c.com/download/frama-c-plugin-development-guide.pdf);
+
+2. Create an `opam` package by
+  [pinning your local plug-in](https://opam.ocaml.org/doc/Packaging.html#Opam-pin) and
+  [editing the `opam` file](https://opam.ocaml.org/doc/Packaging.html#The-quot-opam-quot-file).
+  You can have a look at the
+  [`opam` file of the Hello plug-in](https://github.com/Frama-C/frama-c-hello/blob/master/opam)
+  if necessary.
+
+3. Optionally
+  [publish your plug-in](https://opam.ocaml.org/doc/Packaging.html#Publishing)
+  in the official OPAM packages repository.
+
+4. Announce your contribution to the Frama-C ecosystem on the
+  [Frama-C-discuss mailing list](https://lists.gforge.inria.fr/mailman/listinfo/frama-c-discuss).
+  Well done!
+
+The main advantage of this procedure is that opam will perform several
+consistency checks of your plug-in,
+with respect to several Frama-C versions and OCaml dependencies.
+
+Coding conventions
+==================
+
+- Use [ocp-indent](https://github.com/OCamlPro/ocp-indent), v1.8.1
+  to indent OCaml source files (available from `opam`);
+
+- Use [black](https://pypi.org/project/black/) to indent Python source files;
+
+- Use [clang-format](https://clang.llvm.org/docs/ClangFormat.html) to indent C
+  files (mostly for E-ACSL, and possibly tests);
+
+- Avoid trailing whitespaces;
+
+- Avoid using tabs;
+
+- Strive to keep within 80 characters per line.

Changelog_detailed.md

+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

LICENSE

+Most sources are LGPLv2.1, with some isolated exceptions for
+external libraries modified for Frama-C (BSD, QPL) in src/libraries
+
+Each source file contains its own header. See the licenses directory for the
+complete text of each license.
+
+Documentation is licensed under CC-BY-SA 4.0. See doc/LICENSE for more
+information

Makefile

+##########################################################################
+#                                                                        #
+#  This file is part of Frama-C.                                         #
+#                                                                        #
+#  Copyright (C) 2007-2025                                               #
+#    CEA (Commissariat à l'énergie atomique et aux énergies              #
+#         alternatives)                                                  #
+#                                                                        #
+#  you can redistribute it and/or modify it under the terms of the GNU   #
+#  Lesser General Public License as published by the Free Software       #
+#  Foundation, version 2.1.                                              #
+#                                                                        #
+#  It is distributed in the hope that it will be useful,                 #
+#  but WITHOUT ANY WARRANTY; without even the implied warranty of        #
+#  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the         #
+#  GNU Lesser General Public License for more details.                   #
+#                                                                        #
+#  See the GNU Lesser General Public License version 2.1                 #
+#  for more details (enclosed in the file licenses/LGPLv2.1).            #
+#                                                                        #
+##########################################################################
+
+# This file is the main makefile of Frama-C.
+
+MAKECONFIG_DIR=share
+FRAMAC_DEVELOPER?=
+
+include $(MAKECONFIG_DIR)/Makefile.common
+
+##############################################################################
+# TOOLS CONFIG
+################################
+
+IN_FRAMAC:=yes
+
+FRAMAC_PTESTS_SRC:=tools/ptests
+FRAMAC_HDRCK_SRC:=tools/hdrck
+FRAMAC_LINTCK_SRC:=tools/lint
+
+##############################################################################
+# Frama-C
+################################
+
+.PHONY: all
+
+DUNE_WS?=
+
+ifneq (${DUNE_WS},)
+  WORKSPACE_OPT:=--workspace dev/dune-workspace.${DUNE_WS}
+else
+  WORKSPACE_OPT:=
+endif
+
+DISABLED_PLUGINS?=
+
+all::
+ifeq (${FRAMAC_DEVELOPER},yes)
+	dune build --no-print-directory --root ${FRAMAC_LINTCK_SRC}
+	dune build --no-print-directory --root ${FRAMAC_HDRCK_SRC}
+endif
+ifneq ($(DISABLED_PLUGINS),)
+	dune clean
+	rm -rf _build .merlin
+	./dev/disable-plugins.sh ${DISABLED_PLUGINS}
+endif
+	dune build ${WORKSPACE_OPT} ${DUNE_BUILD_OPTS} @install
+
+clean:: purge-tests # to be done before a "dune" command
+ifeq (${FRAMAC_DEVELOPER},yes)
+	dune clean --no-print-directory --root ${FRAMAC_LINTCK_SRC}
+	dune clean --no-print-directory --root ${FRAMAC_HDRCK_SRC}
+endif
+	dune clean
+	rm -rf _build .merlin
+
+##############################################################################
+# IVETTE
+################################
+
+.PHONY: ivette ivette-api ivette-dev
+
+ivette: all
+	@$(MAKE) -C ivette
+
+ivette-dev: all
+	@$(MAKE) -C ivette dev
+
+ivette-api: all
+	@$(MAKE) -C ivette api
+
+##############################################################################
+# HELP
+################################
+
+help::
+	@echo "Build configuration variables"
+	@echo "  - RELEASE: compile in release mode if set to 'yes'"
+	@echo "  - DUNE_DISPLAY: parameter transmitted to dune --display option"
+	@echo "  - DISABLED_PLUGINS: disable these plugins before (re)building"
+	@echo "    (none for enabling all plugins)"
+
+##############################################################################
+# INSTALL/UNINSTALL
+################################
+
+install:: all
+
+INSTALL_TARGET=Frama-C
+include share/Makefile.installation
+include ivette/Makefile.installation
+
+ifeq (${FRAMAC_DEVELOPER},yes)
+
+install::
+	@echo "Installing frama-c-hdrck and frama-c-lint"
+	dune install --root ${FRAMAC_HDRCK_SRC} --prefix ${PREFIX} ${MANDIR_OPT} 2> /dev/null
+	dune install --root ${FRAMAC_LINTCK_SRC} --prefix ${PREFIX} ${MANDIR_OPT} 2> /dev/null
+
+uninstall::
+	@echo "Uninstalling frama-c-hdrck and frama-c-lint"
+	dune uninstall --root ${FRAMAC_HDRCK_SRC} --prefix ${PREFIX} ${MANDIR_OPT} 2> /dev/null
+	dune uninstall --root ${FRAMAC_LINTCK_SRC} --prefix ${PREFIX} ${MANDIR_OPT} 2> /dev/null
+
+endif
+
+###############################################################################
+# HEADER MANAGEMENT
+################################
+
+# Part that can be shared for external plugins
+include share/Makefile.headers
+
+###############################################################################
+# Testing
+################################
+
+# PTESTS is internal
+FRAMAC_PTESTS:=$(FRAMAC_PTESTS_SRC)/ptests.exe
+
+# WTESTS is internal
+FRAMAC_WTESTS:=$(FRAMAC_PTESTS_SRC)/wtests.exe
+
+# Frama-C also has ptest directories in plugins, so we do not use default
+PTEST_ALL_DIRS:=tests $(shell find src/plugins -type d -name tests) \
+  src/kernel_internals/parsing/tests
+
+# Test aliasing definition allowing ./configure --disable-<plugin>
+PTEST_ALIASES:=@tests/ptests @src/plugins/ptests \
+  @src/kernel_internals/parsing/tests/ptests
+
+# WP tests need WP cache
+PTEST_USE_WP_CACHE:=yes
+
+# Part that can be shared for external plugins
+include share/Makefile.testing
+
+###############################################################################
+# Linters
+################################
+
+# Code prettyfication and lint
+include share/Makefile.linting
+
+###############################################################################
+# Frama-C Documentation
+################################
+
+include share/Makefile.documentation
+
+###############################################################################
+# Local Variables:
+# compile-command: "make"
+# End:

README.md

+![Frama-C](share/frama-c.png?raw=true)
+
+[Frama-C](https://frama-c.com) 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](https://frama-c.com/acsl.html)** (*ANSI/ISO C Specification Language*)
+properties. Plug-ins can also collaborate via their APIs.
+
+## Installation
+
+Frama-C is available through [opam](https://opam.ocaml.org/), the
+OCaml package manager. If you have it, simply run:
+
+    opam install frama-c
+
+or, for `opam` versions less than 2.1:
+
+    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](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](#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]
+    ivette file.c -<plugin> [options]
+
+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 graphical interface,
+`ivette`.
+A legacy version of the GUI (`frama-c-gui`) is also available.
+
+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 complex usage scenarios (several files and directories,
+preprocessing directives, etc), we recommend the following two-step approach:
+
+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 complex C applications usually involves C preprocessor options
+(e.g. GCC's `-D` and `-I`).
+In Frama-C, they are passed via option `-cpp-extra-args`, as in this example:
+
+    frama-c *.c -cpp-extra-args="-D<define> -I<include>" -save parsed.sav
+
+The results can then be loaded into Frama-C for further analyses or for inspection
+via the GUI:
+
+    frama-c -load parsed.sav -<plugin> [options]
+    ivette -load parsed.sav -<plugin> [options]
+
+## Further reference
+
+- Links to user and developer manuals, Frama-C archives,
+  and plug-in manuals are available at <br> https://frama-c.com/html/get-frama-c.html
+
+- The [Frama-C documentation page](https://frama-c.com/html/documentation.html)
+  contains links to all manuals and plugins description, as well as tutorials,
+  courses and more.
+
+- [StackOverflow](https://stackoverflow.com/questions/tagged/frama-c) has several
+  questions with the `frama-c` tag, which is monitored by several members of the
+  Frama-C community.
+
+- The [Frama-c-discuss mailing list](https://groupes.renater.fr/sympa/info/frama-c-discuss)
+  is used for announcements and general discussions.
+
+- The [Frama-C blog](https://frama-c.com/blog) has several posts about
+  new developments of Frama-C, as well as general discussions about the C
+  language, undefined behavior, floating-point computations, etc.
+
+- The [Frama-C public repository](https://git.frama-c.com/pub/frama-c)
+  contains a daily snapshot of the development version of Frama-C, as well as
+  the [issues tracking system](https://git.frama-c.com/pub/frama-c/issues),
+  for reporting bugs.
+  These [contribution guidelines](CONTRIBUTING.md) detail how to submit
+  issues or create merge requests.

TCA.md

+**Trivial Contribution Policy**
+
+The purpose of this Policy is to clarify and document the circumstances
+in which a Contribution, deemed as Trivial, does not fall within the
+scope of the Contributor License Agreement.
+
+As a general rule, Contributions that do not involve creative decisions
+or which are not substantial will be considered to be Trivial.
+
+As a guideline, a Contribution may be qualified according to the
+following:
+
++-----------------------+-----------------------+-----------------------+
+| *Type of              | *≤ 10 lines*          | *\> 10 lines*         |
+| contribution*         |                       |                       |
++=======================+=======================+=======================+
+| Feature               |                       |                       |
+|                       | • Not trivial         | • Not trivial         |
+| (add new functional   |                       |                       |
+| behavior)             |                       |                       |
++-----------------------+-----------------------+-----------------------+
+| Improvement           |                       |                       |
+|                       | • Probably            | • Not trivial         |
+| (improve              |   not trivial         |                       |
+| non-functional        |                       |                       |
+| behavior)             |                       |                       |
++-----------------------+-----------------------+-----------------------+
+|                       | • Not trivial if      | • Not trivial if      |
+|                       | creative code         | creative code         |
+| Bug fix               |                       |                       |
+|                       | • Not trivial if      | • Not trivial if      |
+| (fix incorrect        | comprises a creative  | comprises a creative  |
+| behavior)             | comment               | comment               |
+|                       |                       |                       |
+|                       | • Probably trivial    | • Probably not        |
+|                       | otherwise             | trivial otherwise     |
++-----------------------+-----------------------+-----------------------+
+
+(1) -   -   -   
+
+<!-- -->
+
+(1) 
+
+Without prejudice to the above, and for all intents and purposes, the
+following Contributions are deemed to be Trivial:
+
+-   Spelling / grammar fixes / correcting typos
+
+-   Formatting / cleaning up comments in the code.
+
+-   Contributions that are purely deletions, such as removal of
+    duplicate information or code that never executes.
+
+-   Bug fixes that change default return values or error codes stored in
+    constants, literals, or simple variable types.
+
+-   Adding logging messages or debugging output.
+
+-   Changes to 'metadata' files.
+
+-   Renaming a build directory or changing a constant.
+
+-   Configuration changes.
+
+-   Changes in build or installation scripts.
+
+-   Re-ordering of objects or subroutines.
+
+-   Moving source files from one directory or package to another, with
+    no changes in code.
+
+-   Breaking a source file into multiple source files, or consolidating
+    multiple source files into one source file, with no code changes.
+
+However, there are many gray areas. Please reach us at `cla AT frama-c DOT com`
+should you have any questions on the nature of your
+intended Contribution.