.Makefile.lint

-ML_LINT_KO:=
-ML_LINT_KO+=src/kernel_internals/parsing/check_logic_parser.ml
-ML_LINT_KO+=src/kernel_internals/parsing/errorloc.ml
-ML_LINT_KO+=src/kernel_internals/parsing/errorloc.mli
-ML_LINT_KO+=src/kernel_internals/parsing/lexerhack.ml
-ML_LINT_KO+=src/kernel_internals/parsing/logic_preprocess.mli
-ML_LINT_KO+=src/kernel_internals/runtime/boot.ml
-ML_LINT_KO+=src/kernel_internals/runtime/machdeps.ml
-ML_LINT_KO+=src/kernel_internals/runtime/messages.ml
-ML_LINT_KO+=src/kernel_internals/runtime/messages.mli
-ML_LINT_KO+=src/kernel_internals/runtime/special_hooks.ml
-ML_LINT_KO+=src/kernel_internals/typing/allocates.ml
-ML_LINT_KO+=src/kernel_internals/typing/frontc.mli
-ML_LINT_KO+=src/kernel_internals/typing/infer_annotations.ml
-ML_LINT_KO+=src/kernel_internals/typing/mergecil.mli
-ML_LINT_KO+=src/kernel_internals/typing/translate_lightweight.ml
-ML_LINT_KO+=src/kernel_internals/typing/translate_lightweight.mli
-ML_LINT_KO+=src/kernel_internals/typing/unroll_loops.ml
-ML_LINT_KO+=src/kernel_internals/typing/unroll_loops.mli
-ML_LINT_KO+=src/kernel_services/abstract_interp/abstract_interp.ml
-ML_LINT_KO+=src/kernel_services/abstract_interp/abstract_interp.mli
-ML_LINT_KO+=src/kernel_services/abstract_interp/base.ml
-ML_LINT_KO+=src/kernel_services/abstract_interp/base.mli
-ML_LINT_KO+=src/kernel_services/abstract_interp/fval.mli
-ML_LINT_KO+=src/kernel_services/abstract_interp/int_Base.ml
-ML_LINT_KO+=src/kernel_services/abstract_interp/int_Base.mli
-ML_LINT_KO+=src/kernel_services/abstract_interp/int_Intervals_sig.mli
-ML_LINT_KO+=src/kernel_services/abstract_interp/ival.ml
-ML_LINT_KO+=src/kernel_services/abstract_interp/ival.mli
-ML_LINT_KO+=src/kernel_services/abstract_interp/lattice_messages.ml
-ML_LINT_KO+=src/kernel_services/abstract_interp/lattice_messages.mli
-ML_LINT_KO+=src/kernel_services/abstract_interp/lattice_type.mli
-ML_LINT_KO+=src/kernel_services/abstract_interp/lmap.ml
-ML_LINT_KO+=src/kernel_services/abstract_interp/lmap.mli
-ML_LINT_KO+=src/kernel_services/abstract_interp/lmap_bitwise.ml
-ML_LINT_KO+=src/kernel_services/abstract_interp/lmap_bitwise.mli
-ML_LINT_KO+=src/kernel_services/abstract_interp/locations.ml
-ML_LINT_KO+=src/kernel_services/abstract_interp/locations.mli
-ML_LINT_KO+=src/kernel_services/abstract_interp/map_lattice.ml
-ML_LINT_KO+=src/kernel_services/abstract_interp/map_lattice.mli
-ML_LINT_KO+=src/kernel_services/abstract_interp/offsetmap.ml
-ML_LINT_KO+=src/kernel_services/abstract_interp/offsetmap.mli
-ML_LINT_KO+=src/kernel_services/abstract_interp/offsetmap_bitwise_sig.mli
-ML_LINT_KO+=src/kernel_services/abstract_interp/offsetmap_sig.mli
-ML_LINT_KO+=src/kernel_services/abstract_interp/origin.ml
-ML_LINT_KO+=src/kernel_services/abstract_interp/origin.mli
-ML_LINT_KO+=src/kernel_services/abstract_interp/tr_offset.mli
-ML_LINT_KO+=src/kernel_services/analysis/bit_utils.ml
-ML_LINT_KO+=src/kernel_services/analysis/bit_utils.mli
-ML_LINT_KO+=src/kernel_services/analysis/dataflow2.ml
-ML_LINT_KO+=src/kernel_services/analysis/dataflow2.mli
-ML_LINT_KO+=src/kernel_services/analysis/dataflows.ml
-ML_LINT_KO+=src/kernel_services/analysis/dataflows.mli
-ML_LINT_KO+=src/kernel_services/analysis/dominators.ml
-ML_LINT_KO+=src/kernel_services/analysis/interpreted_automata.ml
-ML_LINT_KO+=src/kernel_services/analysis/interpreted_automata.mli
-ML_LINT_KO+=src/kernel_services/analysis/logic_interp.ml
-ML_LINT_KO+=src/kernel_services/analysis/loop.ml
-ML_LINT_KO+=src/kernel_services/analysis/ordered_stmt.ml
-ML_LINT_KO+=src/kernel_services/analysis/service_graph.ml
-ML_LINT_KO+=src/kernel_services/analysis/service_graph.mli
-ML_LINT_KO+=src/kernel_services/analysis/stmts_graph.ml
-ML_LINT_KO+=src/kernel_services/analysis/stmts_graph.mli
-ML_LINT_KO+=src/kernel_services/analysis/undefined_sequence.ml
-ML_LINT_KO+=src/kernel_services/analysis/wto_statement.ml
-ML_LINT_KO+=src/kernel_services/analysis/wto_statement.mli
-ML_LINT_KO+=src/kernel_services/ast_data/annotations.ml
-ML_LINT_KO+=src/kernel_services/ast_data/annotations.mli
-ML_LINT_KO+=src/kernel_services/ast_data/ast.ml
-ML_LINT_KO+=src/kernel_services/ast_data/ast.mli
-ML_LINT_KO+=src/kernel_services/ast_data/kernel_function.ml
-ML_LINT_KO+=src/kernel_services/ast_data/kernel_function.mli
-ML_LINT_KO+=src/kernel_services/ast_data/property_status.mli
-ML_LINT_KO+=src/kernel_services/ast_queries/ast_info.ml
-ML_LINT_KO+=src/kernel_services/ast_queries/ast_info.mli
-ML_LINT_KO+=src/kernel_services/ast_queries/cil_const.ml
-ML_LINT_KO+=src/kernel_services/ast_queries/cil_const.mli
-ML_LINT_KO+=src/kernel_services/ast_queries/cil_datatype.mli
-ML_LINT_KO+=src/kernel_services/ast_queries/cil_state_builder.mli
-ML_LINT_KO+=src/kernel_services/ast_queries/file.mli
-ML_LINT_KO+=src/kernel_services/ast_queries/logic_const.mli
-ML_LINT_KO+=src/kernel_services/ast_transformations/clone.ml
-ML_LINT_KO+=src/kernel_services/ast_transformations/clone.mli
-ML_LINT_KO+=src/kernel_services/cmdline_parameters/cmdline.ml
-ML_LINT_KO+=src/kernel_services/cmdline_parameters/cmdline.mli
-ML_LINT_KO+=src/kernel_services/cmdline_parameters/parameter_category.ml
-ML_LINT_KO+=src/kernel_services/cmdline_parameters/parameter_category.mli
-ML_LINT_KO+=src/kernel_services/cmdline_parameters/parameter_customize.mli
-ML_LINT_KO+=src/kernel_services/cmdline_parameters/parameter_state.ml
-ML_LINT_KO+=src/kernel_services/cmdline_parameters/parameter_state.mli
-ML_LINT_KO+=src/kernel_services/cmdline_parameters/typed_parameter.ml
-ML_LINT_KO+=src/kernel_services/cmdline_parameters/typed_parameter.mli
-ML_LINT_KO+=src/kernel_services/parsetree/cabshelper.ml
-ML_LINT_KO+=src/kernel_services/parsetree/cabshelper.mli
-ML_LINT_KO+=src/kernel_services/parsetree/logic_ptree.mli
-ML_LINT_KO+=src/kernel_services/plugin_entry_points/db.ml
-ML_LINT_KO+=src/kernel_services/plugin_entry_points/db.mli
-ML_LINT_KO+=src/kernel_services/plugin_entry_points/emitter.ml
-ML_LINT_KO+=src/kernel_services/plugin_entry_points/emitter.mli
-ML_LINT_KO+=src/kernel_services/plugin_entry_points/journal.ml
-ML_LINT_KO+=src/kernel_services/plugin_entry_points/journal.mli
-ML_LINT_KO+=src/kernel_services/plugin_entry_points/log.ml
-ML_LINT_KO+=src/kernel_services/plugin_entry_points/log.mli
-ML_LINT_KO+=src/kernel_services/visitors/cabsvisit.ml
-ML_LINT_KO+=src/kernel_services/visitors/cabsvisit.mli
-ML_LINT_KO+=src/kernel_services/visitors/visitor.ml
-ML_LINT_KO+=src/kernel_services/visitors/visitor.mli
-ML_LINT_KO+=src/libraries/datatype/datatype.ml
-ML_LINT_KO+=src/libraries/datatype/datatype.mli
-ML_LINT_KO+=src/libraries/datatype/descr.ml
-ML_LINT_KO+=src/libraries/datatype/descr.mli
-ML_LINT_KO+=src/libraries/datatype/structural_descr.ml
-ML_LINT_KO+=src/libraries/datatype/structural_descr.mli
-ML_LINT_KO+=src/libraries/datatype/type.ml
-ML_LINT_KO+=src/libraries/datatype/type.mli
-ML_LINT_KO+=src/libraries/datatype/unmarshal.ml
-ML_LINT_KO+=src/libraries/datatype/unmarshal.mli
-ML_LINT_KO+=src/libraries/datatype/unmarshal_hashtbl_test.ml
-ML_LINT_KO+=src/libraries/datatype/unmarshal_test.ml
-ML_LINT_KO+=src/libraries/datatype/unmarshal_z.ml
-ML_LINT_KO+=src/libraries/project/project.ml
-ML_LINT_KO+=src/libraries/project/project.mli
-ML_LINT_KO+=src/libraries/project/project_skeleton.mli
-ML_LINT_KO+=src/libraries/project/state.ml
-ML_LINT_KO+=src/libraries/project/state.mli
-ML_LINT_KO+=src/libraries/project/state_builder.ml
-ML_LINT_KO+=src/libraries/project/state_builder.mli
-ML_LINT_KO+=src/libraries/project/state_dependency_graph.ml
-ML_LINT_KO+=src/libraries/project/state_dependency_graph.mli
-ML_LINT_KO+=src/libraries/project/state_selection.ml
-ML_LINT_KO+=src/libraries/project/state_selection.mli
-ML_LINT_KO+=src/libraries/project/state_topological.mli
-ML_LINT_KO+=src/libraries/stdlib/FCHashtbl.mli
-ML_LINT_KO+=src/libraries/stdlib/extlib.ml
-ML_LINT_KO+=src/libraries/stdlib/extlib.mli
-ML_LINT_KO+=src/libraries/utils/bag.ml
-ML_LINT_KO+=src/libraries/utils/binary_cache.ml
-ML_LINT_KO+=src/libraries/utils/bitvector.ml
-ML_LINT_KO+=src/libraries/utils/bitvector.mli
-ML_LINT_KO+=src/libraries/utils/cilconfig.ml
-ML_LINT_KO+=src/libraries/utils/command.ml
-ML_LINT_KO+=src/libraries/utils/command.mli
-ML_LINT_KO+=src/libraries/utils/escape.mli
-ML_LINT_KO+=src/libraries/utils/filepath.ml
-ML_LINT_KO+=src/libraries/utils/hook.ml
-ML_LINT_KO+=src/libraries/utils/hook.mli
-ML_LINT_KO+=src/libraries/utils/hptmap.ml
-ML_LINT_KO+=src/libraries/utils/hptmap.mli
-ML_LINT_KO+=src/libraries/utils/hptset.ml
-ML_LINT_KO+=src/libraries/utils/hptset.mli
-ML_LINT_KO+=src/libraries/utils/indexer.ml
-ML_LINT_KO+=src/libraries/utils/indexer.mli
-ML_LINT_KO+=src/libraries/utils/pretty_utils.ml
-ML_LINT_KO+=src/libraries/utils/pretty_utils.mli
-ML_LINT_KO+=src/libraries/utils/qstack.ml
-ML_LINT_KO+=src/libraries/utils/qstack.mli
-ML_LINT_KO+=src/libraries/utils/rangemap.ml
-ML_LINT_KO+=src/libraries/utils/rangemap.mli
-ML_LINT_KO+=src/libraries/utils/vector.ml
-ML_LINT_KO+=src/libraries/utils/vector.mli
-ML_LINT_KO+=src/libraries/utils/wto.ml
-ML_LINT_KO+=src/libraries/utils/wto.mli
-ML_LINT_KO+=src/plugins/aorai/Aorai.mli
-ML_LINT_KO+=src/plugins/aorai/aorai_dataflow.ml
-ML_LINT_KO+=src/plugins/aorai/aorai_dataflow.mli
-ML_LINT_KO+=src/plugins/aorai/aorai_option.ml
-ML_LINT_KO+=src/plugins/aorai/aorai_register.ml
-ML_LINT_KO+=src/plugins/aorai/data_for_aorai.ml
-ML_LINT_KO+=src/plugins/aorai/data_for_aorai.mli
-ML_LINT_KO+=src/plugins/aorai/logic_simplification.ml
-ML_LINT_KO+=src/plugins/aorai/logic_simplification.mli
-ML_LINT_KO+=src/plugins/aorai/ltl_output.ml
-ML_LINT_KO+=src/plugins/aorai/path_analysis.ml
-ML_LINT_KO+=src/plugins/aorai/promelaast.mli
-ML_LINT_KO+=src/plugins/aorai/promelaoutput.ml
-ML_LINT_KO+=src/plugins/aorai/promelaoutput.mli
-ML_LINT_KO+=src/plugins/aorai/utils_parser.ml
-ML_LINT_KO+=src/plugins/callgraph/callgraph_api.mli
-ML_LINT_KO+=src/plugins/callgraph/cg.ml
-ML_LINT_KO+=src/plugins/callgraph/cg.mli
-ML_LINT_KO+=src/plugins/callgraph/journalize.ml
-ML_LINT_KO+=src/plugins/callgraph/journalize.mli
-ML_LINT_KO+=src/plugins/callgraph/register.ml
-ML_LINT_KO+=src/plugins/callgraph/services.ml
-ML_LINT_KO+=src/plugins/callgraph/services.mli
-ML_LINT_KO+=src/plugins/callgraph/subgraph.ml
-ML_LINT_KO+=src/plugins/callgraph/subgraph.mli
-ML_LINT_KO+=src/plugins/callgraph/uses.ml
-ML_LINT_KO+=src/plugins/constant_propagation/propagationParameters.ml
-ML_LINT_KO+=src/plugins/constant_propagation/api.ml
-ML_LINT_KO+=src/plugins/from/callwise.ml
-ML_LINT_KO+=src/plugins/from/from_compute.ml
-ML_LINT_KO+=src/plugins/from/from_parameters.ml
-ML_LINT_KO+=src/plugins/from/from_register.ml
-ML_LINT_KO+=src/plugins/from/functionwise.ml
-ML_LINT_KO+=src/plugins/gui/analyses_manager.ml
-ML_LINT_KO+=src/plugins/gui/book_manager.ml
-ML_LINT_KO+=src/plugins/gui/book_manager.mli
-ML_LINT_KO+=src/plugins/gui/design.mli
-ML_LINT_KO+=src/plugins/gui/filetree.mli
-ML_LINT_KO+=src/plugins/gui/gtk_form.ml
-ML_LINT_KO+=src/plugins/gui/gtk_form.mli
-ML_LINT_KO+=src/plugins/gui/gui_printers.ml
-ML_LINT_KO+=src/plugins/gui/history.ml
-ML_LINT_KO+=src/plugins/gui/history.mli
-ML_LINT_KO+=src/plugins/gui/launcher.ml
-ML_LINT_KO+=src/plugins/gui/menu_manager.ml
-ML_LINT_KO+=src/plugins/gui/menu_manager.mli
-ML_LINT_KO+=src/plugins/gui/project_manager.ml
-ML_LINT_KO+=src/plugins/gui/project_manager.mli
-ML_LINT_KO+=src/plugins/gui/source_manager.mli
-ML_LINT_KO+=src/plugins/gui/warning_manager.ml
-ML_LINT_KO+=src/plugins/gui/warning_manager.mli
-ML_LINT_KO+=src/plugins/gui/wbox.ml
-ML_LINT_KO+=src/plugins/gui/wbox.mli
-ML_LINT_KO+=src/plugins/gui/wfile.ml
-ML_LINT_KO+=src/plugins/gui/widget.ml
-ML_LINT_KO+=src/plugins/gui/wpalette.ml
-ML_LINT_KO+=src/plugins/gui/wpalette.mli
-ML_LINT_KO+=src/plugins/gui/wpane.ml
-ML_LINT_KO+=src/plugins/gui/wpane.mli
-ML_LINT_KO+=src/plugins/gui/wtable.ml
-ML_LINT_KO+=src/plugins/gui/wtext.ml
-ML_LINT_KO+=src/plugins/gui/wtext.mli
-ML_LINT_KO+=src/plugins/impact/Impact.mli
-ML_LINT_KO+=src/plugins/impact/compute_impact.ml
-ML_LINT_KO+=src/plugins/impact/compute_impact.mli
-ML_LINT_KO+=src/plugins/impact/options.ml
-ML_LINT_KO+=src/plugins/impact/options.mli
-ML_LINT_KO+=src/plugins/impact/pdg_aux.ml
-ML_LINT_KO+=src/plugins/impact/pdg_aux.mli
-ML_LINT_KO+=src/plugins/impact/register.ml
-ML_LINT_KO+=src/plugins/inout/cumulative_analysis.ml
-ML_LINT_KO+=src/plugins/inout/cumulative_analysis.mli
-ML_LINT_KO+=src/plugins/inout/derefs.ml
-ML_LINT_KO+=src/plugins/inout/inout_parameters.ml
-ML_LINT_KO+=src/plugins/inout/inputs.ml
-ML_LINT_KO+=src/plugins/inout/operational_inputs.ml
-ML_LINT_KO+=src/plugins/inout/outputs.ml
-ML_LINT_KO+=src/plugins/inout/register.ml
-ML_LINT_KO+=src/plugins/loop_analysis/region_analysis.ml
-ML_LINT_KO+=src/plugins/loop_analysis/region_analysis_stmt.ml
-ML_LINT_KO+=src/plugins/metrics/metrics_acsl.ml
-ML_LINT_KO+=src/plugins/metrics/metrics_base.ml
-ML_LINT_KO+=src/plugins/metrics/metrics_base.mli
-ML_LINT_KO+=src/plugins/metrics/metrics_cabs.ml
-ML_LINT_KO+=src/plugins/metrics/metrics_cilast.mli
-ML_LINT_KO+=src/plugins/metrics/metrics_coverage.ml
-ML_LINT_KO+=src/plugins/metrics/metrics_gui.ml
-ML_LINT_KO+=src/plugins/metrics/metrics_parameters.ml
-ML_LINT_KO+=src/plugins/metrics/register.ml
-ML_LINT_KO+=src/plugins/metrics/register_gui.ml
-ML_LINT_KO+=src/plugins/occurrence/Occurrence.mli
-ML_LINT_KO+=src/plugins/occurrence/options.ml
-ML_LINT_KO+=src/plugins/occurrence/register.ml
-ML_LINT_KO+=src/plugins/occurrence/register_gui.ml
-ML_LINT_KO+=src/plugins/pdg/annot.ml
-ML_LINT_KO+=src/plugins/pdg/annot.mli
-ML_LINT_KO+=src/plugins/pdg/build.ml
-ML_LINT_KO+=src/plugins/pdg/ctrlDpds.ml
-ML_LINT_KO+=src/plugins/pdg/ctrlDpds.mli
-ML_LINT_KO+=src/plugins/pdg/marks.ml
-ML_LINT_KO+=src/plugins/pdg/marks.mli
-ML_LINT_KO+=src/plugins/pdg/pdg_parameters.ml
-ML_LINT_KO+=src/plugins/pdg/pdg_state.ml
-ML_LINT_KO+=src/plugins/pdg/pdg_state.mli
-ML_LINT_KO+=src/plugins/pdg/register.ml
-ML_LINT_KO+=src/plugins/pdg/sets.ml
-ML_LINT_KO+=src/plugins/pdg/sets.mli
-ML_LINT_KO+=src/plugins/pdg_types/pdgIndex.ml
-ML_LINT_KO+=src/plugins/pdg_types/pdgIndex.mli
-ML_LINT_KO+=src/plugins/pdg_types/pdgMarks.ml
-ML_LINT_KO+=src/plugins/pdg_types/pdgMarks.mli
-ML_LINT_KO+=src/plugins/pdg_types/pdgTypes.ml
-ML_LINT_KO+=src/plugins/pdg_types/pdgTypes.mli
-ML_LINT_KO+=src/plugins/postdominators/compute.ml
-ML_LINT_KO+=src/plugins/postdominators/postdominators_parameters.ml
-ML_LINT_KO+=src/plugins/postdominators/print.ml
-ML_LINT_KO+=src/plugins/print_api/print_interface.ml
-ML_LINT_KO+=src/plugins/scope/Scope.mli
-ML_LINT_KO+=src/plugins/scope/datascope.ml
-ML_LINT_KO+=src/plugins/scope/defs.ml
-ML_LINT_KO+=src/plugins/scope/zones.ml
-ML_LINT_KO+=src/plugins/security_slicing/components.ml
-ML_LINT_KO+=src/plugins/security_slicing/register_gui.ml
-ML_LINT_KO+=src/plugins/security_slicing/security_slicing_parameters.ml
-ML_LINT_KO+=src/plugins/security_slicing/security_slicing_parameters.mli
-ML_LINT_KO+=src/plugins/slicing/Slicing.mli
-ML_LINT_KO+=src/plugins/slicing/api.ml
-ML_LINT_KO+=src/plugins/slicing/fct_slice.ml
-ML_LINT_KO+=src/plugins/slicing/fct_slice.mli
-ML_LINT_KO+=src/plugins/slicing/printSlice.ml
-ML_LINT_KO+=src/plugins/slicing/register.ml
-ML_LINT_KO+=src/plugins/slicing/register_gui.ml
-ML_LINT_KO+=src/plugins/slicing/slicingActions.ml
-ML_LINT_KO+=src/plugins/slicing/slicingCmds.ml
-ML_LINT_KO+=src/plugins/slicing/slicingInternals.ml
-ML_LINT_KO+=src/plugins/slicing/slicingMacros.ml
-ML_LINT_KO+=src/plugins/slicing/slicingMarks.ml
-ML_LINT_KO+=src/plugins/slicing/slicingMarks.mli
-ML_LINT_KO+=src/plugins/slicing/slicingParameters.ml
-ML_LINT_KO+=src/plugins/slicing/slicingProject.ml
-ML_LINT_KO+=src/plugins/slicing/slicingSelect.ml
-ML_LINT_KO+=src/plugins/slicing/slicingState.ml
-ML_LINT_KO+=src/plugins/slicing/slicingTransform.ml
-ML_LINT_KO+=src/plugins/slicing/slicingTransform.mli
-ML_LINT_KO+=src/plugins/slicing/slicingTypes.ml
-ML_LINT_KO+=src/plugins/sparecode/globs.ml
-ML_LINT_KO+=src/plugins/sparecode/register.ml
-ML_LINT_KO+=src/plugins/sparecode/spare_marks.ml
-ML_LINT_KO+=src/plugins/sparecode/sparecode_params.ml
-ML_LINT_KO+=src/plugins/sparecode/sparecode_params.mli
-ML_LINT_KO+=src/plugins/sparecode/transform.ml
-ML_LINT_KO+=src/plugins/studia/Studia.mli
-ML_LINT_KO+=src/plugins/studia/options.ml
-ML_LINT_KO+=src/plugins/studia/reads.ml
-ML_LINT_KO+=src/plugins/studia/studia_gui.ml
-ML_LINT_KO+=src/plugins/studia/studia_gui.mli
-ML_LINT_KO+=src/plugins/users/users_register.ml
-ML_LINT_KO+=src/plugins/value_types/cilE.mli
-ML_LINT_KO+=src/plugins/value_types/cvalue.ml
-ML_LINT_KO+=src/plugins/value_types/cvalue.mli
-ML_LINT_KO+=src/plugins/value_types/function_Froms.ml
-ML_LINT_KO+=src/plugins/value_types/function_Froms.mli
-ML_LINT_KO+=src/plugins/value_types/inout_type.ml
-ML_LINT_KO+=src/plugins/value_types/precise_locs.ml
-ML_LINT_KO+=src/plugins/value_types/value_types.ml
-ML_LINT_KO+=src/plugins/value_types/value_types.mli
-ML_LINT_KO+=src/plugins/value_types/widen_type.ml
-ML_LINT_KO+=src/plugins/variadic/classify.ml
-ML_LINT_KO+=src/plugins/variadic/environment.ml
-ML_LINT_KO+=src/plugins/variadic/extends.ml
-ML_LINT_KO+=src/plugins/variadic/extends.mli
-ML_LINT_KO+=src/plugins/variadic/format_parser.ml
-ML_LINT_KO+=src/plugins/variadic/format_parser.mli
-ML_LINT_KO+=src/plugins/variadic/format_pprint.ml
-ML_LINT_KO+=src/plugins/variadic/format_string.ml
-ML_LINT_KO+=src/plugins/variadic/format_typer.ml
-ML_LINT_KO+=src/plugins/variadic/format_typer.mli
-ML_LINT_KO+=src/plugins/variadic/format_types.mli
-ML_LINT_KO+=src/plugins/variadic/generic.ml
-ML_LINT_KO+=src/plugins/variadic/options.ml
-ML_LINT_KO+=src/plugins/variadic/standard.ml
-ML_LINT_KO+=src/plugins/variadic/translate.ml
-ML_LINT_KO+=src/plugins/variadic/va_build.ml
-ML_LINT_KO+=src/plugins/variadic/va_types.mli
-ML_LINT_KO+=src/plugins/e-acsl/src/analyses/mmodel_analysis.ml
-ML_LINT_KO+=src/plugins/e-acsl/src/analyses/rte.ml
-ML_LINT_KO+=src/plugins/e-acsl/src/code_generator/at_with_lscope.ml
-ML_LINT_KO+=src/plugins/e-acsl/src/code_generator/at_with_lscope.mli
-ML_LINT_KO+=src/plugins/e-acsl/src/code_generator/temporal.ml
-ML_LINT_KO+=src/plugins/e-acsl/src/code_generator/temporal.mli
-

.for_devel

-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

.force-reconfigure

-2

.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
 
-*.pdf binary
+################
+# 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

@@ -3,71 +3,52 @@
 ###########
 
 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
+/bin/ivette
+.ivette
 
 #build
+/_opam/
+/frama-c*.tar.gz
+/distributed
+_build
+*.install
+*.coverage
+_coverage
+_bisect
 
-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
-.ocamldebug
+# This file is generated (on need) during configure
+/src/plugins/dune
+
+#lint
+/.lint/
 
 #tests
 
-/tests/ptests_config
-/tests/**/result/
-/tests/**/result_*/
+/.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
-/tests/journal/intra.byte
-/tests/misc/my_visitor_plugin/my_visitor.opt
-/tests/misc/my_visitor.sav
-/tests/spec/preprocess_dos.c
-/tests/*/*.opt
-/tests/pdg/*.dot
 
-/devel_tools/fc-time
-/devel_tools/fc-memuse
-/bin/ocamldep_transitive_closure
+/.test-errors.log
 
 #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/
@@ -93,13 +74,15 @@ autom4te.cache
 
 /doc/acsl/
 
-/doc/aorai/aorai-example.tgz
+/doc/aorai/aorai-example.tar.gz
 /doc/aorai/aorai-example/
-/doc/aorai/frama-c-aorai-example.tgz
+/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
@@ -109,11 +92,6 @@ autom4te.cache
 /doc/code/print_api/dynamic_plugins.mli
 /doc/code/print_api/_build/
 
-/doc/code/builtin
-/doc/code/studia
-/doc/code/qed
-/doc/code/wp
-
 /doc/doxygen
 
 /doc/pdg/call-f.eps
@@ -124,19 +102,11 @@ autom4te.cache
 /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
@@ -151,23 +121,7 @@ autom4te.cache
 
 /doc/server/
 
-#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
@@ -180,39 +134,29 @@ autom4te.cache
 /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/fc_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/libraries/stdlib/transitioning.ml
-/src/plugins/gui/dgraph.ml
-/src/plugins/gui/dgraph.mli
-/src/plugins/gui/dgraph_helper.ml
-/src/plugins/gui/GSourceView.ml
-/src/plugins/gui/GSourceView.mli
-/src/plugins/gui/GSourceView2.ml
-/src/plugins/gui/GSourceView2.mli
-/src/plugins/gui/gtk_compat.ml
+# 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:
- - git-update
- - build
- - tests
- - distrib_and_compatibility
- - make_public
+  - prepare
+  - build
+  - tests
+  - distrib
+  - compatibility
+  - release
+  - publish
+
+################################################################################
+### DEFAULT JOB PARAMETERS
+
+default:
+  interruptible: true
+  tags: [ nix-v2 ]
+
+################################################################################
+### VARIABLES
 
 variables:
-    CURRENT: $CI_COMMIT_REF_NAME
-    DEFAULT: "master"
-    FRAMA_CI_OPT: "--override frama-c:$CI_COMMIT_REF_NAME,$CI_COMMIT_SHA"
-    OCAML: "4_08"
+  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: git-update
+  stage: prepare
   script:
-   - (! git merge-base --is-ancestor a1e186c68a6418a53b3dc06237f49e8dcbf75f4a HEAD)
-   - git merge-base --is-ancestor a35d2118fe6999dddce9e1847eff626fae9cc37c HEAD
-  tags:
-   - nix
+    - (! git merge-base --is-ancestor a1e186c68a6418a53b3dc06237f49e8dcbf75f4a HEAD)
+    - git merge-base --is-ancestor a35d2118fe6999dddce9e1847eff626fae9cc37c HEAD
 
-#avoid a nix error https://github.com/NixOS/nix/issues/2087
-git-update:
-  stage: git-update
+.build_template: &do_not_stop_pipeline_template
+  stage: prepare
+  interruptible: false
   script:
-   - nix/frama-ci.sh instantiate --eval -A frama-c.src.outPath
-  tags:
-   - nix
+    - 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/frama-ci.sh build -A frama-c.installed
-  tags:
-   - nix
+    - ./nix/build-proxy.sh frama-c
+  artifacts:
+    when: on_failure
+    paths:
+      - commits.nix
+      - results.log
+    expire_in: 1 day
 
-lint:
+ivette:
   stage: build
+  <<: *ivette_setup
   script:
-   - nix/frama-ci.sh build -A frama-c.lint
-  coverage: '/lint coverage: \d+\.\d+/'
+    - make -C ivette check-lint
+    - make -C ivette dist
   tags:
-   - nix
+    - docker
+
+################################################################################
+### TESTS
 
-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/frama-ci.sh build -A frama-c.tests
-  tags:
-   - nix
+    - ./nix/build-proxy.sh e-acsl-tests
+  <<: *coverage
 
-wp-qualif:
+.build_template: &eva_template
   stage: tests
   script:
-   - nix/frama-ci.sh build -A frama-c.wp-qualif
-  tags:
-   - nix
-  allow_failure: true
+    - ./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
 
-genassigns:
+.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/frama-ci.sh build -A genassigns.tests
-  tags:
-   - nix
+    - ./nix/build-proxy.sh kernel-tests
+  <<: *coverage
 
-frama-clang:
+plugins-tests:
   stage: tests
   script:
-   - nix/frama-ci.sh build -A frama-clang.tests
-  tags:
-   - nix
+    - ./nix/build-proxy.sh plugins-tests
+  <<: *coverage
 
-counter-examples:
+wp-tests:
   stage: tests
   script:
-   - nix/frama-ci.sh build -A counter-examples.tests
-  tags:
-   - nix
+    - ./nix/build-proxy.sh wp-tests
+  <<: *coverage
 
-acsl-importer:
+ivette-tests:
   stage: tests
+  when: manual
+  <<: *ivette_setup
   script:
-   - nix/frama-ci.sh build -A acsl-importer.tests
+    - 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:
-   - nix
+    - docker
 
-volatile:
+external-plugins:
   stage: tests
   script:
-   - nix/frama-ci.sh build -A volatile.tests
-  tags:
-   - nix
+    - ./nix/external-plugin-ci.sh $PLUGIN
+  parallel:
+    matrix:
+      - PLUGIN: [
+          "acsl-importer",
+          "caveat-importer",
+          "context-from-precondition",
+          "frama-clang",
+          "genassigns",
+          "meta",
+          "minimal",
+          "pathcrawler",
+          "security",
+          "volatile"
+        ]
 
-Security:
-  stage: tests
+################################################################################
+### DISTRIB
+
+# API documentation
+
+api-doc:
+  stage: distrib
+  variables:
+    OUT: "api"
   script:
-   - nix/frama-ci.sh build -A security.tests
-  tags:
-   - nix
+    - ./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
 
-CFP:
-  stage: tests
+api-json-doc:
+  stage: distrib
+  variables:
+    OUT: "api"
   script:
-   - nix/frama-ci.sh build -A context-from-precondition.tests
-  tags:
-   - nix
+    - ./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: build
+  stage: distrib
+  variables:
+    OPEN_SOURCE: "yes"
+    CI_LINK: "yes"
+    HDRCK: "frama-c-hdrck"
   script:
-   - nix/frama-ci.sh build -A frama-c.build-distrib-tarball
+    - ./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:
-   - nix
+    - docker
 
-build-from-distrib-tarball:
-  stage: tests
+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:
-   - nix/frama-ci.sh build -A frama-c.build-from-distrib-tarball
+    # 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:
-   - nix
+    - 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: distrib_and_compatibility
-  tags:
-   - nix
+  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:
-   - nix/frama-ci.sh build -A frama-c.internal
+    - 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
 
-internal_nightly:
-  <<: *internal_template
+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:
-   - nix/frama-ci.sh build -A frama-c.internal
-  only:
-  - schedules
+    - 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
 
-.build_template: &frama-c-ocaml
-  stage: distrib_and_compatibility
+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:
-   - nix/frama-ci.sh build -A frama-c.tests
+    - 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:
-   - nix
+    - 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
 
-frama-c-ocaml-4.09:
+.build_template: &src_distrib_tests_template
+  stage: compatibility
   variables:
-    OCAML: "4_09"
-  <<: *frama-c-ocaml
-  only:
-  - schedules
+    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
 
-frama-c-ocaml-4.10:
+.build_template: &prepare_ssh_template
+  before_script:
+    - export GIT_SSH=$PWD/nix/frama-c-public/ssh.sh
+
+release-branch:
+  stage: release
   variables:
-    OCAML: "4_10"
-  <<: *frama-c-ocaml
+    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
 
-caveat-importer:
-  stage: tests
+release-opam:
+  stage: release
+  <<: *prepare_ssh_template
   script:
-   - nix/frama-ci.sh build -A caveat-importer.tests
-  tags:
-   - nix
+    - nix-shell -p git git-lfs coreutils openssh --run './nix/frama-c-public/publish-opam.sh'
+  <<: *when_release
+  interruptible: false
 
-mthread:
-  stage: tests
+release-website:
+  stage: release
+  <<: *prepare_ssh_template
   script:
-   - nix/frama-ci.sh build -A mthread.tests
-  tags:
-   - nix
+    - nix-shell -p git git-lfs coreutils openssh --run './nix/frama-c-public/publish-website.sh'
+  <<: *when_release
+  interruptible: false
 
-pathcrawler:
-  stage: tests
+release-wiki:
+  stage: release
+  <<: *prepare_ssh_template
   script:
-   - nix/frama-ci.sh build -A pathcrawler.tests
-  tags:
-   - nix
+    - nix-shell -p git git-lfs coreutils openssh --run './nix/frama-c-public/publish-wiki.sh'
+  <<: *when_release
+  interruptible: false
 
-e-acsl-tests-dev:
-  stage: tests
+################################################################################
+### 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:
-   - nix/frama-ci.sh build -A frama-c.e-acsl-tests-dev
-  tags:
-   - nix
+    - (! 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
 
-ivette:
-  stage: build
-  image: node
-  cache:
-    paths:
-    - ivette/node_modules/
+publish-fclang:
+  stage: publish
+  variables:
+    BRANCH: "master"
+    REPOSITORY: "frama-clang"
+  <<: *prepare_ssh_template
   script:
-   - node --version
-   - npm --version
-   - yarn --version
-   - make -C ivette
-  tags:
-    - docker
+    - nix-shell -p coreutils openssh --run './nix/frama-c-public/publish-branch.sh'
+  <<: *when_publish
+  interruptible: false
 
-make_public:
-  stage: make_public
+publish-meta:
+  stage: publish
+  variables:
+    BRANCH: "master"
+    REPOSITORY: "meta"
+  <<: *prepare_ssh_template
   script:
-   - (! git merge-base --is-ancestor a1e186c68a6418a53b3dc06237f49e8dcbf75f4a origin/master)
-   - echo "$FRAMA_C_PUBLIC_SSH_PRIVATE_KEY" | nix run -f channel:nixos-19.03 coreutils --command base64 -d > nix/frama-c-public/id_ed25519
-   - nix run -f channel:nixos-19.03 coreutils --command chmod 400 nix/frama-c-public/id_ed25519
-   - GIT_SSH=nix/frama-c-public/ssh.sh nix run -f channel:nixos-19.03 openssh --command git push git@git.frama-c.com:pub/frama-c.git origin/master:refs/heads/master
-  tags:
-  - nix
+    - 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:
-  - schedules
+    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 confirm (by adding a X in the [ ]):
+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).
 
-- [ ] the issue has not yet been reported on [Gitlab](https://git.frama-c.com/pub/frama-c/issues);
-- [ ] the issue has not yet been reported on our [BTS](https://bts.frama-c.com);
-- [ ] 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]…
+-->
 
-# Contextual information
+### Steps to reproduce the issue
 
-- 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*
-
-*Please add specific information deemed relevant with regard to this issue.*
+<!--
+Please indicate here steps to follow to get a [minimal, complete, and verifiable example](https://stackoverflow.com/help/mcve) which reproduces the issue.
+-->
 
-# Steps to reproduce the issue
+### Expected behaviour
 
-*Please indicate here steps to follow to get a [minimal, complete, and verifiable example](https://stackoverflow.com/help/mcve) which reproduces the issue.*
+<!--
+Please explain here what is the expected behaviour.
+-->
 
-# Expected behaviour
+### Actual behaviour
 
-*Please explain here what is the expected behaviour.*
+<!--
+Please explain here what is the actual (faulty) behaviour.
+-->
 
-# Actual behaviour
+### Contextual information
 
-*Please explain here what is the actual (faulty) behaviour.*
+- 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*
 
-# Fix ideas
+### Additional information (optional)
 
-*Please tell us if you already tried some work-arounds or have some ideas to solve this issue.*
+<!--
+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/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

@@ -13,4 +13,4 @@ Muriel Roger <muriel.roger@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>
+<mounir.assaf@cea.fr> <mounir.assaf@cea.Fr>
\ No newline at end of file

.make-clean-stamp

-7

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)

ALL_VERSIONS

-Version number			Date of release		Notes
-==============			===============		=====
-21.1 (Scandium)                 2020, June 25           Bugs fixed
-21.0 (Scandium)                 2020, June 11
-20.0 (Calcium)                  2019, December 4
-19.1 (Potassium)                2019, September 18      OCaml 4.08 compatibility
-19.0 (Potassium)                2019, June 21
-18.0 (Argon)                    2018, November 29
-Chlorine-20180502               2018, July 06           Bug fixed
-Chlorine-20180501               2018, June 01
-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

CONTRIBUTING.md

@@ -8,7 +8,7 @@ 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://lists.gforge.inria.fr/mailman/listinfo/frama-c-discuss);
+  [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);
@@ -19,7 +19,7 @@ There are several ways to participate in the Frama-C project:
 - [Developing external plug-ins](#developing-external-plug-ins)
   and sharing it with us through a Gitlab merge request;
 
-- Joining the [Frama-C team](http://frama-c.com/about.html) (as an intern, a PhD
+- [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
@@ -35,6 +35,10 @@ 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
@@ -44,7 +48,7 @@ The detailed steps to submit a contribution to Frama-C are:
 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 snapshot repository on your computer;
+3. Clone the forked Frama-C repository on your computer;
 
 4. Create and switch to a dedicated branch. We suggest the following
    naming convention:
@@ -56,43 +60,47 @@ The detailed steps to submit a contribution to Frama-C are:
   the [coding conventions](#coding-conventions);
 
 6. (Optional) Locally add non-regression test cases to the appropriate
-  subdirectory in `./tests/`. The `hello` tutorial in the
-  [plug-in developer manual](http://frama-c.com/download/frama-c-plugin-development-guide.pdf)
-  provides an example of the use of the dedicated `ptests`
-  tool used by Frama-C developers. The full documentation for `ptests` is also
-  present later in the same manual.
+  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 lint`
+  Use the command `make check-lint`
   in your terminal from the Frama-C root directory to detect trailing spaces,
-  tabulations or incorrect indentation (ocp-ident >= 1.7.0 is needed).
+  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 tests`
-  in your terminal (you should be in the Frama-C root directory);
+  `make default-tests`
+  in your terminal (you should be in the Frama-C root directory).
 
-9. Locally add (if needed) and commit your contribution;
+9. Locally add (if needed) and commit your contribution.
 
-10. Push your contribution to Gitlab;
+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. you didn't already do that and your contribution is
-    not trivial in the sense of [this document](TCA.md)), please don't forget
-    to fill and sign the [Contributor Licence Agreement](CLA.pdf) and send us
-    the signed version at `cla AT frama-c DOT com`
+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 file 2>
+git add <file1 file2 ...>
 git commit -m "<Commit message>"
 git push origin <branch-name>
 ```
@@ -100,7 +108,7 @@ where:
 
 - `<username>` is your Gitlab username;
 - `<branch-name>` is your chosen branch name;
-- `<file1 file2>` are the files to add to the commit;
+- `<file1 file2 ...>` are the files to add to the commit;
 - `<Commit message>` is your commit message.
 
 
@@ -109,26 +117,26 @@ 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](http://frama-c.com/download/frama-c-plugin-development-guide.pdf).
+[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 as exemplified by the [Hello plug-in](https://github.com/Frama-C/frama-c-hello).
+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](http://frama-c.com/download/frama-c-plugin-development-guide.pdf);
+  [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](http://opam.ocaml.org/doc/Packaging.html#Opam-pin) and
-  [editing the `opam` file](http://opam.ocaml.org/doc/Packaging.html#The-quot-opam-quot-file).
+  [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](http://opam.ocaml.org/doc/Packaging.html#Publishing)
+  [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
@@ -142,8 +150,13 @@ with respect to several Frama-C versions and OCaml dependencies.
 Coding conventions
 ==================
 
-- Use [ocp-indent](https://github.com/OCamlPro/ocp-indent), v1.7.0
-  to indent OCaml source files;
+- 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;
 

Changelog

@@ -6,21 +6,564 @@
 # Mark "+": change for Frama-C-commits audience (not in html version).        #
 # Mark "*": bug fixed.                                                        #
 # Mark "!": change that can break compatibility with existing development.    #
-# '#nnn'   : BTS entry #nnn                                                   #
-# '#!nnn'  : BTS private entry #nnn                                           #
+# '##nnn'  : Public Gitlab (pub/frama-c) issue
 # '#@nnn'  : Gitlab frama-c/frama-c issue                                     #
 # For compatibility with old change log formats:                              #
+# '#nnn'   : BTS entry #nnn (OBSOLETE)                                        #
+# '#!nnn'  : BTS private entry #nnn  (OBSOLETE)                               #
 # '#?nnn'  : OLD-BTS entry #nnn                                               #
 ###############################################################################
 
-##################################
+###############################################################################
 Open Source Release <next-release>
-##################################
+###############################################################################
+
+-!  Kernel    [2025-03-21] Change API to register attributes, with now the
+              possibility to ignore an attribute when comparing types, and
+              to print or not the attribute in the AST. AttrIgnored was replaced
+              by AttrUnknown which by default has the same behavior.
+-   Kernel    [2025-03-13] Add option `-commands-file` to group Frama-C options
+              in a separate file.
+-   Kernel    [2025-03-12] Fix handling of qualifiers in array formals during
+              typing phase (fix #@998).
+o   Kernel    [2025-02-25] Frama-C now uses OCamlmig (see developer manual) to
+              perform migrations between versions.
+o!  Kernel    [2025-02-25] New module Ast_types for type related functions. Most
+              functions migrated from Cil, where they have been deprecated.
+o!  Kernel    [2025-02-17] New module Ast_attributes for attribute related
+              functions. Most functions migrated from Cil, where they have been
+              deprecated.
+-   Libc      [2025-02-14] Add __fc_gcc_builtin_macros.h to improve analyses
+              for code using GCC libc builtins (e.g. __builtin_strlen).
+-*  Kernel    [2025-02-14] Proper support for forwarded enum as gcc extension
+              Fixes ##2681 and #@1348
+-*  Kernel    [2025-02-13] ACSL arrays can have an arbitrary term as length,
+              provided it can be evaluated to an integer constant.
+              Fixes ##2695 and #@1413
+o!  Kernel    [2025-02-13] Move some functions from Logic_typing to Logic_utils
+-   Alias     [2025-02-07] New message key printer:show-libc-vars for
+              including variables stemming from the C library in the console
+              output (now disabled by default).
+o   Kernel    [2025-02-05] New parameter builder `Float` for decimal
+              command-line parameters.
+o!  Kernel    [2025-02-05] Remove the parameter `Functor_info` for every
+              `Datatype` functor building collection(s).
+-!  Kernel    [2025-02-04] Undefine some predefined GCC macros, to minimize
+              parsing errors due to unsupported compiler extensions.
+o!  Kernel    [2025-02-05] Remove attributes annotations (Cil.AttrAnnot). Use
+              normal attributes instead.
+o!  Kernel    [2025-01-31] Use a record to represent `Cil_types.typ` with two
+              fields `tnode` and `tattr` for its `typ_node` and `attributes`.
+-   Ivette    [2025-01-23] New sidebar listing functions and global variables
+              for each source file.
+-   Eva       [2025-01-23] Rename warning key `invalid-assigns` to
+              `assigns:invalid-location`
+-   Eva       [2025-01-23] All warnings about missing assigns or \from clauses
+              are now emitted as errors by default, with the new warning key
+              `assigns:missing`.
+-   Kernel    [2025-01-17] New option -memory-footprint to configure the memory
+              usage of analyses.
+o!  Kernel    [2024-12-20] Remove Cabs.SEQUENCE statement
+
+###############################################################################
+Open Source Release 30.0 (Zinc)
+###############################################################################
+
+-!  Kernel    [2024-11-04] Add partial parsing support for statement/label
+              attributes
+-   Eva       [2024-10-25] Never emit alarms on pointer conversions to intptr_t
+              or uintptr_t.
+-   Kernel    [2024-10-15] Warn when encountering an unknown attribute
+o!  Kernel    [2024-10-08] introduce logic type Lboolean and constants
+-   Kernel    [2024-10-08] Asm contracts can now have \initialized ensures.
+              See option -asm-contracts-ensure-init
+-   Kernel    [2024-10-08] Option for converting stmt contracts into
+              ACSL assert for plug-ins with incomplete stmt contract support
+              See option -inline-stmt-contracts
+-   Ivette    [2024-10-07] Complete rewriting of the callgraph, improving its
+              readability and usability and adding new features: filtering
+              and selecting functions, showing alarms by function, and more.
+-   Ivette    [2024-10-04] Show the "Source Code" view at first launch.
+-*  RTE       [2024-10-04] Fixed missing assertion on modulo signed overflow.
+-*  Eva       [2024-10-04] Fixed missing signed overflow alarm on modulo.
+-   Eva       [2024-10-04] Fewer false alarms of signed overflow on divisions.
+o!  Kernel    [2024-09-30] ACSL extensions are now associated to a plug-in,
+              allowing the registration of several extensions with the same name
+              from different plug-ins
+-   Eva       [2024-09-26] Removes approximation messages "more than N elements
+              to enumerate".
+-   Kernel    [2024-09-23] Support for ACSL modules.
+-   Kernel    [2024-09-23] Extension for importing external modules in ACSL
+o   Kernel    [2024-09-23] API to register ACSL extern modules import functions
+o!  Kernel    [2024-09-23] Move functions for finding logic types, functions,
+              predicates and constructors from Logic_typing to Logic_env.
+-   Kernel    [2024-09-20] New warning category typing:implicit-int, allowing
+              to omit type specifiers in declarations (default is error).
+o!  Kernel    [2024-09-13] Pragma nodes in the AST have been removed
+-   Slicing   [2024-09-13] -slice-pragma is now -slice-annot
+-   Slicing   [2024-09-13] `slice pragma <elem>` is now `slice_preserve_<elem>`
+-   Impact    [2024-09-13] -impact-pragma is now -impact-annot
+-   Impact    [2024-09-13] `impact pragma stmt` is now `impact_stmt`
+-   Kernel    [2024-09-03] Place noreturn attribute on types instead of vars
+-   Alias     [2024-08-22] no longer classify virtually all casts as unsafe
+o!  Kernel    [2024-08-08] New Machine module to manage theMachine and machdeps.
+              Cil functions related to theMachine are deprecated.
+-!  Kernel    [2024-08-08] New minimal OCaml version: 4.14
+o!  Kernel    [2024-08-08] Plug-ins Dominators and Postdominators have been
+              removed and replaced by the Dominators module in the kernel.
+-   Eva       [2024-08-06] Support for 'calls' ACSL extension
+o   Kernel    [2024-08-05] Added new modules `Cache_dir` and `State_dir`
+              and additional facilities to build sub-directories in these
+-!  Kernel    [2024-08-05] Changed `Config_dir` module signature, and
+              behavior on macOS and Windows
+o!  Kernel    [2024-08-05] Changed `Share` module signature
+o   Kernel    [2024-07-30] mapNoCopy moved to Extlib and deprecated in Cil
+o   Eva       [2024-07-31] Export profiling information about the analysis
+              performance via the new module Eva_perf in Eva.mli.
+-   Ivette    [2024-07-26] New flamegraph component to visualize Eva analysis
+              time by C functions, in the "Eva Summary" view by default.
+-   Ivette    [2024-07-19] New left sidebar to configure and run Eva analyses.
+-*  Eva       [2024-07-18] Fixes number of sure alarms by function shown in
+              Ivette.
+-*  Eva       [2024-06-21] Fixes possible unsoundness when writing 0 on a set of
+              contiguous and non-overlapping locations containing a value with a
+              different size or alignment than the write.
+-   Ivette    [2024-06-12] Include global initializations in the list of writes
+              of a global variable.
+-   Ivette    [2024-06-04] In the sidebar, global variables and types are sorted
+              by name.
+-   Kernel    [2024-05-20] New ACSL extension loop unfold (replaces loop pragma UNROLL)
+-!  Kernel    [2024-05-20] Removed loop pragma UNROLL annotations
+o!  Kernel    [2024-05-20] Renamed module Unroll_loop into Unfold_loop
+-   Ivette    [2024-05-17] Improved colored status bullets in AST view.
+
+###############################################################################
+Open Source Release 29.0 (Copper)
+###############################################################################
+
+-   Ivette    [2024-05-03] Fix performance issues on large codebases.
+-   Kernel    [2024-04-30] new warning category too-large-array, allowing to
+              use array > SIZE_MAX by changing its status (default is error).
+-   Eva       [2024-04-26] Improve builtins memcpy, memmove and memset when
+              arguments are imprecise.
+o   Dev       [2024-04-22] Remove frama-c-build-scripts.sh; add a section in
+              the user manual about how to manually replace it.
+-!  Kernel    [2024-04-19] Change format of custom_defs field in machdep schema
+              and allow #undefining builtin macros in the command-line.
+-   Eva       [2024-04-18] Remove support for deprecated WIDEN_HINTS loop pragma.
+              Use ACSL extension "widen_hints" instead.
+o   Kernel    [2024-04-17] Remove deprecated funcs Extlib.string_{pre,suf}fix
+-   Alias     [2024-04-16] Fix analysis results in the presence of structures.
+              Complete rework of the API. Improved documentation. Fix stack
+              overflow in case of a cyclic graph.
+-   Eva       [2024-04-10] Reduce pointer values according to ACSL predicate
+              \base_addr.
+-*  Eva       [2024-04-10] Fix a crash when running successive analyses using
+              the -eva-domains-function parameter.
+-   Ivette    [2024-04-09] New notifications at the bottom-right of the main
+              window. Some components are highlighted in the bottom bar when
+              they are updated but are not currently visible.
+-   Kernel    [2024-04-04] Avoid ambiguous pretty-printing when C labels match
+              the name of an ACSL built-in label (fix #@1359)
+-!  Kernel    [2024-04-02] Systematically abort when a function is redeclared
+              with an incompatible type, instead of trying to finish
+              type-checking, preventing misleading error msgs after the first
+              report. IncompatibleDeclHook has thus been removed from the API.
+o   Kernel    [2024-04-02] Annotations.{fold,iter}_behaviors now pass full
+              behaviors to the iterated function. To iter on fragments split by
+              behavior and emitter, use {fold,iter}_behaviors_by_emitter.
+-   Eva       [2024-03-29] Reduce pointer values according to ACSL predicate
+              valid_string and valid_read_string.
+o!  Kernel    [2024-03-29] Refactor current location handling mechanism
+o   Ivette    [2024-03-29] Upgrade to node 20 and electron 28. Use vite instead
+              of webpack. Upgrade many dependencies.
+-   Ivette    [2024-03-28] In the Eva values table, show values before/after
+              statements with annotation, as values can be reduced after them.
+-   Ivette    [2024-03-26] Add feedback when the user requests the evaluation
+              of a custom term.
+-   Kernel    [2024-03-26] Introduce \plugin:: prefix for ACSL extensions,
+              unknown extensions can be safely ignored when the plug-in that
+              handles them is not available
+-   Ivette    [2024-03-20] Add shortcut to select next/previous tab.
+-   Ivette    [2024-03-14] Complete redesign of the main view. Components and
+              views can be selected in the left sidebar (the right sidebar has
+              been removed). The top bar contains tabs of the currently selected
+              views. Components can be docked in the bottom bar, to be shown or
+              hidden on a simple click.
+-*  Variadic  [2024-03-07] Make sure that generated functions have fresh names
+o!  Kernel    [2024-03-07] More coherent naming of functions determining if a
+              symbol is a Frama-C built-in.
+-   Eva       [2024-03-04] Better reporting of imprecise "garbled mix" values
+              (resulting from imprecise or unsupported operations on addresses)
+              through more relevant messages and a compact summary at the end of
+              the analysis, enabled by default.
+-*  Kernel    [2024-03-04] Accept conditional expr whose 2d and 3d operands
+              have type void, as per C11 6.5.15§3
+-*  Kernel    [2024-02-22] When an array is declared with a fixed length l,
+              raise an error if l * sizeof(elem) > SIZE_MAX
+o!  Kernel    [2024-02-22] Merged AST nodes TCastE and TLogic_coerce
+o!  Kernel    [2024-01-29] Db is now mostly empty, the only remaining value is
+              Db.Main.extend which is deprecated and replaced by
+              Boot.Main.extend. Features related to asynchronous interactions
+              are now handled in module Async
+-   Ivette    [2023-11-24] Global variables and types are listed in the sidebar.
+              Global variables can be filtered according to some criteria.
+
+###############################################################################
+Open Source Release 28.1 (Nickel)
+###############################################################################
+
+-*  Kernel    [2024-01-18] Fix Cil.isConstant on lvalues with offset.
+-*  Ivette    [2024-01-11] Fix Ivette shell wrapper on macOS.
+
+###############################################################################
+Open Source Release 28.0 (Nickel)
+###############################################################################
+
+-   Eva       [2023-10-11] Optimization of the multidim domain.
+-!  Kernel    [2023-10-09] Remove options -no-type and -no-obj and related
+              functions.
+o!  Kernel    [2023-10-03] New mechanism for generating default specifications
+-   Kernel    [2023-10-03] New options -generated-spec-mode and
+              -generated-spec-custom for configuring how default specifications
+              are generated
+-   Eva       [2023-09-26] Support evaluation of simple \let bindings in
+              ACSL terms and predicates.
+o!  Kernel    [2023-09-25] Remove Dynamic.Unloadable exception, useless since
+              the move from dynamic to static API for plug-ins.
+-   Alias     [2023-09-07] New alias plugin that implements a points-to
+              analysis and an alias analysis based on Steensgaard's algorithm.
+              For these purposes it presents a more efficient (albeit less
+              precise) alternative to Eva. See src/plugins/alias/README.md.
+-   Kernel    [2023-09-04] Fix #@846 (printing ACSL attribute in ghost code)
+-   Eva       [2023-08-31] Adds warning key "garbled-mix" to all log messages
+              related to garbled mix (degenerated imprecise values).
+o   Eva       [2023-08-05] Remove deprecated API Db.Value.
+-   Eva       [2023-08-01] Print less messages unless -eva-show-progress is set.
+o   Kernel    [2023-07-24] Expose Cil functions for type compatibility
+-*  Eva       [2023-07-17] Fix unsound behavior on goto or switch statements
+              skipping local variable declarations: initialization alarms about
+              such variables are now properly emitted.
+-*  Eva       [2023-06-21] Fix convergence issue on dynamic memory allocation
+              in some loops.
+
+###############################################################################
+Open Source Release 27.1 (Cobalt)
+###############################################################################
+
+-   Kernel    [2023-07-17] New frama-c-script wrapper for make_machdep.py
+-*  Ivette    [2023-07-06] Fixes crash with multiple instances
+-*  GUI       [2023-07-05] Fixes freeze when a plugin aborts during splash screen
+-*  GUI       [2023-07-05] Fixes crash related to tags and undefined types
+
+###############################################################################
+Open Source Release 27.0 (Cobalt)
+###############################################################################
+
+-!  Kernel    [2023-05-15] New machdep mechanism, based on YAML files. A new
+              make_machdep.py script allows automatic machdep creation from a
+              C11-compatible (cross-)compiler.
+-   Eva       [2023-05-04] The octagon domain can now infer relations between
+              any lvalues of integer or pointer types.
+-*  Ivette    [2023-05-02] Ends properly frama-c process when Ivette is closed.
+-*  Ivette    [2023-05-02] Custom views are correctly saved and reloaded.
+-*  Eva       [2023-05-02] Fixes interpretation of Eva annotations at the end of
+              a block, and of multiple split annotations after a function call.
+-   Eva       [2023-04-24] When possible, Eva shows the name of enumeration tags
+              instead of their integer values, in the log and the GUI.
+-   Aorai     [2023-04-24] Allows comments in .ya automata files.
+-   Aorai     [2023-04-24] Supports specification about floating-point variables.
+-   Ivette    [2023-04-24] New callgraph component.
+-   Ivette    [2023-04-07] The values table shows the status of uninitialized
+              and escaping variables.
+-   Eva       [2023-04-05] Better display of large integer sets for high values
+              of the -eva-ilevel parameter.
+-   Ivette    [2023-03-31] The values table shows values of function parameters.
+-   Ivette    [2023-03-31] The values table can show the logical status of ACSL
+              predicates, and the values of C lvalues in these predicates.
+o!  GUI       [2023-03-27] Remove GTK2 bindings. Only support GTK3 as of now.
+-   Ivette    [2023-03-23] Improves function filtering in the left sidebar.
+-   Ivette    [2023-03-23] Better display of dead and non-terminating statements.
+-*  Eva       [2023-03-13] Fixes a soundness bug of the equality domain when
+              the same equality holds in two programs paths, but involving a
+              pointer pointing to different variables in the two paths.
+-   Kernel    [2023-03-03] Deprecate option -c11 (now enabled by default).
+-   Ivette    [2023-02-15] Shows information about C types in the Inspector.
+-   Eva       [2023-02-06] Fixes performance issues on programs with too many
+              function calls (more than 20000 callsites).
+-!  Kernel    [2023-01-25] Add support for C11's _Generic. Modifies Cabs AST.
+-*  Eva       [2023-01-16] Fixes unsoundness of the bitwise domain on shifts
+              and casts on big-endian architectures.
+-   Eva       [2023-01-12] Better partitioning splits on ACSL predicates.
+
+###############################################################################
+Open Source Release 26.1 (Iron)
+###############################################################################
+
+-   Logic     [2023-01-16] Accept \ghost attribute in logic annotations (##2638)
+-   Logic     [2023-01-10] Fix issue in pretty-printing ranges (##2639)
+
+###############################################################################
+Open Source Release 26.0 (Iron)
+###############################################################################
+
+-   Ivette    [2022-10-26] After an Eva analysis with taint, the taint status of
+              lvalues is shown in the Inspector component and in Dive graphs.
+-   Eva       [2022-10-25] The octagon domain can infer relations on the integer
+              conversion of floating-point variables.
+-   Ivette    [2022-10-20] The installation of Frama-C provides an installation
+              script for Ivette: run 'ivette' once to finalize its installation.
+-   Kernel    [2022-10-14] 'calls' ACSL extension is now registered in the
+              kernel and not WP
+o!  From      [2022-10-13] Removed Db.From API: use the From API instead.
+-   Ivette    [2022-10-13] Fixes some issues in the data dependency graphs
+              generated by the Dive plugin in the 'Dive Dataflow' component.
+-*  Eva       [2022-10-10] Fixes a crash on recursive functions with an ACSL
+              specification without assigns clause.
+-!  Aorai     [2022-10-11] Remove support for LTL and Promela input formats
+-   Kernel    [2022-10-05] Support for ghost VLA and calls to builtins with
+              ghost arguments.
+-   Kernel    [2022-10-03] -version prints a newline, -print-version does not.
+-   Eva       [2022-09-16] Numerors now needs MLMPFR 4.1.0+bugfix2
+o!  Eva       [2022-09-07] Deprecate Db.Value API: use the new Eva API instead.
+-   Kernel    [2022-09-07] Improve error message for invalid options -D/-I/-U.
+o!  Configure [2022-07-28] Removed autoconf and configure
+o!  Makefile  [2022-07-11] Removed Makefile, Frama-C is now built using Dune 3.x
+o!  Pdg       [2022-07-01] Removed from Db. Use proper Pdg API instead.
+-   Ivette    [2022-06-30] New component 'Eva States' that prints the internal
+              Eva domain states at a given statement for the selected marker.
+-   Ivette    [2022-06-20] In the AST component, the user can fold/unfold ACSL
+              specifications, and preconditions are now shown at call sites.
+-   Eva       [2022-06-17] Improved precision: arguments of calls interpreted by
+              an Eva builtin or with an ACSL specification can now be reduced in
+              the caller. This is especially useful on C asserts.
+-*  Eva       [2022-06-06] Fixes a possible crash when -eva-subdivide-non-linear
+              and relational domains are enabled.
+-!  Kernel    [2022-06-06] Remove journalisation.
+-   Eva       [2022-05-11] Avoid false alarms of partially overlapping lvalue
+              assignments when writing a struct array from itself.
+
+###############################################################################
+Open Source Release 25.0 (Manganese)
+###############################################################################
+
+o   Kernel    [2022-05-03] Prototype of AST comparison between two versions
+              of the same program, via the new option -ast-diff.
+-   Eva       [2022-05-02] Fixes stack overflow errors on very large C functions.
+-   Eva       [2022-04-25] Improve the multidim abstract domain: it is now
+              more precise and more robust, it is able to infer simple array
+              invariants on some loops without unrolling, and has a new option
+              -eva-multidim-disjunctive-invariants to infer structures
+              disjunctive invariants.
+o   Kernel    [2022-03-07] Known compiler builtins are no longer hardcoded in
+              OCaml, but defined via JSON files (in share/compliance).
+o   Kernel    [2022-02-23] New visitor functions visitFramacFileFunctions
+              and visitCilFileFunctions to visit only function definitions,
+              for better performance.
+o!  Kernel    [2022-02-23] Remove State_selection.Static (deprecated since
+              10 years, use directly State_selection instead)
+-*  Kernel    [2022-02-22] Fix list of potential types for decimal
+              integer literal constants
+*   Kernel    [2022-02-17] Reject programs using unsupported
+              vector_size attribute (fixes ##2573)
+o   Eva       [2022-02-15] New API to run the analysis and access its results,
+              intended to replace the old API in Db.Value. It is more precise
+              as it uses all available domains to evaluate values and locations.
+              See file Eva.mli for more details.
+*   Kernel    [2022-02-08] Reject array whose size is too big with a proper
+              error message instead of a crash (fixes ##2590)
+o!  Kernel    [2022-02-19] Removed obsolete AST nodes IndexPI and Info
+*   Kernel    [2022-02-08] Reject array whose size is too big with a proper
+              error message instead of a crash (fixes ##2590)
+o!  Kernel    [2021-12-03] Remove unused AST node Dcustom_annot and field
+              fpadding_in_bits. Do not cache size of types in the AST but in
+              a dedicated table.
+-*  Logic     [2021-11-30] Fix type of expressions whose value are functions
+o!  Kernel    [2021-11-29] Integer.pretty does not have the optional argument
+              hexa anymore. Use Integer.pretty_hex or Integer.pp_hex if you
+              want to print integers in hexadecimal format.
+
+###############################################################################
+Open Source Release 24.0 (Chromium)
+###############################################################################
+
+-*  Eva       [2022-01-19] Always emits alarms about initialization, escaping
+              pointers and special floating-point values for the arguments of
+              calls to functions without body (or whose body is not analyzed),
+              even when -eva-warn-copy-indeterminate is unset.
+-   ACSL      [2021-10-28] better type checks for volatile clauses
+-   Variadic  [2021-10-26] translates printf/scanf calls even if formatting
+              string is not constant, warning that it will assume arguments
+              match the format.
+-   Kernel    [2021-10-26] Support for C11's  _Static_assert
+-   Libc      [2021-10-26] Frama-C's libc #define _STDC_NO_COMPLEX as mandated by
+              ISO C11 for libraries without support for complex numbers
+-   Eva       [2021-10-19] New options to allow states partitioning to survive
+              function returns: -eva-interprocedural-split for disjunctions
+              from split annotations, and -eva-interprocedural-history for
+              disjunctions from the -eva-partition-history option.
+-   Eva       [2021-10-14] Supports the evaluation of ACSL set comprehension.
+-   Eva       [2021-10-14] On a SIGINT signal (Ctrl-C), the analysis is stopped
+              but partial results are saved if option -save is set.
+-*  Eva       [2021-10-12] Always checks the arguments of builtin calls for
+              alarms about initialization, escaping pointers and special
+              floating-point values, unless -eva-warn-copy-indeterminate is set.
+-*  Kernel    [2021-10-11] Fixes crashes on C integer constants overflowing
+              ocaml integers.
+-   Eva       [2021-10-06] Improves the precision of the octagon domain on
+              unsigned variables.
+-*  Eva       [2021-10-06] Fixes a soundness bug in the octagon domain on
+              integer downcasts wrapping around.
+-   Eva       [2021-09-10] Improves the symbolic-locations domain precision.
+-   Kernel    [2021-09-02] 0-sized flexible array members only available in
+              gcc_* machdeps, that now also support FAM in nested struct.
+-   Eva       [2021-07-26] Removes the maximum limit of option -eva-ilevel.
+-   Eva       [2021-07-26] New \tainted predicate to evaluate if the value of an
+              expression is tainted according to the taint domain.
+-o  Eva       [2021-07-25] Changes the Domain_builder.Complete functor to
+              automatically build more abstract domain functions.
+-*  Eva       [2021-06-24] Fixes a soundness bug of the bitwise domain with the
+              memexec cache.
+-*  Variadic  [2021-06-23] Create a fallback specialisation if there is an error
+              while translating a variadic call so that no variadic call are
+              left in the AST after Variadic.
+-   Eva       [2021-06-22] Reduction of "garbled mix" values by \valid and
+              \valid_read ACSL predicates.
+-   Eva       [2021-06-15] New experimental multidim domain to improve analysis
+              precision on arrays of structures and multidimensional arrays.
+-*  Eva       [2021-06-10] Fixes a crash in the octagon domain.
+o   Kernel    [2021-06-10] New module Cil_builder, simplifies C and ACSL code
+                           generation.
+o   Ptests    [2021-06-03] Add new PLUGIN directive and new predefined macros.
+-   Eva       [2021-06-01] Annotations split and dynamic_split can be applied
+              to logic predicates (in addition to terms).
+-   Eva       [2021-06-01] New annotation dynamic_split, similar to split, but
+              separates the analysis w.r.t. the current value of an expression
+              instead of the value it had at the annotation point: the partition
+              can be changed at an assignment to ensure that the expression
+              always evaluates to a singleton in each analysis state.
+-   Eva       [2021-05-20] New taint analysis via an experimental taint domain.
+              New annotations //@ taint … (for statements) and //@ taints … (in
+              function contracts) to initiate taint on lvalues.
+              Tainted properties can then be seen in the future GUI Ivette.
+-   Eva       [2021-05-11] Support for ACSL predicate \is_infinite.
+
+###############################################################################
+Open Source Release 23.1 (Vanadium)
+###############################################################################
+
+###############################################################################
+Open Source Release 23.0 (Vanadium)
+###############################################################################
+
+-*  Kernel    [2021-04-26] Do not crash on _Alignof(void): accept or properly
+              reject, depending on machdep. Fixes pub/frama-c#2551
+-   Eva       [2021-04-21] Partial support for recursion:
+              new option -eva-unroll-recursive-calls to precisely analyze the n
+              first recursive calls, before using the function specification
+              to interpret the remaining calls.
+              The unsound option -eva-ignore-recursive-calls has been removed.
+-!  RTE       [2021-04-16] -rte-initialized takes a set of functions as
+                           parameter (defaults to none)
+-   RTE       [2021-04-16] No more initialization warnings for full structures
+                           and unions reads. Initialization warnings for other
+                           types *without* trap representation. Refer to the
+                           documentation for more details.
+-*  Kernel    [2021-04-16] Pretty prints array formals in their original form.
+              Fixes pub/frama-c#392
+o!  Kernel    [2021-04-13] Removed deprecated function Filepath.pretty
+o!  Kernel    [2021-04-13] Filepath directories functions now return
+              Filepath.Normalized.t, Frama-C configuration and plugin
+              configuration getters updated accordingly
+o!  Kernel    [2021-04-09] Change the type of the measure from string to
+              logic_info in the variant AST node.
+o   Ptests    [2021-04-08] FILTER directive reads the standard input and can be
+              chained.
+-   Eva       [2021-04-02] Improved automatic loop unroll (-eva-auto-loop-unroll
+              option) of loops with goto or continue statements, or assigning
+              constant values to loop variants.
+-   Libc      [2021-03-31] In math.h specifications, new behaviors for cases
+              creating NaN or infinite values. These behaviors are allowed or
+              forbidden according to the -warn-special-float option.
+-*  Kernel    [2021-03-26] Raise an error if trying to merge a tentative
+              definition with a proper definition during linking
+o   Ptests    [2021-03-25] Modify MODULE directive.
+o   Ptests    [2021-03-24] Add new EXIT directive.
+-   Eva       [2021-03-15] Slightly more precise evaluation of ACSL quantifiers.
+o!  Eva       [2021-03-01] New signature for builtins, that are now registered
+              via Eva.mli instead of Db.Value.
+-   Eva       [2021-02-18] New "audit mode" to track file checksums, correctness
+              options and enabled warnings, via options -audit-prepare and
+              -audit-check.
+-   Aorai     [2021-02-09] New option for tracking last N states of the
+              automaton. Easier analysis of instrumented code with Eva.
+o!  Kernel    [2021-02-08] Avoid triggering warning 16 (unerasable optional
+              argument). Implies changing some labeled functions' signatures.
+-   ACSL      [2021-02-04] New admit annotations to express hypotheses to be
+              admitted but not verified by Frama-C.
+-   Eva       [2021-01-28] Improved automatic widening thresholds (widen hints):
+              use constant modulo as threshold, and infer thresholds globally
+              for global variables.
+-   Eva       [2021-01-21] Better interpretation of logical operators && and ||
+              (useful when option -keep-logical-operators is enabled).
+o!  Kernel    [2021-01-15] Make cfields list optional. None means undefined,
+              empty struct allowed only in specific machdeps.
+              removed cdefined field
+-*  RTE       [2021-01-13] Remove spurious assert when comparing function
+              pointer to NULL (fixes #@940)
+-   Kernel    [2021-01-12] Set default machdep to x86_64 (was x86_32);
+              allow setting machdep via environment variable FRAMAC_MACHDEP.
+-   Kernel    [2021-01-08] Allow -add-symbolic-path to survive saves/loads and
+              invert argument order (path:name).
+-*  Eva       [2020-12-05] Fixes a crash when subdividing the evaluation of
+              pointer expressions (via option -eva-subdivide-non-linear).
+-   Libc      [2020-12-02] Remove obsolete attribute FRAMA_C_MODEL in the libc.
+              Fixes #@877.
+-*  Logic     [2020-11-30] The assigns clause can't mention const locations
+              anymore. Fixes #@855.
+o   Kernel    [2020-11-27] Extract builtin-related functions from module Cil
+              to module Cil_builtins. Code can be updated using
+              `bin/migration_scripts/titanium2vanadium.sh`.
+-   Eva       [2020-11-26] Allow using Eva directives Frama_C_show_each and
+              Frama_C_dump_each in ghost code.
+-   Metrics   [2020-10-27] Add json output in addition to text and html.
 
+###############################################################################
+Open Source Release 22.0 (Titanium)
+###############################################################################
+
+-   MdR       [2020-10-19] Update Sarif output to 2.1.0 + prettier URI
+-   Dev       [2020-10-20] Support for OCamlGraph 2.0.0
+-   ACSL      [2020-10-16] Allows for axiomatic blocks-like extensions
+-   Variadic  [2020-10-14] Don't print generated function name but print
+              original name and a comment with the generated name so that the
+              printed code is compilable.
+-   Aorai     [2020-10-13] Ya automata can set auxiliary variables during a
+              transition, and use such variables in subsequent guards.
+-   Kernel    [2020-10-09] Add option -print-config-json, to output Frama-C
+              configuration data in JSON format.
+-   Logic     [2020-10-14] '\from' now accepts '&v' expressions
+-   Metrics   [2020-10-01] Distinguish between undefined but specified functions
+              and functions with neither definition nor specification.
+-*  Eva       [2020-09-28] Improved string builtins on wide strings: crash fixed,
+              better performance, misaligned pointers now considered invalid.
+-   Kernel    [2020-09-22] New option -autocomplete p1, ..., pn that list the
+              options of plug-ins p1, ..., pn in a format suitable for
+              autocompletion scripts.
+-   Kernel    [2020-09-21] Option -permissive now allows non-existent option
+              names.
+-   Logic     [2020-09-11] Introduce check-only annotations for
+              requires, ensures, loop invariant and lemmas
+-   Kernel    [2020-09-08] Add option -print-cpp-commands, to print the
+              preprocessing commands used by Frama-C.
+-   Eva       [2020-09-07] Deprecates legacy options aliases -val-* in favor
+              of option names -eva-*.
+-*  Slicing   [2020-09-07] Better handling of invalid command line options.
 -   Eva       [2020-07-27] Improved automatic loop unroll (-eva-auto-loop-unroll
               option) on loops with several exit conditions, conditions using
               equality operators, temporary variables introduced by the Frama-C
               normalization or goto statements.
+-!  Kernel    [2020-07-21] OCaml version greater than or equal to 4.08.1 required.
 -   Eva       [2020-05-29] New builtins for trigonometric functions acos, asin
               and atan (and their single-precision version acosf, asinf, atanf).
 -   Kernel    [2020-05-28] Support for C11's _Thread_local storage specifier
@@ -34,13 +577,13 @@ Open Source Release <next-release>
 -   Eva       [2020-05-20] Supports the ACSL mathematical operator \abs
 -   Kernel    [2020-05-18] Support for C11's _Noreturn function specifier
 
-###################################
+###############################################################################
 Open Source Release 21.1 (Scandium)
-###################################
+###############################################################################
 
-###################################
+###############################################################################
 Open Source Release 21.0 (Scandium)
-###################################
+###############################################################################
 
 -*  Doc       [2020-05-07] Fixes internal refs in generated pdfs (fixes #2505)
 -*  Kernel    [2020-05-04] Accept UCN-encoded unicode char in ACSL (fixes #@849)
@@ -120,9 +663,9 @@ o!  Kernel    [2020-02-04] Removed FCBuffer, FCMap and FCSet. Use directly
                 overrides the global option for the given functions;
               - via /*@ subdivide N; */ annotations on specific statements.
 
-##################################
+###############################################################################
 Open Source Release 20.0 (Calcium)
-##################################
+###############################################################################
 
 -   Eva       [2019-11-25] In the summary, fixes the number of alarms by
               category when the RTE plugin is used, and do not count logical
@@ -179,9 +722,9 @@ o!  Kernel    [2019-06-28] removes AST constructors TCoerce, TCoerceE,
               PLCoercion, PLCoercionE, Psubtype and PLsubtype
 -*  Kernel    [2019-06-20] fixes dangling ref when removing unused static local
 
-####################################
+###############################################################################
 Open Source Release 19.0 (Potassium)
-####################################
+###############################################################################
 
 -*  RTE       [2019-05-24] fixes a crash when visiting variable declarations
 -   Eva       [2019-04-19] The new annotation /*@ split exp; */ enumerates the
@@ -248,9 +791,9 @@ o   Kernel    [2018-12-11] New functions for retrieving major and minor version
 -*  Kernel    [2018-12-04] Fixes AST integrity check wrt volatile accesses
 -*  Kernel    [2018-11-21] Fixes #@553 - pretty-printing of basic asm template
 
-################################
+###############################################################################
 Open Source Release 18.0 (Argon)
-################################
+###############################################################################
 
 -!  Kernel    [2018-10-24] Log.error and Log.failure will eventually make
               Frama-C exit with a non-zero status. Fixes #@552
@@ -331,7 +874,7 @@ o!  Constant Propagation [2018-09-12] Removing Db API for Constant Propagation
 o!  Kernel    [2018-07-23] Remove completely outdated module Dataflow.
               Deprecated since 3+ years. Use Dataflow2 instead.
 -*  RTE       [2018-07-23] Stop generating spurious \initialized alarms.
-              Fixes #@429  
+              Fixes #@429
 -*  Kernel    [2018-07-06] Respect relative order of labels and ACSL annots.
               Fixes #@524
 o*  Ptests    [2018-07-02] Do not keep oracles for empty stderr. Fixes #@402
@@ -359,15 +902,15 @@ o*  Ptests    [2018-07-02] Do not keep oracles for empty stderr. Fixes #@402
               specific code annotations /*@ loop unroll N; */. The new strategy
               may affect analyses even without loop unrolling.
 
-############################################
+###############################################################################
 Open Source Release 17.1 (Chlorine-20180502)
-############################################
+###############################################################################
 
 -  Libc       [2018-07-05] Fix C++ compatibility for Frama-Clang plug-in
 
-############################################
+###############################################################################
 Open Source Release 17.0 (Chlorine-20180501)
-############################################
+###############################################################################
 
 -  Eva        [2018-04-25] Added scripts and templates to help automate case
               studies (in $FRAMAC_SHARE/analysis-scripts)
@@ -499,9 +1042,9 @@ o! Eva        [2017-11-09] The Fval module now supports NaN and infinite values.
 -* Eva        [2017-10-27] Fix bug in the handling of non-explicitly volatile
               fields inside volatile structs or unions
 
-##########################################
+###############################################################################
 Open Source Release 16.0 (Sulfur-20171101)
-##########################################
+###############################################################################
 
 -* Eva        [2017-10-27] Fix bugs when evaluating \ìnitialized, \dangling
               and \separated on addresses of bitfields
@@ -632,9 +1175,9 @@ o! Kernel     [2017-04-27] Completely separate types between Cil_types and
 -  Eva        [2017-04-06] More precise evaluation of \initialized and
               \dangling predicates.
 
-##############################################
+###############################################################################
 Open Source Release 15.0 (Phosphorus-20170501)
-##############################################
+###############################################################################
 
 -* Eva        [2017-05-08] Fix widening in the gauges domain, in particular with
               nested loops and pointers that change base address through
@@ -719,9 +1262,9 @@ o! Gui        [2017-03-10] Signature change for constructor
 o* Eva        [2016-10-22] Functions Db.Value.fun_set_args and
               Db.Value.globals_set_initial_state are now compatible with Eva.
 
-###########################################
+###############################################################################
 Open Source Release 14.0 (Silicon-20161101)
-###########################################
+###############################################################################
 
 -*! Eva       [2016-10-29] Fix soundness bug on statements with RTE or
               programmatically-added user assertions (bts #2258). This
@@ -832,7 +1375,7 @@ o! Kernel     [2016-06-14] Remove class Filecheck.check from API.
               translated as 'tmp = e;' instead of 'if (e) {}' (which was
               incorrect when e did not have a scalar type)
 -  Eva        [2016-05-27] Improvements to option -val-subdivide-non-linear for
-              high number of subdivisions 
+              high number of subdivisions
 -* Value      [2016-05-23] Option -val-show-initial-state has been removed.
               Instead, -value-msg-key=-initial-state can be used
 -  Value      [2016-05-23] New message key final-states, that can be used
@@ -868,9 +1411,9 @@ o  Makefile   [2016-03-31] Warnings and warn-error are activated only if a file
 o! Kernel     [2016-03-29] Functions Integer.pgcd and Integer.ppcm are now
               guaranteed to return a positive result.
 
-#############################################
+###############################################################################
 Open Source Release 13.0 (Aluminium-20160502)
-#############################################
+###############################################################################
 
 -  Value      [2016-04-19] Support for evaluation of predicate
               \valid_read_string on constant strings.
@@ -1043,9 +1586,9 @@ o  Ptests     [2015-07-29] New EXEC: directive.
 -  Kernel     [2015-07-01] New option -remove-projects.
 -  Kernel     [2015-06-30] New option -set-project-as-default.
 
-#############################################
+###############################################################################
 Open Source Release 12.0 (Magnesium-20151002)
-#############################################
+###############################################################################
 
 o! Kernel     [2016-01-03] Modules Dataflow is deprecated, and will be removed
               in Aluminium. Module Dataflow2 offers a very similar but simpler
@@ -1267,9 +1810,9 @@ o! Kernel     [2015-30-01] Fixed bug #!2012 about combining
               subdividing may avoid the emission of an alarm.
 -  Value      [2015-01-21] Support for \subset predicate.
 
-##########################################
+###############################################################################
 Open Source Release 11.0 (Sodium-20150201)
-##########################################
+###############################################################################
 
 -  Kernel     [2015-02-01] Tests are added to the distrib (make tests).
 -* Logic      [2015-02-09] The ACSL parser accepts qualifiers in logic C types.
@@ -1487,9 +2030,9 @@ o  Logic      [2014-03-04] Annotations.{iter,fold}_all_code_annot are now
 -* Configure   [2014-03-10] fix for autoconf < 2.67 when checking ability
                of default pre-processor to keep comments
 
-########################################
+###############################################################################
 Open Source Release 10.0 (Neon-20140301)
-########################################
+###############################################################################
 
 -* Value      [2014-03-04] Fix bug when writing imprecisely in a struct
               containing a 1-bit wide bitfield (bug #!1671)
@@ -1858,15 +2401,15 @@ o! Value      [2013-05-03] Remove functions Cvalue.Model.pretty_without_null and
               reference to the real function. Removed last argument of
               Cvalue.Model.pretty_filter.
 
-###########################################
+###############################################################################
 Open Source Release 9.2 (Fluorine-20130601)
-###########################################
+###############################################################################
 
 -* Value      [2013-06-11] Add missing C library files.
 
-###########################################
+###############################################################################
 Open Source Release 9.1 (Fluorine-20130501)
-###########################################
+###############################################################################
 
 -  Value      [2013-05-22] Better precision for ^ (bitwise xor) operator
               when applied on intervals of positive integers
@@ -1879,9 +2422,9 @@ o* Kernel     [2013-05-06] Fixed Type.pp_ml_name for polymorphic types
 -* Makefile   [2013-05-06] Fixed installation directory of the doc in
               plug-in's Makefile (bug #1278).
 
-###########################################
+###############################################################################
 Open Source Release 9.0 (Fluorine-20130401)
-###########################################
+###############################################################################
 
 o! Cil        [2013-04-11] Remove Cil pretty-printer. Use module Printer
               instead. The script bin/oxygen2fluorine.sh may be used to
@@ -2137,9 +2680,9 @@ o  Kernel     [2012-09-20] Provide Datatype.triple and Datatype.quadruple
 o* Kernel     [2012-09-20] Fixed consistency check of descriptor when
               building polymorphic datatypes (fixed bts #1277).
 
-#########################################
+###############################################################################
 Open Source Release 8.0 (Oxygen-20120901)
-#########################################
+###############################################################################
 
 -! Kernel     [2012-09-17] Remove useless negative options -no-help,
               -no-version, -no-print-share-path, -no-print-lib-path and
@@ -2518,9 +3061,9 @@ o! Kernel     [2011-10-18] Logic_preprocess.file takes an additional parameter,
               completely invalid. Soundness was not affected (the
               alarm for whatever made e invalid was present).
 
-###########################################
+###############################################################################
 Open Source Release 7.0 (Nitrogen-20111001)
-###########################################
+###############################################################################
 
 -  Rte        [2011-10-07] No longer position 'Don't know' statuses
 -  Value      [2011-10-07] New alarm for left shift of negative values.
@@ -2972,9 +3515,9 @@ o  Cil/Logic  [2011-02-16] New functions Clexer.is_c_keyword and
 -* Value      [2011-02-09] Changes related to 0., +0., -0., sort of thing.
               Unwarranted loss of precision fixed.
 
-#########################################
+###############################################################################
 Open Source Release 6.2 (Carbon-20110201)
-#########################################
+###############################################################################
 
 -  WP         [2011-02-07] Plug-in WP removed from kernel-releases (now an
               independent plug-in).
@@ -3085,17 +3628,17 @@ o* Cil        [2010-12-20] Fixed bug #645. Ast_info.constant_expr,
               ~loc:Cil_datatype.Location.unknown which is most of the time
               not accurate.
 
-#########################################
+###############################################################################
 Open Source Release 6.1 (Carbon-20101202)
-#########################################
+###############################################################################
 
 -* WP         [2010-12-16] Fixed bug #639: no more Coq compilation to shared
               directory.
 - WP          [2010-12-16] Accessibility of all provers from gui.
 
-#########################################
+###############################################################################
 Open Source Release 6.0 (Carbon-20101201)
-#########################################
+###############################################################################
 
 -! Kernel     [2010-12-13] Fixed bug #548: limit.h now syntactically correct.
               Architectures other than x86_32 still unsupported.
@@ -3296,9 +3839,9 @@ o! Kernel     [2010-04-22] Ptmap (resp. Ptset) is renamed into Hptmap (Hptset)
 +  Logic      [2010-04-13] #!346 Formals have an \old label when used in post
               conditions
 
-########################################
+###############################################################################
 Open Source Release 5.0 (Boron-20100401)
-########################################
+###############################################################################
 
 -  Kernel     [2010-04-12] Preliminary standard C library in $FRAMAC_SHARE/libc
 o* Cil        [2010-04-12] New hook after Cabs elaboration (fix bug #!446)
@@ -3467,9 +4010,9 @@ o! Cil        [2009-09-28] pAssigns now prints directly a whole list of assigns
 -  Value      [2009-09-25] Improved treatment of "assigns p[..]" clauses
               in -input
 
-############################################
+###############################################################################
 Open Source Release 4.2 (Beryllium-20090902)
-############################################
+###############################################################################
 
 -* Obfuscator [2009-09-23] obfuscator does not lose links between logic
               and C variables anymore (bts #250).
@@ -3519,9 +4062,9 @@ o* Makefile   [2009-09-18] Fixed bugs with the use of PLUGIN_EXTRA_BYTE
               which does not support native dynlink and with ocaml >= 3.11
               (bts #224).
 
-############################################
+###############################################################################
 Open Source Release 4.1 (Beryllium-20090901)
-############################################
+###############################################################################
 
 -! Syntactic_callgraph [2009-08-27] New design of the callgraph in the GUI.
               Frama-C now requires ocamlgraph 1.2.
@@ -3564,9 +4107,9 @@ o! Cil        [2009-06-24] Added 2 components to Cil_types.typ to optimize
 -* Kernel     [2009-06-24] Restore compatibility with ocaml 3.10.2
 -* Configure  [2009-06-24] Fixed bug with --disable-gui in configure.in
 
-############################################
+###############################################################################
 Open Source Release 4.0 (Beryllium-20090601)
-############################################
+###############################################################################
 
 o  Value      [2009-06-23] New constructor Signed_overflow_alarm for type
               Alarms.t
@@ -3756,9 +4299,9 @@ o! Kernel     [2009-01-05] Some changes in API of module Type
 -  Value      [2008-12-18] Improved support for state reduction on a
               memory read.
 
-##########################################
+###############################################################################
 Open Source Release 3.1 (Lithium-20081201)
-##########################################
+###############################################################################
 
 -! GUI        [2008-12-09] Improved consistency of some information messages.
 -  Value      [2008-12-09] Abstract structs are now supported in
@@ -3803,9 +4346,9 @@ o  Cil        [2008-11-17] New methods for visiting compinfo, enuminfo,
 o  Makefile   [2008-11-03] Support for native compilation in Makefile.template
               (require ocaml >= 3.11).
 
-##########################################
+###############################################################################
 Open Source Release 3.0 (Lithium-20081002)
-##########################################
+###############################################################################
 
 -! Value      [2008-10-23] Changed behavior of option
               -context-valid-pointers to make it more like the
@@ -3865,9 +4408,9 @@ o! Kernel     [2008-09-11] Refined UnspecifiedSequence information.
 o! Cil        [2008-07-17] AST changes for unspecified sequences (experimental).
 -* Jessie     [2008-07-16] Fixed path problems with binary distributions.
 
-#########################################
+###############################################################################
 Open Source Release 2.0 (Helium-20080701)
-#########################################
+###############################################################################
 
 -  Occurrence [2008-07-11] Occurrences of a variable can be computed from
               any occurrence of the program (not only from its declaration).
@@ -3936,17 +4479,17 @@ o! Logic      [2008-06-24] AST changes for invariants.
 -* Kernel     [2008-06-03] Correct promotion rules from bitfields to integers.
 -* Kernel     [2008-06-02] -machdep was ignored (bts #?309).
 
-###########################################
+###############################################################################
 Open Source Release 1.2 (Hydrogen-20080502)
-###########################################
+###############################################################################
 
 o* Makefile   [2008-05-21] Fixed bug in "make clean-doc" (and "make distclean").
 -  GUI        [2008-05-19] All internal options are available in the GUI
               preferences pannel.
 
-###########################################
+###############################################################################
 Open Source Release 1.1 (Hydrogen-20080501)
-###########################################
+###############################################################################
 
 -! Value      [2008-04-24] Display a warning whenever an uninitialized value
               causes the death of a branch.
@@ -3972,9 +4515,9 @@ o  GUI        [2008-04-07] Project management redesigned for older Gtk and
 -* Kernel     [2008-04-01] Various Win32 path fixes.
 -  Kernel     [2008-04-01] Option -no-unicode : do not print Unicode chars.
 
-######################################
+###############################################################################
 Binary Release 1.0 (Hydrogen-20080302)
-######################################
+###############################################################################
 
 -  Occurrence [2008-03-17] New option -occurrence.
 -  Occurrence [2008-03-17] First release of the plug-in.
@@ -3984,9 +4527,9 @@ Binary Release 1.0 (Hydrogen-20080302)
 -* Project    [2008-03-14] Fixed bug with checksum computation during save/load.
 -* Slicing    [2008-02-25] Fixed bug in interprocedural slicing (bts #?201).
 
-###########################################
+###############################################################################
 Open Source Release 1.0 (Hydrogen-20080301)
-###########################################
+###############################################################################
 
 -  Kernel     [2008-03-01] First release.
 

INSTALL.md

@@ -7,7 +7,10 @@
         - [Installing Frama-C from opam repository](#installing-frama-c-from-opam-repository)
         - [Installing Custom Versions of Frama-C](#installing-custom-versions-of-frama-c)
         - [Installing Frama-C on Windows via WSL](#installing-frama-c-on-windows-via-wsl)
-        - [Installing Frama-C on macOS](#installing-frama-c-on-mac-os)
+        - [Installing Frama-C on macOS](#installing-frama-c-on-macos)
+    - [Installing Ivette via the online packages](#installing-ivette-via-the-online-packages)
+        - [On Linux](#installing-ivette-via-the-online-packages-on-linux)
+        - [On macOS](#installing-ivette-via-the-online-packages-on-macos)
     - [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)
@@ -19,8 +22,9 @@
         - [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)
+        - [Man files: (in `/INSTALL_DIR/share/man/man1`)](#man-files-in-install_dirsharemanman1)
 - [Installing Additional Frama-C Plugins](#installing-additional-frama-c-plugins)
+- [Frama-C additional tools](#frama-c-additional-tools)
     - [HAVE FUN WITH FRAMA-C!](#have-fun-with-frama-c)
 
 ## Installing Frama-C via opam
@@ -34,42 +38,57 @@ First you need to install opam, then you may install Frama-C using opam.
 
 Several Linux distributions already include an `opam` package.
 
-**Note:** make sure your opam version is >= 2.0.0.
-
 macOS has opam through Homebrew.
 
 Windows users can install opam via WSL (Windows Subsystem for Linux).
 
-If your system does not have an opam package >= 2.0.0, you can
-[compile it from source](#compiling-from-source),
-or use the provided opam binaries available at:
+If your system does not have an opam package, you can use the provided
+opam binaries available at:
 
 http://opam.ocaml.org/doc/Install.html
 
-### Installing Frama-C from opam repository
+Note: the `opam` binary itself is very small, but the initialization of an
+*opam switch* usually takes time and disk space, since it downloads and builds
+an OCaml compiler. Please refer to the opam documentation for details.
 
-The 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`.
+### Installing Frama-C (including dependencies) via opam
 
-`frama-c` has some 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
+The Frama-C package in opam is called `frama-c`. It includes:
+- the command-line `frama-c` executable;
+- the graphical interface, `frama-c-gui` (in supported systems);
+- `ivette`, Frama-C's new Electron-based GUI.
 
-    # install Frama-C's dependencies
-    opam install depext
-    opam depext frama-c
+Note: Ivette's dependencies are _not_ included in the opam package,
+but downloaded from `npm` when the user runs `ivette` for the first time.
 
-will install the appropriate system packages (this of course requires
-administrator rights on the system).
+`frama-c` has some non-OCaml dependencies, such as GMP. opam includes
+a mechanism (`depext`) to handle such dependencies. It may require
+administrative rights to install system packages (e.g. `libgmp`).
 
-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 [Gitlab issue](https://git.frama-c.com/pub/frama-c/issues/new))
-so that we can add it to the Frama-C `depext` package.
+If your `opam` version is >= 2.1, such dependencies are installed
+automatically when installing `frama-c` itself:
 
-    # install Frama-C
-    opam install frama-c
+```shell
+# install Frama-C and dependencies with opam >= 2.1
+opam install frama-c
+```
+
+If your opam version is < 2.1, you need to install `depext` first, then
+use it to install Frama-C's dependencies:
+
+```shell
+# install Frama-C's dependencies with pre-2.1 opam
+opam install depext
+opam depext frama-c
+# then install Frama-C itself
+opam install frama-c
+```
+
+If there are errors due to missing external dependencies, opam usually emits a
+message indicating which packages to install. If this is not sufficient,
+there may be missing dependencies in opam's packages for your system. In this
+case, you may [create a Gitlab issue](https://git.frama-c.com/pub/frama-c/issues/new)
+indicating your distribution and error message.
 
 ### Configuring provers for Frama-C/WP
 
@@ -85,35 +104,39 @@ Actually, you can use any prover supported by Why3 in combination with Frama-C/W
 Most provers are available on all platforms. After their installation,
 Why3 must be configured to make them available for Frama-C/WP:
 
-    ```shell
-    why3 config --detect
-    ```
+```shell
+why3 config detect
+```
 
 ### Reference configuration
 
 See file [reference-configuration.md](reference-configuration.md)
-for a set of packages that is known to work with Frama-C 21 (Scandium).
+for a set of packages that is known to work with this version of Frama-C.
 
 ### Installing Custom Versions of Frama-C
 
 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
+you can still use opam to install Frama-C's dependencies and compile your
 own sources directly:
 
-    # optional: remove the standard frama-c package if it was installed
-    opam remove --force frama-c
+```shell
+# optional: remove the standard frama-c package if it was installed
+opam remove --force frama-c
 
-    # install Frama-C's dependencies
-    opam install depext
-    opam depext frama-c
-    opam install --deps-only frama-c
+# install Frama-C's dependencies
+opam install depext # only for opam < 2.1.0
+opam depext frama-c # only for opam < 2.1.0
+opam install --deps-only frama-c [--with-test]
 
-    # install custom version of frama-c
-    opam pin add --kind=path frama-c <dir>
+# install custom version of frama-c
+opam pin add --kind=path frama-c <dir>
+```
 
 where `<dir>` is the root of your unpacked Frama-C archive.
-See `opam pin` for more details.
+See `opam pin` for more details. The option `--with-test` is optional and
+is necessary only if you want to be able to execute the tests available in
+the frama-c repository.
 
 If your extensions require other libraries than the ones already used
 by Frama-C, they must of course be installed as well.
@@ -121,103 +144,109 @@ by Frama-C, they must of course be installed as well.
 ### Installing Frama-C on Windows via WSL
 
 Frama-C is developed on Linux, but it can be installed on Windows using the
-following tools:
+Windows Subsystem for Linux (WSL).
 
-- Windows Subsystem for Linux
-- VcXsrv (X server for Windows)
+**Note**: if you have WSL2 (Windows 11), you can run the graphical interface
+          directly, thanks to WSLg. If you are using WSL 1, you need to install
+          an X server for Windows, such as VcXsrv
+          (see section "Running the Frama-C GUI on WSL").
 
 #### Prerequisites: WSL + a Linux distribution
 
-For enabling WSL on Windows, you may follow these instructions
-(we tested with Ubuntu 18.04 LTS;
+To enable WSL on Windows, you may follow these instructions
+(we tested with Ubuntu 20.04 LTS;
 other distributions/versions should also work,
 but the instructions below may require some modifications).
 
-https://docs.microsoft.com/en-us/windows/wsl/install-win10
-
-Note: older builds of Windows 10 and systems without access to the
-      Microsoft Store may have no compatible Linux packages.
+https://docs.microsoft.com/en-us/windows/wsl/install
 
-##### PowerShell-based quick guide
+Notes:
 
-This is a quick guide based on running a PowerShell with administrator rights.
-Note that, depending on your build version of Windows 10, the Ubuntu package
-selected below may not work. If you are unsure, follow the above instructions
-from the Microsoft website.
-
-Inside PowerShell, run the following command to activate Windows Subsystem for Linux:
-
-```
-Enable-WindowsOptionalFeature -Online -FeatureName Microsoft-Windows-Subsystem-Linux
-```
-
-Then, reboot the operating system.
-
-After rebooting, run again the PowerShell terminal with administrator rights.
-Move to your user directory, download the distribution and install it:
-
-```
-cd C:\Users\<Your User Directory>
-Invoke-WebRequest -Uri https://aka.ms/wsl-ubuntu-1804 -OutFile Ubuntu.appx -UseBasicParsing
-Add-AppxPackage .\Ubuntu.appx
-```
-
-Ubuntu should now be available in the Windows menu. Run it and follow the
-instructions to create a user.
+- older builds of Windows 10 and systems without access to the
+  Microsoft Store may have no compatible Linux packages.
+- in WSL 1, Frama-C/WP cannot use Why3 because of some missing features in WSL
+  support, thus using WSL 2 is **highly recommended**.
 
 #### Installing opam and Frama-C on WSL
 
-For installing opam, some packages are required. The following commands can be
+To install opam, some packages are required. The following commands can be
 run to update the system and install those packages:
 
-```
-sudo add-apt-repository -y ppa:avsm/ppa # unnecessary for Ubuntu 20.04
+```shell
 sudo apt update
 sudo apt upgrade
-sudo apt install make m4 gcc opam
+sudo apt install make m4 gcc opam gnome-icon-theme
 ```
 
 Then opam can be set up using these commands:
 
-```
-opam init --disable-sandboxing -c 4.05.0 --shell-setup
+```shell
+opam init --disable-sandboxing --shell-setup
 eval $(opam env)
 opam install -y depext
 ```
 
-Now, for installing Frama-C, run the following commands that will use `apt` to
+You can force a particular Ocaml version during `opam init` by using the option
+`-c <version>` if needed. For instance, you can try installing the OCaml version
+mentioned in the [reference configuration](reference-configuration.md).
+
+Now, to install Frama-C, run the following commands, which will use `apt` to
 install the dependencies of the opam packages and then install them:
 
-```
+```shell
 opam depext --install -y lablgtk3 lablgtk3-sourceview3
 opam depext --install -y frama-c
 ```
 
 #### Running the Frama-C GUI on WSL
 
-Microsoft WSL does not support graphical user interfaces directly. If you want
-to run Frama-C's GUI, you need to install an X server, such as VcXsrv or
-Cygwin/X. We present below how to install VcXsrv.
+If you have WSL2: a known issue with some versions of Frama-C, lablgtk3 and
+Wayland requires prefixing the command running the Frama-C GUI with
+`GDK_BACKEND=x11`, as in:
+
+```shell
+GDK_BACKEND=x11 frama-c-gui <options>
+```
+
+If you have WSL 1: WSL 1 does not support graphical user interfaces directly.
+If you want to run Frama-C's GUI, you need to install an X server,
+such as VcXsrv or Cygwin/X. We present below how to install VcXsrv.
 
 First, install VcXsrv from:
 
 https://sourceforge.net/projects/vcxsrv/
 
 The default installation settings should work.
-Now run it from the Windows menu (it is named XLaunch).
-On the first configuration screen, select "Multiple Windows". On the
-second, keep "Start no client" selected. On the third configuration step, add an
-additional parameter `-nocursor` in the field "Additional parameters for
-VcXsrv". You can save this configuration at the last step if you want, before
-clicking "Finish".
 
-Once it is done, the Xserver is ready. From WSL, run:
+Now run VcXsrv from the Windows menu (it is named XLaunch), the firewall
+must authorize both "Public" and "Private" domains. On the first configuration
+screen, select "Multiple Windows". On the second:
 
-```
+- keep "Start no client" selected,
+- keep "Native opengl" selected,
+- select "Disable access control".
+
+Now specific settings must be provided in WSL. you can put the export commands
+in your `~/.bashrc` file, so this is done automatically when starting WSL.
+
+##### WSL 1
+
+The Xserver is ready. From WSL, run:
+
+```shell
+export LIBGL_ALWAYS_INDIRECT=1
 export DISPLAY=:0
 frama-c-gui
 ```
 
+##### WSL 2
+
+```shell
+export LIBGL_ALWAYS_INDIRECT=1
+export DISPLAY=$(cat /etc/resolv.conf | grep nameserver | awk '{print $2; exit;}'):0.0
+frama-c-gui
+```
+
 ### Installing Frama-C on macOS
 
 [opam](https://opam.ocaml.org) works perfectly on macOS via
@@ -227,44 +256,100 @@ We highly recommend to rely on it for the installation of Frama-C.
 1. Install *required* general macOS tools for OCaml:
 
     ```shell
-    brew install autoconf pkg-config opam
+    brew install opam
     ```
 
-   Do not forget to `opam init` and ``eval `opam config env` `` for a proper
+   Do not forget to `opam init` and `eval $(opam env)` for a proper
    opam installation (if not already done before).
 
 2. Set up a compatible OCaml version (replace `<version>` with the version
-   indicated in the 'recommended working configuration' section):
+   indicated in the [reference configuration](#reference-configuration)):
 
     ```shell
     opam switch create <version>
     ```
 
-3. Install *required* dependencies for Frama-C:
+3. Install Frama-C:
 
     ```shell
-    brew install gmp gtk+ gtksourceview libgnomecanvas
+    opam install frama-c
     ```
 
-    The graphical libraries require additional manual configuration of your
-    bash profile. Consult this [issue](https://github.com/ocaml/opam-repository/issues/13709) on opam
-    for details. A known working configuration is:
+   Opam may ask for the administrator password to handle required system
+   dependencies.
+
+   **It is likely that, at this point, opam will fail due to some Homebrew
+   packages and pkg-config.** The error messages should indicate what you need
+   to do, e.g.:
 
     ```shell
-    export PKG_CONFIG_PATH=/usr/local/opt/libffi/lib/pkgconfig:/usr/local/opt/libxml2/lib/pkgconfig:/usr/local/lib/pkgconfig
+    For pkg-config to find zlib you may need to set:
+      export PKG_CONFIG_PATH="/usr/local/opt/zlib/lib/pkgconfig"
     ```
 
-4. Install *recommended* dependencies for Frama-C:
+    After setting such environment variables, re-running `opam install frama-c`
+    should work. If you still have issues, try manually installing the required
+    packages (via `brew install <package>`) and then re-installing Frama-C.
+    **Note**: opam packages prefixed with `conf-` only check if the
+    corresponding system package is findable. If you cannot install some
+    `conf-` package, the solution will likely involve Homebrew and/or setting
+    environment variables, not opam.
 
-    ```shell
-    brew install graphviz
-    ```
+4. Install the new Frama-C graphical interface (Ivette).
 
-5. Install Frama-C:
+   **The traditional GTK-based Frama-C GUI no longer works on macOS!**
 
-    ```shell
-    opam install frama-c
-    ```
+   You need to use Ivette, the new Frama-C graphical interface.
+   Instructions on installing and running it are presented by opam when
+   the `frama-c` package is installed. Follow them to get Ivette running.
+
+## Installing Ivette via the online packages
+
+**Warning:** if you already have an `ivette` script along with `frama-c`, that
+script is used for bootstrapping the installation of Ivette from source through
+your internet connection.  The instructions provided here are intended to
+_replace_ the installation procedure from source. Hence, it is highly
+recommended for you to remove the bootstrapping `ivette` script if you want to
+use the binary distribution of Ivette.
+
+Only stable distributions are available online for now.
+Download the Ivette distribution that corresponds to your version of Frama-C,
+following the appropriate link from this page: https://frama-c.com/html/framac-versions.html
+
+### Installing Ivette via the online packages on Linux
+
+Requirement: libfuse2 must be installed.
+
+Download the binary distribution (for now, only x86-64 and ARM64 are supported).
+Install it wherever you want:
+
+```sh
+cp frama-c-ivette-linux-<arch>-<version>.AppImage <IVETTE-INSTALL-PATH>/ivette.AppImage
+```
+
+Then add an alias `ivette` that just runs the AppImage:
+
+```sh
+alias ivette=<ABSOLUTE-IVETTE-INSTALL-PATH>/ivette.AppImage
+```
+
+### Installing Ivette via the online packages on macOS
+
+Download the universal binary distribution of Ivette and install it, typically
+in `/Applications/Ivette.app`. To launch Ivette from the command line, you will
+need your own `ivette` script, like the following one:
+
+```sh
+#! /usr/bin/env sh
+exec open -na <IVETTE-INSTALL>/Ivette.app --args\
+  --command <FRAMAC-INSTALL>/frama-c\
+  --working $PWD $*
+```
+
+Simply replace `<IVETTE-INSTALL>` and `<FRAMAC-INSTALL>` in the code above with
+the (absolute) paths to your `Ivette.app` and `frama-c` binaries,
+respectively. Then, make your `ivette` script executable and simply use it like
+the `frama-c` command-line binary!
 
 ## Installing Frama-C via your Linux distribution (Debian/Ubuntu/Fedora)
 
@@ -301,12 +386,14 @@ Arch Linux: `pikaur -S frama-c`
 1. Install [opam](http://opam.ocaml.org/) and use it to get all of Frama-C's
    dependencies (including some external ones):
 
-        opam install depext
-        opam depext frama-c
-        opam install --deps-only frama-c
+   ```shell
+   opam install depext # only for opam < 2.1.0
+   opam depext frama-c # only for opam < 2.1.0
+   opam install --deps-only frama-c
+   ```
 
    If not using [opam](http://opam.ocaml.org/), you will need to install
-   the Frama-C dependencies by yourself. The `opam/opam` file in the Frama-C
+   the Frama-C dependencies by yourself. The `opam` file in the Frama-C
    .tar.gz lists the required dependencies (e.g. `ocamlfind`, `ocamlgraph`,
    `zarith`, etc.). A few of these dependencies are optional, only required
    for the graphical interface: `lablgtk`, `conf-gnomecanvas` and
@@ -314,69 +401,89 @@ Arch Linux: `pikaur -S frama-c`
 
 2. On Linux-like distributions:
 
-        ./configure && make && sudo make install
+   ```shell
+   make RELEASE=yes && make install
+   ```
 
-    See section *Configuration* below for options.
+   See section *Installation* below for options.
 
 3. On Windows+Cygwin:
 
-        ./configure --prefix="$(cygpath -a -m <installation path>)" && make && make install
-
-4. The binary `frama-c` (and `frama-c-gui` if you have lablgtk2) is now installed.
+   ```shell
+   make RELEASE=yes && make install
+   ```
 
 ### Full Compilation Guide
 
 #### Frama-C Requirements
 
-See the `opam/opam` file, section `depends`, for compatible OCaml versions and
+See the `opam` file, section `depends`, for compatible OCaml versions and
 required dependencies (except for those related to `lablgtk`, which are
 required for the GUI but otherwise optional).
 
-Section `deptops` lists optional dependencies.
-
-#### Configuration
-
-Frama-C is configured by `./configure [options]`.
+To install the required dependencies, you can use opam v2.1
+or higher to do the following (assuming you are in frama-c
+root source folder):
 
-`configure` is generated by `autoconf`, so that the standard options for setting
-installation directories are available, in particular `--prefix=/path`.
+1. `opam switch create frama-c ocaml-base-compiler.4.14.2`
+   to create a compatible opam switch
+2. `opam pin . -n` to pin to the latest development version
+3. `opam install --deps-only .` will fetch and build all
+   relevant dependencies
 
-A plugin can be enabled by `--enable-plugin` and disabled by `--disable-plugin`.
-By default, all distributed plugins are enabled, unless some optional
-dependencies are not met.
-
-See `./configure --help` for the current list of plugins, and available options.
+#### Compilation
 
-##### Under Cygwin
+There are basically two compilation modes: development and release.
 
-Use `./configure --prefix="$(cygpath -a -m <installation path>)"`.
+Typing `make` builds in development mode, this is a shortcut for:
+```shell
+dune build @install
+```
 
-(using Unix-style paths without the drive letter will probably not work)
+Typing `make RELEASE=yes` builds in release mode, this is a shortcut for:
+```shell
+dune build @install --release --promote-install-files=false
+```
 
+For more precise build configurations, use directly the `dune` command.
 
-#### Compilation
+#### Testing
 
-Type `make` (you can use `-j` for parallelization).
-
-Some Makefile targets of interest are:
-- `doc`      generates the API documentation.
-- `oracles`  sets up the Frama-C test suite oracles for your own configuration.
-- `tests`    performs Frama-C's own tests.
+Basic tests can be executed using:
 
+```shell
+make run-ptests
+make default-tests
+```
 
 #### Installation
 
-Type `make install`
-(depending on the installation directory, this may require superuser
-privileges. The installation directory is chosen through `--prefix`).
+Type `make install` (depending on the installation directory, this may require
+superuser privileges. The installation directory is chosen through the variable
+`PREFIX`). This is a shortcut for:
+
+```shell
+dune install
+```
 
+Makefile (and dune) support the `DESTDIR` variable, which can be used to
+configure the location of the installation.
 
 #### API Documentation
 
 For plugin developers, the API documentation of the Frama-C kernel and
-distributed plugins is available in the file `frama-c-api.tar.gz`, after running
-`make doc-distrib`.
+distributed plugins is available in the `_build/default/_doc/_html` directory
+after running:
+
+```shell
+make doc
+```
 
+or:
+
+```shell
+dune build @doc
+```
 
 #### Uninstallation
 
@@ -391,20 +498,24 @@ This step is optional.
 
 Download some test files:
 
-    export PREFIX_URL="https://git.frama-c.com/pub/frama-c/raw/master/tests/value"
-    wget -P test ${PREFIX_URL}/CruiseControl.c
-    wget -P test ${PREFIX_URL}/CruiseControl_const.c
-    wget -P test ${PREFIX_URL}/CruiseControl.h
-    wget -P test ${PREFIX_URL}/CruiseControl_extern.h
-    wget -P test ${PREFIX_URL}/scade_types.h
-    wget -P test ${PREFIX_URL}/config_types.h
-    wget -P test ${PREFIX_URL}/definitions.h
+```shell
+export PREFIX_URL="https://git.frama-c.com/pub/frama-c/raw/master/tests/value"
+wget -P test ${PREFIX_URL}/CruiseControl.c
+wget -P test ${PREFIX_URL}/CruiseControl_const.c
+wget -P test ${PREFIX_URL}/CruiseControl.h
+wget -P test ${PREFIX_URL}/CruiseControl_extern.h
+wget -P test ${PREFIX_URL}/scade_types.h
+wget -P test ${PREFIX_URL}/config_types.h
+wget -P test ${PREFIX_URL}/definitions.h
+```
 
 Then test your installation by running:
 
-    frama-c -eva test/CruiseControl*.c
-    # or (if frama-c-gui is available)
-    frama-c-gui -eva test/CruiseControl*.c
+```shell
+frama-c -eva test/CruiseControl*.c
+# or (if ivette is available)
+ivette -eva test/CruiseControl*.c
+```
 
 # Available resources
 
@@ -415,27 +526,21 @@ available:
 
 - `frama-c`
 - `frama-c-gui`       if available
-- `frama-c-config`    displays Frama-C configuration paths
-- `frama-c.byte`      bytecode version of frama-c
-- `frama-c-gui.byte`  bytecode version of frama-c-gui, if available
-- `ptests.opt`        testing tool for Frama-c
-- `frama-c-script`    utilities related to analysis parametrization
+- `frama-c-config`    lightweight wrapper used to display configuration paths
+- `frama-c-ptests`    testing tool for Frama-c
+- `frama-c-wtests`    testing tool for Frama-c
+- `frama-c-script`    utilities related to e.g. analysis parametrization
+- `ivette`            new graphical interface
 
 ## Shared files: (in `/INSTALL_DIR/share/frama-c` and subdirectories)
 
-- some `.h` and `.c` files used as preludes by Frama-C
 - some `Makefiles` used to compile dynamic plugins
-- some `.rc` files used to configure Frama-C
 - some image files used by the Frama-C GUI
 - some files for Frama-C/plug-in development (autocomplete scripts,
   Emacs settings, scripts for running Eva, ...)
 - an annotated C standard library (with ACSL annotations) in `libc`
 - plugin-specific files (in directories `wp`, `e-acsl`, etc.)
 
-## Documentation files: (in `/INSTALL_DIR/share/frama-c/doc`)
-
-- files used to generate dynamic plugin documentation
-
 ## Object files: (in `/INSTALL_DIR/lib/frama-c`)
 
 - object files used to compile dynamic plugins
@@ -455,10 +560,38 @@ Plugins may be released independently of Frama-C.
 
 The standard way for installing them should be:
 
-    ./configure && make && make install
+```shell
+dune build @install && dune install
+```
 
 Plugins may have their own custom installation procedures.
 Consult their specific documentation for details.
 
+# Frama-C additional tools
+
+A few additional tools that are unnecessary for most users might be useful for
+plugin developers. These tools are:
+- `frama-c-lint`, used for checking coding conventions
+- `frama-c-hdrck`, used for checking file license headers
+
+They can be installed either by pinning them via Opam:
+
+```shell
+opam pin tools/lint
+opam pin tools/hdrck
+```
+
+Or by compiling/installing Frama-C manually in developer mode:
+```shell
+FRAMAC_DEVELOPER=yes make
+FRAMAC_DEVELOPER=yes make install
+
+# Or:
+make -C tools/<the-tool>
+make -C tools/<the-tool> install
+```
+
+For convenience, `FRAMAC_DEVELOPER` can be exported globally.
+
 
 # HAVE FUN WITH FRAMA-C!

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

@@ -2,7 +2,7 @@
 #                                                                        #
 #  This file is part of Frama-C.                                         #
 #                                                                        #
-#  Copyright (C) 2007-2020                                               #
+#  Copyright (C) 2007-2025                                               #
 #    CEA (Commissariat à l'énergie atomique et aux énergies              #
 #         alternatives)                                                  #
 #                                                                        #
@@ -22,2521 +22,150 @@
 
 # This file is the main makefile of Frama-C.
 
-FRAMAC_SRC=.
 MAKECONFIG_DIR=share
-PLUGIN_TESTS_LIST:=
-include share/Makefile.common
-include share/Makefile.dynamic_config.internal
+FRAMAC_DEVELOPER?=
 
-#Check share/Makefile.config available
-ifndef FRAMAC_ROOT_SRCDIR
-$(error \
-  "You should run ./configure first (or autoconf if there is no configure)")
-endif
-
-###################
-# Frama-C Version #
-###################
-
-VERSION:=$(shell $(CAT) VERSION)
-VERSION_CODENAME:=$(shell $(CAT) VERSION_CODENAME)
-
-###########################
-# Global plugin variables #
-###########################
-
-# the directory where compiled plugin non-GUI files are stored
-PLUGIN_TOP_LIB_DIR= $(PLUGIN_LIB_DIR)/top
-
-# the directory where compiled plugin GUI files are stored
-PLUGIN_GUI_LIB_DIR= $(PLUGIN_LIB_DIR)/gui
-
-# the directory where the other Makefiles are
-FRAMAC_SHARE	= share
+include $(MAKECONFIG_DIR)/Makefile.common
 
-# Shared lists between Makefile.plugin and Makefile :
-# initialized them as "simply extended variables" (with :=)
-# for a correct behavior of += (see section 6.6 of GNU Make manual)
-PLUGIN_LIST	:=
-PLUGIN_GENERATED_LIST:=
-PLUGIN_CMO_LIST	:=
-PLUGIN_CMX_LIST	:=
-PLUGIN_META_LIST :=
-PLUGIN_DYN_CMI_LIST :=
-PLUGIN_DYN_CMO_LIST :=
-PLUGIN_DYN_CMX_LIST :=
-PLUGIN_INTERNAL_CMO_LIST:=
-PLUGIN_INTERNAL_CMX_LIST:=
-PLUGIN_GUI_CMO_LIST:=
-PLUGIN_GUI_CMX_LIST:=
-PLUGIN_DYN_DEP_GUI_CMO_LIST:=
-PLUGIN_DYN_DEP_GUI_CMX_LIST:=
-PLUGIN_DYN_GUI_CMO_LIST :=
-PLUGIN_DYN_GUI_CMX_LIST :=
-PLUGIN_TYPES_CMO_LIST :=
-PLUGIN_TYPES_CMX_LIST :=
-PLUGIN_DEP_LIST:=
-PLUGIN_DOC_LIST :=
-PLUGIN_DOC_DIRS :=
-PLUGIN_DISTRIBUTED_LIST:=
-PLUGIN_DIST_TARGET_LIST:=
-PLUGIN_DIST_DOC_LIST:=
-PLUGIN_BIN_DOC_LIST:=
-PLUGIN_DIST_EXTERNAL_LIST:=
-PLUGIN_DIST_TESTS_LIST:=
-PLUGIN_DISTRIBUTED_NAME_LIST:=
-MERLIN_PACKAGES:=
-
-PLUGIN_HEADER_SPEC_LIST :=
-PLUGIN_HEADER_DIRS_LIST :=
-PLUGIN_HEADER_EXCEPTIONS_LIST :=
-PLUGIN_CEA_PROPRIETARY_HEADERS_LIST :=
-PLUGIN_CEA_PROPRIETARY_FILES_LIST :=
-
-# default value used for HEADER_SPEC and PLUGIN_HEADER_SPEC
-DEFAULT_HEADER_SPEC := headers/header_spec.txt
-# default value used for HEADER_DIRS and PLUGIN_HEADER_DIRS
-DEFAULT_HEADER_DIRS := headers
-# default value used for HEADER_EXCEPTIONS and PLUGIN_HEADER_EXCEPTIONS
-DEFAULT_HEADER_EXCEPTIONS := configure
-# default value used for CEA_PROPRIETARY_FILES and PLUGIN_CEA_PROPRIETARY_FILES
-DEFAULT_CEA_PROPRIETARY_FILES := tests/non-free/%
-# default value used for CEA_PROPRIETARY_HEADERS
-# and PLUGIN_CEA_PROPRIETARY_HEADERS
-DEFAULT_CEA_PROPRIETARY_HEADERS := CEA_PROPRIETARY
+##############################################################################
+# TOOLS CONFIG
+################################
 
-MERLIN_PACKAGES:=
+IN_FRAMAC:=yes
 
-###############################
-# Additional global variables #
-###############################
+FRAMAC_PTESTS_SRC:=tools/ptests
+FRAMAC_HDRCK_SRC:=tools/hdrck
+FRAMAC_LINTCK_SRC:=tools/lint
 
-# Directories containing some source code
-SRC_DIRS= ptests $(PLUGIN_LIB_DIR) $(FRAMAC_SRC_DIRS)
+##############################################################################
+# Frama-C
+################################
 
-# Directory containing source code documentation
-DOC_DIR	= doc/code
+.PHONY: all
 
-# Source files to document
-MODULES_TODOC=
+DUNE_WS?=
 
-# Directories to include when compiling
-INCLUDES=$(addprefix -I ,$(FRAMAC_SRC_DIRS)) -I $(PLUGIN_LIB_DIR)
-ifneq ($(ENABLE_GUI),no)
-GUI_INCLUDES = $(addprefix -package ,$(LIBRARY_NAMES_GUI))
+ifneq (${DUNE_WS},)
+  WORKSPACE_OPT:=--workspace dev/dune-workspace.${DUNE_WS}
 else
-GUI_INCLUDES =
+  WORKSPACE_OPT:=
 endif
 
-# Files for which dependencies must be computed.
-# Other files are added later in this Makefile.
-FILES_FOR_OCAMLDEP+=$(PLUGIN_LIB_DIR)/*.mli
+DISABLED_PLUGINS?=
 
-BFLAGS	= $(PACKAGES) $(FLAGS) $(DEBUG) $(INCLUDES) \
-		$(FRAMAC_USER_BFLAGS)
-OFLAGS	= $(PACKAGES) $(FLAGS) $(DEBUG) $(INCLUDES) -compact \
-		$(FRAMAC_USER_OFLAGS)
-
-BLINKFLAGS += -linkpkg $(BFLAGS) -linkall -custom
-OLINKFLAGS += -linkpkg $(OFLAGS) -linkall
-
-DOC_FLAGS= -charset utf8 -colorize-code -stars -m A $(PACKAGES) $(INCLUDES) $(GUI_INCLUDES)
-
-ifneq ($(VERBOSEMAKE),yes)
-DOC_FLAGS+= -hide-warnings
-endif
-
-# Files that depend on external libraries -namely Zarith- whose interface
-# has not been explicitely declared -opaque, hence would trigger warning 58.
-# This can't be solved by Frama-C itself, we can only wait for an update of
-# said library.
-
-NON_OPAQUE_DEPS:=
-
-# Libraries generated by Frama-C
-GEN_BYTE_LIBS=
-GEN_OPT_LIBS=
-
-# Libraries used in Frama-C
-EXTRA_OPT_LIBS:=
-PACKAGES = $(addprefix -package ,$(LIBRARY_NAMES))
-BYTE_LIBS = $(GEN_BYTE_LIBS)
-OPT_LIBS = $(EXTRA_OPT_LIBS)
-
-OPT_LIBS+= $(GEN_OPT_LIBS)
-
-ICONS:= $(addprefix share/,\
-		frama-c.ico frama-c.png unmark.png \
-		switch-on.png switch-off.png)
-
-THEME_ICON_NAMES:= \
-		never_tried.png \
-		unknown.png \
-		surely_valid.png \
-		surely_invalid.png \
-		considered_valid.png \
-		valid_under_hyp.png \
-		invalid_under_hyp.png \
-		invalid_but_dead.png \
-		unknown_but_dead.png \
-		valid_but_dead.png \
-		inconsistent.png \
-		fold.png unfold.png
-
-THEME_ICONS_DEFAULT:= \
-  $(addprefix share/theme/default/,$(THEME_ICON_NAMES))
-THEME_ICONS_COLORBLIND:= \
-  $(addprefix share/theme/colorblind/,$(THEME_ICON_NAMES))
-THEME_ICONS_FLAT:= \
-  $(addprefix share/theme/flat/,$(THEME_ICON_NAMES))
-
-ROOT_LIBC_DIR:= share/libc
-LIBC_SUBDIRS:= sys netinet net arpa
-LIBC_DIR:= $(ROOT_LIBC_DIR) $(addprefix $(ROOT_LIBC_DIR)/,$(LIBC_SUBDIRS))
-LIBC_FILES:= \
-	$(wildcard share/*.h share/*.c) \
-	$(wildcard $(addsuffix /*.h,$(LIBC_DIR))) \
-	$(wildcard $(addsuffix /*.c,$(LIBC_DIR)))
-
-# Checks that all .h can be included multiple times.
-ALL_LIBC_HEADERS:=$(wildcard share/*.h $(addsuffix /*.h,$(LIBC_DIR)))
-
-check-libc: bin/toplevel.$(OCAMLBEST)$(EXE)
-	@echo "checking libc..."; \
-	 EXIT_VALUE=0; \
-	 for file in $(filter-out share/builtin.h,$(ALL_LIBC_HEADERS)); do \
-	   echo "#include \"$$file\"" > check-libc.c; \
-	   echo "#include \"$$file\"" >> check-libc.c; \
-	   FRAMAC_SHARE=share bin/toplevel.$(OCAMLBEST)$(EXE) \
-	   -cpp-extra-args="-Ishare/libc -nostdinc" check-libc.c \
-	       > $$(basename $$file .h).log 2>&1; \
-	   if test $$? -ne 0; then \
-	     if grep -q -e '#error "Frama-C:' $$file; then : ; \
-	     else \
-	       echo "$$file cannot be included twice. \
-Output is in $$(basename $$file .h).log"; \
-	       EXIT_VALUE=1; \
-	     fi; \
-	   else \
-	     rm $$(basename $$file .h).log; \
-	   fi; \
-	 done; \
-	 rm check-libc.c; \
-	 exit $$EXIT_VALUE
-
-clean-check-libc:
-	$(RM) *.log
-
-# Kernel files to be included in the distribution.
-# Plug-ins should use PLUGIN_DISTRIB_EXTERNAL if they export something else
-# than *.ml* files in their directory.
-# NB: configure for the distribution is generated in the distrib directory
-# itself, rather than copied: otherwise, it could include references to
-# non-distributed plug-ins.
-DISTRIB_FILES:=\
-      $(wildcard bin/migration_scripts/*2*.sh) bin/local_export.sh      \
-      bin/frama-c bin/frama-c.byte bin/frama-c-gui bin/frama-c-gui.byte \
-      bin/frama-c-config bin/frama-c-script                             \
-      share/frama-c.WIN32.rc share/frama-c.Unix.rc                      \
-      $(ICONS) $(THEME_ICONS_DEFAULT) $(THEME_ICONS_COLORBLIND)         \
-      $(THEME_ICONS_FLAT)                                               \
-      man/frama-c.1 doc/README						\
-      doc/code/docgen.ml                                                \
-      doc/code/*.css doc/code/intro_plugin.txt				\
-      doc/code/intro_plugin_D_and_S.txt                                 \
-      doc/code/intro_plugin_default.txt                                 \
-      doc/code/intro_kernel_plugin.txt					\
-      doc/code/toc_head.htm                                             \
-      doc/code/toc_tail.htm                                             \
-      doc/Makefile                                                      \
-      $(filter-out ptests/ptests_config.ml,$(wildcard ptests/*.ml*))   \
-      configure.in Makefile Makefile.generating				\
-      Changelog config.h.in						\
-      VERSION VERSION_CODENAME $(wildcard licenses/*)                   \
-      $(LIBC_FILES)							\
-      share/analysis-scripts/analysis.mk                                \
-      share/analysis-scripts/benchmark_database.py                      \
-      share/analysis-scripts/cmd-dep.sh                                 \
-      share/analysis-scripts/concat-csv.sh                              \
-      share/analysis-scripts/clone.sh                                   \
-      share/analysis-scripts/creduce.sh                                 \
-      share/analysis-scripts/epilogue.mk                                \
-      share/analysis-scripts/fc_stubs.c                                 \
-      share/analysis-scripts/find_fun.py                                \
-      share/analysis-scripts/flamegraph.pl                              \
-      share/analysis-scripts/frama_c_results.py                         \
-      share/analysis-scripts/function_finder.py                         \
-      share/analysis-scripts/git_utils.py                               \
-      share/analysis-scripts/list_files.py                              \
-      share/analysis-scripts/make_template.py                           \
-      share/analysis-scripts/make_wrapper.py                            \
-      share/analysis-scripts/parse-coverage.sh                          \
-      share/analysis-scripts/prologue.mk                                \
-      share/analysis-scripts/README.md                                  \
-      share/analysis-scripts/results_display.py                         \
-      share/analysis-scripts/summary.py                                 \
-      share/analysis-scripts/template.mk                                \
-      $(wildcard share/emacs/*.el) share/autocomplete_frama-c           \
-      share/_frama-c                                                    \
-      share/compliance/c11_functions.json                               \
-      share/compliance/glibc_functions.json                             \
-      share/compliance/nonstandard_identifiers.json                     \
-      share/compliance/posix_identifiers.json                           \
-      share/configure.ac                                                \
-      share/Makefile.config.in share/Makefile.common                    \
-      share/Makefile.generic						\
-      share/Makefile.plugin.template share/Makefile.dynamic		\
-      share/Makefile.dynamic_config.external				\
-      share/Makefile.dynamic_config.internal				\
-      share/META.frama-c                                                \
-      $(filter-out src/kernel_internals/runtime/fc_config.ml,              \
-	  $(wildcard src/kernel_internals/runtime/*.ml*))               \
-      $(wildcard src/kernel_services/abstract_interp/*.ml*)             \
-      $(wildcard src/plugins/gui/*.ml*)                                 \
-      $(wildcard src/libraries/stdlib/*.ml*)                            \
-      $(wildcard src/libraries/utils/*.ml*)                             \
-      $(wildcard src/libraries/utils/*.c)                               \
-      $(wildcard src/libraries/project/*.ml*)                           \
-      $(filter-out src/kernel_internals/parsing/check_logic_parser.ml,  \
-          $(wildcard src/kernel_internals/parsing/*.ml*))               \
-      $(wildcard src/kernel_internals/typing/*.ml*)                     \
-      $(wildcard src/kernel_services/ast_data/*.ml*)                    \
-      $(wildcard src/kernel_services/ast_queries/*.ml*)                 \
-      $(wildcard src/kernel_services/ast_printing/*.ml*)                \
-      $(wildcard src/kernel_services/cmdline_parameters/*.ml*)          \
-      $(wildcard src/kernel_services/analysis/*.ml*)                    \
-      $(wildcard src/kernel_services/ast_transformations/*.ml*)         \
-      $(wildcard src/kernel_services/plugin_entry_points/*.ml*)         \
-      $(wildcard src/kernel_services/visitors/*.ml*)                    \
-      $(wildcard src/kernel_services/parsetree/*.ml*)                   \
-      $(wildcard src/libraries/datatype/*.ml*)                          \
-      bin/sed_get_make_major bin/sed_get_make_minor                     \
-      INSTALL.md README.md .make-clean	                        \
-      .make-clean-stamp .force-reconfigure 	\
-      opam/opam \
-
-# Test files to be included in the distribution (without header checking).
-# Plug-ins should use PLUGIN_DISTRIB_TESTS to export their test files. 
-DISTRIB_TESTS=$(shell git ls-files \
-                  tests \
-                  src/plugins/aorai/tests \
-                  src/plugins/report/tests \
-                  src/plugins/wp/tests | $(SED) 's/ /@/g')
-
-
-# files that are needed to compile API documentation of external plugins
-DOC_GEN_FILES:=$(addprefix doc/code/,\
-	*.css intro_plugin.txt intro_kernel_plugin.txt \
-	intro_plugin_default.txt intro_plugin_D_and_S \
-	kernel-doc.ocamldoc \
-	docgen.ml docgen.cm* *.htm)
-
-################
-# Main targets #
-################
-
-# additional compilation targets for 'make all'.
-# cannot be delayed after 'make all'
-EXTRAS	= ptests bin/fc-config$(EXE)
-
-ifneq ($(ENABLE_GUI),no)
-ifeq ($(HAS_LABLGTK),yes)
-EXTRAS	+= gui
+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
 
-all:: byte $(OCAMLBEST) $(EXTRAS) plugins_ptests_config
-
-.PHONY: top opt byte dist bdist rebuild rebuild-branch
-
-dist: clean
-	$(QUIET_MAKE) all
-
-clean-rebuild: clean
-	$(QUIET_MAKE) all
-
-rebuild: config.status
-	$(MAKE) smartclean
-	$(MAKE) depend $(FRAMAC_PARALLEL)
-	$(MAKE) all $(FRAMAC_PARALLEL) || \
-		(touch .force-reconfigure; \
-		 $(MAKE) config.status && \
-		 $(MAKE) depend $(FRAMAC_PARALLEL) && \
-		 $(MAKE) all $(FRAMAC_PARALLEL))
-
-sinclude .Makefile.user
-# Should define FRAMAC_PARALLEL, FRAMAC_USER_FLAGS, FRAMAC_USER_MERLIN_FLAGS
-
-#Create link in share for local execution if
-.PHONY:create_share_link
-create_share_link: share/.gitignore
-
-# note: when using opam pin path in a cloned Frama-C git, the symbolic links
-# become directories, so a different command is necessary for each situation
-
-share/.gitignore: share/Makefile.config
-	if test -f $@; then \
-	  for link in $$(cat $@); do \
-	    if test -L share$$link; then \
-	      rm -f share$$link \
-	    else \
-	      rm -rf share$$link; \
-	    fi; \
-	  done; \
-	fi
-	$(RM) $@.tmp
-	touch $@.tmp
-	$(foreach dir,$(EXTERNAL_PLUGINS),\
-		if test -d $(dir)/share; then \
-			echo "Sharing $(dir)/link"; \
-			ln -s $(realpath $(dir)/share) share/$(notdir $(dir)); \
-			echo /$(notdir $(dir)) >> $@.tmp; \
-		fi; )
-	mv $@.tmp $@
-
-ifeq ("$(DEVELOPMENT)","yes")
-all:: share/.gitignore
-endif
-
-clean_share_link:
-	if test -f share/.gitignore; then \
-	  for link in $$(cat share/.gitignore); do \
-	    if test -L share$$link; then \
-	      rm -f share$$link \
-	    else \
-	      rm -rf share$$link; \
-	    fi; \
-	  done; \
-	  rm share/.gitignore; \
-	fi
-
-clean:: clean_share_link
-
-##############
-# Ocamlgraph #
-##############
-
-# dgraph (included in ocamlgraph)
-#[LC] Cf https://github.com/backtracking/ocamlgraph/pull/32
-ifeq ($(HAS_GNOMECANVAS),yes)
-ifneq ($(ENABLE_GUI),no)
-GRAPH_GUICMO= dgraph.cmo
-GRAPH_GUICMX= dgraph.cmx
-GRAPH_GUIO= dgraph.o
-HAS_DGRAPH=yes
-else # enable_gui is no: disable dgraph
-HAS_DGRAPH=no
-endif
-else # gnome_canvas is not yes: disable dgraph
-HAS_DGRAPH=no
+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
 
-##################
-# Frama-C Kernel #
-##################
-
-# Libraries which could be compiled fully independently
-#######################################################
-
-VERY_FIRST_CMO = src/kernel_internals/runtime/frama_c_init.cmo
-CMO	+= $(VERY_FIRST_CMO)
-
-LIB_CMO =\
-        src/libraries/stdlib/transitioning \
-	src/libraries/stdlib/FCHashtbl \
-	src/libraries/stdlib/extlib \
-	src/libraries/datatype/unmarshal \
-	src/libraries/datatype/unmarshal_z \
-	src/libraries/datatype/structural_descr \
-	src/libraries/datatype/type \
-	src/libraries/datatype/descr \
-	src/libraries/utils/filepath \
-	src/libraries/utils/sanitizer \
-	src/libraries/utils/pretty_utils \
-	src/libraries/utils/hook \
-	src/libraries/utils/bag \
-	src/libraries/utils/wto \
-	src/libraries/utils/vector \
-	src/libraries/utils/indexer \
-	src/libraries/utils/rgmap \
-	src/libraries/utils/bitvector \
-	src/libraries/utils/qstack \
-	src/libraries/stdlib/integer \
-	src/libraries/utils/json \
-	src/libraries/utils/markdown \
-	src/libraries/utils/rich_text \
-	src/libraries/utils/dotgraph
-
-NON_OPAQUE_DEPS+=\
-  src/libraries/datatype/unmarshal_z \
-  src/libraries/stdlib/integer
-
-LIB_CMO:= $(addsuffix .cmo,$(LIB_CMO))
-CMO	+= $(LIB_CMO)
-
-# Very first files to be linked (most modules use them)
-###############################
-
-FIRST_CMO= src/kernel_internals/runtime/fc_config \
-	src/kernel_internals/runtime/gui_init \
-	src/kernel_services/plugin_entry_points/log \
-	src/kernel_services/cmdline_parameters/cmdline \
-	src/libraries/project/project_skeleton \
-	src/libraries/datatype/datatype \
-	src/kernel_services/plugin_entry_points/journal
-
-# project_skeleton requires log
-# datatype requires project_skeleton
-# rangemap requires datatype
-
-FIRST_CMO:= $(addsuffix .cmo,$(FIRST_CMO))
-CMO	+= $(FIRST_CMO)
-
-#Project (Project_skeleton must be linked before Journal)
-PROJECT_CMO= \
-	state \
-	state_dependency_graph \
-	state_topological \
-	state_selection \
-	project \
-	state_builder
-PROJECT_CMO:= $(patsubst %,src/libraries/project/%.cmo,$(PROJECT_CMO))
-CMO	+= $(PROJECT_CMO)
-
-# kernel
-########
-
-KERNEL_CMO=\
-	src/libraries/utils/utf8_logic.cmo                              \
-	src/libraries/utils/binary_cache.cmo                            \
-	src/libraries/utils/hptmap.cmo                                  \
-	src/libraries/utils/hptset.cmo                                  \
-	src/libraries/utils/escape.cmo                                  \
-	src/kernel_services/ast_queries/cil_datatype.cmo             \
-	src/kernel_services/cmdline_parameters/typed_parameter.cmo      \
-	src/kernel_services/plugin_entry_points/dynamic.cmo             \
-	src/kernel_services/cmdline_parameters/parameter_category.cmo   \
-	src/kernel_services/cmdline_parameters/parameter_customize.cmo  \
-	src/kernel_services/cmdline_parameters/parameter_state.cmo      \
-	src/kernel_services/cmdline_parameters/parameter_builder.cmo    \
-	src/kernel_services/plugin_entry_points/plugin.cmo              \
-	src/kernel_services/plugin_entry_points/kernel.cmo              \
-	src/libraries/utils/unicode.cmo                                 \
-	src/kernel_services/plugin_entry_points/emitter.cmo             \
-	src/libraries/utils/floating_point.cmo                          \
-	src/libraries/utils/rangemap.cmo                                \
-	src/kernel_services/ast_printing/cil_types_debug.cmo            \
-	src/kernel_services/ast_printing/printer_builder.cmo            \
-	src/libraries/utils/cilconfig.cmo                               \
-	src/kernel_internals/typing/alpha.cmo                         \
-	src/kernel_services/ast_queries/cil_state_builder.cmo        \
-	src/kernel_internals/runtime/machdeps.cmo                       \
-	src/kernel_services/ast_queries/cil_const.cmo                \
-	src/kernel_services/ast_queries/logic_env.cmo                \
-	src/kernel_services/ast_queries/logic_const.cmo              \
-	src/kernel_services/visitors/visitor_behavior.cmo		\
-	src/kernel_services/ast_queries/cil.cmo                      \
-	src/kernel_internals/parsing/errorloc.cmo                      \
-	src/kernel_services/ast_printing/cil_printer.cmo                \
-	src/kernel_services/ast_printing/cil_descriptive_printer.cmo    \
-	src/kernel_services/parsetree/cabs.cmo                               \
-	src/kernel_services/parsetree/cabshelper.cmo                         \
-	src/kernel_services/ast_printing/logic_print.cmo                \
-	src/kernel_services/ast_queries/logic_utils.cmo              \
-	src/kernel_internals/parsing/logic_parser.cmo                  \
-	src/kernel_internals/parsing/logic_lexer.cmo                   \
-	src/kernel_services/ast_queries/logic_typing.cmo             \
-	src/kernel_services/ast_queries/acsl_extension.cmo				\
-	src/kernel_services/ast_queries/ast_info.cmo                 \
-	src/kernel_services/ast_data/ast.cmo                            \
-	src/kernel_services/ast_printing/cprint.cmo                     \
-	src/kernel_services/visitors/cabsvisit.cmo                      \
-	src/kernel_internals/typing/cabs2cil.cmo                      \
-	src/kernel_services/ast_data/globals.cmo                        \
-	src/kernel_internals/typing/cfg.cmo                           \
-	src/kernel_services/ast_data/kernel_function.cmo                \
-	src/kernel_services/ast_data/property.cmo                       \
-	src/kernel_services/ast_data/property_status.cmo                \
-	src/kernel_services/ast_data/annotations.cmo                    \
-	src/kernel_services/ast_printing/printer.cmo                    \
-	src/kernel_internals/typing/logic_builtin.cmo                 \
-	src/kernel_services/ast_printing/cabs_debug.cmo                 \
-	src/kernel_internals/parsing/lexerhack.cmo                     \
-	src/kernel_internals/parsing/clexer.cmo                        \
-	src/kernel_internals/parsing/cparser.cmo                       \
-	src/kernel_internals/parsing/logic_preprocess.cmo              \
-	src/kernel_internals/typing/mergecil.cmo                      \
-	src/kernel_internals/typing/rmtmps.cmo                        \
-	src/kernel_internals/typing/oneret.cmo                        \
-	src/kernel_internals/typing/frontc.cmo                        \
-	src/kernel_internals/typing/substitute_const_globals.cmo        \
-	src/kernel_services/analysis/ordered_stmt.cmo                   \
-	src/kernel_services/analysis/wto_statement.cmo                  \
-	src/kernel_services/analysis/dataflows.cmo                      \
-	src/kernel_services/analysis/dataflow2.cmo                      \
-	src/kernel_services/analysis/stmts_graph.cmo                    \
-	src/kernel_services/analysis/dominators.cmo                     \
-	src/kernel_services/analysis/service_graph.cmo                  \
-	src/kernel_services/analysis/undefined_sequence.cmo             \
-	src/kernel_services/analysis/interpreted_automata.cmo           \
-	src/kernel_services/ast_data/alarms.cmo                         \
-	src/kernel_services/ast_printing/description.cmo                \
-	src/kernel_services/abstract_interp/lattice_messages.cmo        \
-	src/kernel_services/abstract_interp/abstract_interp.cmo         \
-	src/kernel_services/abstract_interp/bottom.cmo                  \
-	src/kernel_services/abstract_interp/int_Base.cmo                \
-	src/kernel_services/analysis/bit_utils.cmo                      \
-	src/kernel_services/abstract_interp/fc_float.cmo                \
-	src/kernel_services/abstract_interp/float_interval.cmo          \
-	src/kernel_services/abstract_interp/fval.cmo                    \
-	src/kernel_services/abstract_interp/int_interval.cmo            \
-	src/kernel_services/abstract_interp/int_set.cmo                 \
-	src/kernel_services/abstract_interp/int_val.cmo                 \
-	src/kernel_services/abstract_interp/ival.cmo                    \
-	src/kernel_services/abstract_interp/base.cmo                    \
-	src/kernel_services/abstract_interp/origin.cmo                  \
-	src/kernel_services/abstract_interp/map_lattice.cmo             \
-	src/kernel_services/abstract_interp/tr_offset.cmo               \
-	src/kernel_services/abstract_interp/offsetmap.cmo               \
-	src/kernel_services/abstract_interp/int_Intervals.cmo           \
-	src/kernel_services/abstract_interp/locations.cmo               \
-	src/kernel_services/abstract_interp/lmap.cmo                    \
-	src/kernel_services/abstract_interp/lmap_bitwise.cmo            \
-	src/kernel_services/visitors/visitor.cmo                        \
-	src/kernel_services/ast_data/statuses_by_call.cmo               \
-	src/kernel_services/ast_printing/printer_tag.cmo                \
-	$(PLUGIN_TYPES_CMO_LIST)                                        \
-	src/kernel_services/plugin_entry_points/db.cmo                  \
-	src/libraries/utils/command.cmo                                 \
-	src/libraries/utils/task.cmo                                    \
-	src/kernel_services/ast_queries/filecheck.cmo                \
-	src/kernel_services/ast_queries/json_compilation_database.cmo   \
-	src/kernel_services/ast_queries/file.cmo                     \
-	src/kernel_internals/typing/translate_lightweight.cmo         \
-	src/kernel_internals/typing/ghost_cfg.cmo			\
-	src/kernel_internals/typing/ghost_accesses.cmo  		\
-	src/kernel_internals/typing/allocates.cmo                     \
-	src/kernel_internals/typing/unroll_loops.cmo                  \
-	src/kernel_internals/typing/asm_contracts.cmo                 \
-	src/kernel_services/analysis/loop.cmo                           \
-	src/kernel_services/analysis/exn_flow.cmo                       \
-        src/kernel_services/analysis/destructors.cmo                    \
-	src/kernel_services/analysis/logic_interp.cmo                   \
-	src/kernel_internals/typing/infer_annotations.cmo             \
-	src/kernel_services/ast_transformations/clone.cmo                           \
-	src/kernel_services/ast_transformations/filter.cmo                          \
-	src/kernel_services/ast_transformations/inline.cmo              \
-	src/kernel_internals/runtime/special_hooks.cmo                  \
-	src/kernel_internals/runtime/messages.cmo
-
-CMO	+= $(KERNEL_CMO)
-
-MLI_ONLY+=\
-	src/libraries/utils/hptmap_sig.mli                                   \
-	src/kernel_services/cmdline_parameters/parameter_sig.mli             \
-	src/kernel_services/ast_data/cil_types.mli                           \
-	src/kernel_services/parsetree/logic_ptree.mli                             \
-	src/kernel_services/ast_printing/printer_api.mli                     \
-	src/kernel_services/abstract_interp/float_sig.mli                    \
-	src/kernel_services/abstract_interp/float_interval_sig.mli           \
-	src/kernel_services/abstract_interp/lattice_type.mli                 \
-	src/kernel_services/abstract_interp/eva_lattice_type.mli             \
-	src/kernel_services/abstract_interp/int_Intervals_sig.mli            \
-	src/kernel_services/abstract_interp/offsetmap_lattice_with_isotropy.mli \
-	src/kernel_services/abstract_interp/offsetmap_sig.mli                \
-	src/kernel_services/abstract_interp/lmap_sig.mli                     \
-	src/kernel_services/abstract_interp/offsetmap_bitwise_sig.mli
-
-NO_MLI+= src/kernel_services/parsetree/cabs.mli                \
-	src/kernel_internals/runtime/machdep_ppc_32.mli         \
-	src/kernel_internals/runtime/machdep_x86_16.mli         \
-	src/kernel_internals/runtime/machdep_x86_32.mli         \
-	src/kernel_internals/runtime/machdep_x86_64.mli         \
-	src/kernel_services/ast_printing/cabs_debug.mli        \
-	src/kernel_internals/parsing/logic_lexer.mli           \
-	src/kernel_internals/parsing/lexerhack.mli             \
-
-MODULES_NODOC+= src/kernel_internals/runtime/machdep_ppc_32.ml \
-	src/kernel_internals/runtime/machdep_x86_16.ml         \
-	src/kernel_internals/runtime/machdep_x86_32.ml         \
-	src/kernel_internals/runtime/machdep_x86_64.ml         \
-	external/unmarshal_z.mli
-
-
-GENERATED += $(addprefix src/kernel_internals/parsing/,\
-		clexer.ml cparser.ml cparser.mli \
-		logic_lexer.ml logic_parser.ml \
-		logic_parser.mli logic_preprocess.ml)
-
-
-.PHONY: check-logic-parser-wildcard
-check-logic-parser-wildcard:
-	cd src/kernel_internals/parsing && ocaml check_logic_parser.ml
-
-NON_OPAQUE_DEPS+= src/kernel_services/plugin_entry_points/dynamic
-
-# C Bindings
-############
+##############################################################################
+# IVETTE
+################################
 
-GEN_C_BINDINGS=src/libraries/utils/c_bindings.o
-GEN_C_BINDINGS_FLAGS= -fPIC
-GEN_BYTE_LIBS+= $(GEN_C_BINDINGS)
-GEN_OPT_LIBS+= $(GEN_C_BINDINGS)
+.PHONY: ivette ivette-api ivette-dev
 
-src/libraries/utils/c_bindings.o: src/libraries/utils/c_bindings.c
-	$(PRINT_CC) $@
-	$(CC) $(GEN_C_BINDINGS_FLAGS) -c -I$(call winpath,$(OCAMLLIB)) -O3 -Wall -o $@ $<
+ivette: all
+	@$(MAKE) -C ivette
 
-# Common startup module
-# All link command should add it as last linked module and depend on it.
-########################################################################
+ivette-dev: all
+	@$(MAKE) -C ivette dev
 
-STARTUP_CMO=src/kernel_internals/runtime/boot.cmo
-STARTUP_CMX=$(STARTUP_CMO:.cmo=.cmx)
+ivette-api: all
+	@$(MAKE) -C ivette api
 
-# GUI modules
-# See below for GUI compilation
 ##############################################################################
+# HELP
+################################
 
-WTOOLKIT= \
-	wutil widget wbox wfile wpane wpalette wtext wtable
-
-ifeq ("$(LABLGTK_VERSION)","3")
-
-src/plugins/gui/GSourceView.ml: src/plugins/gui/GSourceView3.ml.in
-	$(CP) $< $@
-	$(CHMOD_RO) $@
+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)"
 
-src/plugins/gui/GSourceView.mli: src/plugins/gui/GSourceView3.mli.in
-	$(CP) $< $@
-	$(CHMOD_RO) $@
+##############################################################################
+# INSTALL/UNINSTALL
+################################
 
-else
-src/plugins/gui/GSourceView.ml: src/plugins/gui/GSourceView2.ml.in
-	$(CP) $< $@
-	$(CHMOD_RO) $@
+install:: all
 
-src/plugins/gui/GSourceView.mli: src/plugins/gui/GSourceView2.mli.in
-	$(CP) $< $@
-	$(CHMOD_RO) $@
+INSTALL_TARGET=Frama-C
+include share/Makefile.installation
+include ivette/Makefile.installation
 
-endif
+ifeq (${FRAMAC_DEVELOPER},yes)
 
-SOURCEVIEWCOMPAT:=GSourceView
-GENERATED+=src/plugins/gui/GSourceView.ml src/plugins/gui/GSourceView.mli \
-           src/plugins/gui/dgraph_helper.ml src/plugins/gui/gtk_compat.ml
+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
 
-ifeq ($(LABLGTK),lablgtk3)
-src/plugins/gui/gtk_compat.ml: src/plugins/gui/gtk_compat.3.ml
-	$(CP) $< $@
-	$(CHMOD_RO) $@
-else
-src/plugins/gui/gtk_compat.ml: src/plugins/gui/gtk_compat.2.ml
-	$(CP) $< $@
-	$(CHMOD_RO) $@
-endif
-GENERATED+=src/plugins/gui/gtk_compat.ml
+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
 
-ifeq ($(HAS_DGRAPH),yes)
-  DGRAPHFILES:=debug_manager
-  src/plugins/gui/dgraph_helper.ml: src/plugins/gui/dgraph_helper.yes.ml
-	$(CP) $< $@
-	$(CHMOD_RO) $@
-else
-  DGRAPHFILES:=
-  src/plugins/gui/dgraph_helper.ml: src/plugins/gui/dgraph_helper.no.ml
-	$(CP) $< $@
-	$(CHMOD_RO) $@
 endif
 
-SINGLE_GUI_CMO:= \
-	wutil_once \
-	gtk_compat \
-	$(WTOOLKIT) \
-	$(SOURCEVIEWCOMPAT) \
-	gui_parameters \
-	gtk_helper \
-        dgraph_helper \
-        gtk_form \
-	source_viewer pretty_source source_manager book_manager \
-	warning_manager \
-	filetree \
-	launcher \
-	menu_manager \
-	history \
-	gui_printers \
-	design \
-	analyses_manager file_manager project_manager \
-	help_manager \
-        $(DGRAPHFILES) \
-        property_navigator \
-
-SINGLE_GUI_CMO:= $(patsubst %,src/plugins/gui/%.cmo,$(SINGLE_GUI_CMO))
-
-###############################################################################
-#                                                                             #
-####################                                                          #
-# Plug-in sections #                                                          #
-####################                                                          #
-#                                                                             #
-# For 'internal' developers:                                                  #
-# you can add your own plug-in here,                                          #
-# but it is better to have your own separated Makefile                        #
 ###############################################################################
+# HEADER MANAGEMENT
+################################
 
-###########
-# Metrics #
-###########
-
-PLUGIN_ENABLE:=$(ENABLE_METRICS)
-PLUGIN_NAME:=Metrics
-PLUGIN_DISTRIBUTED:=yes
-PLUGIN_DIR:=src/plugins/metrics
-PLUGIN_CMO:= metrics_parameters css_html metrics_base metrics_acsl \
-	     metrics_cabs metrics_cilast metrics_coverage \
-	     register
-PLUGIN_GUI_CMO:= metrics_gui register_gui
-PLUGIN_DEPENDENCIES:=Eva
-PLUGIN_INTERNAL_TEST:=yes
-$(eval $(call include_generic_plugin_Makefile,$(PLUGIN_NAME)))
-
-#############
-# Callgraph #
-#############
-
-PLUGIN_ENABLE:=$(ENABLE_CALLGRAPH)
-PLUGIN_NAME:=Callgraph
-PLUGIN_DISTRIBUTED:=yes
-PLUGIN_DIR:=src/plugins/callgraph
-PLUGIN_CMO:= options journalize subgraph cg services uses register
-ifeq ($(HAS_DGRAPH),yes)
-PLUGIN_GUI_CMO:=cg_viewer
-else
-PLUGIN_GUI_CMO:=
-PLUGIN_DISTRIB_EXTERNAL:=cg_viewer.ml
-endif
-PLUGIN_CMI:= callgraph_api
-PLUGIN_INTERNAL_TEST:=yes
-PLUGIN_TESTS_DIRS:=callgraph
-PLUGIN_TESTS_LIB:=tests/callgraph/function_pointer.ml
-$(eval $(call include_generic_plugin_Makefile,$(PLUGIN_NAME)))
-
-
-##################
-# Evolved Value Analysis #
-##################
-
-PLUGIN_ENABLE:=$(ENABLE_EVA)
-PLUGIN_NAME:=Eva
-PLUGIN_DIR:=src/plugins/value
-PLUGIN_EXTRA_DIRS:=engine values domains api domains/cvalue domains/apron \
-	domains/gauges domains/equality legacy partitioning utils gui_files \
-	api values/numerors domains/numerors
-PLUGIN_TESTS_DIRS+=value/traces
-
-# Files for the binding to Apron domains. Only available if Apron is available.
-ifeq ($(HAS_APRON),yes)
-PLUGIN_REQUIRES+= apron.octMPQ apron.boxMPQ apron.polkaMPQ apron.apron gmp
-APRON_CMO:= domains/apron/apron_domain
-else
-APRON_CMO:=
-PLUGIN_DISTRIB_EXTERNAL+= \
-	domains/apron/apron_domain.ml domains/apron/apron_domain.mli
-endif
-
-# Files for the numerors domain. Only available is MPFR is available.
-NUMERORS_FILES:= \
-	values/numerors/numerors_utils values/numerors/numerors_float \
-	values/numerors/numerors_interval values/numerors/numerors_arithmetics \
-	values/numerors/numerors_value domains/numerors/numerors_domain
-
-ifeq ($(HAS_MPFR),yes)
-PLUGIN_REQUIRES+= gmp
-PLUGIN_TESTS_DIRS+=value/numerors
-NUMERORS_CMO:= $(NUMERORS_FILES)
-else
-# Do not compile numerors files, but include them in the distributed files.
-NUMERORS_CMO:=
-PLUGIN_DISTRIB_EXTERNAL+= $(addsuffix .ml,$(NUMERORS_FILES))
-PLUGIN_DISTRIB_EXTERNAL+= $(addsuffix .mli,$(NUMERORS_FILES))
-endif
-
-# General rules for ordering files within PLUGIN_CMO:
-# - try to keep the legacy Value before Eva
-PLUGIN_CMO:= partitioning/split_strategy domains/domain_mode value_parameters \
-	utils/value_perf utils/eva_annotations \
-	utils/value_util utils/red_statuses \
-	utils/mark_noresults \
-	utils/widen_hints_ext utils/widen \
-	partitioning/split_return \
-	partitioning/per_stmt_slevel \
-	utils/library_functions \
-	utils/eval_typ utils/backward_formals \
-	alarmset eval utils/structure utils/abstract \
-	values/value_product values/location_lift \
-	values/cvalue_forward values/cvalue_backward \
-	values/main_values values/main_locations \
-	values/offsm_value values/sign_value \
-	legacy/eval_op legacy/function_args \
-	domains/domain_store domains/domain_builder \
-	domains/domain_product domains/domain_lift domains/unit_domain \
-	domains/printer_domain \
-	domains/traces_domain \
-	domains/simple_memory \
-	domains/octagons \
-	domains/gauges/gauges_domain \
-	domains/hcexprs \
-	domains/equality/equality domains/equality/equality_domain \
-	domains/offsm_domain \
-	domains/symbolic_locs \
-	domains/sign_domain \
-	domains/cvalue/warn domains/cvalue/locals_scoping \
-	domains/cvalue/cvalue_offsetmap \
-	utils/value_results \
-	domains/cvalue/builtins domains/cvalue/builtins_malloc \
-	domains/cvalue/builtins_string domains/cvalue/builtins_misc \
-	domains/cvalue/builtins_memory domains/cvalue/builtins_print_c \
-	domains/cvalue/builtins_watchpoint \
-	domains/cvalue/builtins_float domains/cvalue/builtins_split \
-	domains/inout_domain \
-	utils/state_import \
-	legacy/eval_terms legacy/eval_annots \
-	domains/powerset engine/transfer_logic \
-	domains/cvalue/cvalue_transfer domains/cvalue/cvalue_init \
-	domains/cvalue/cvalue_specification \
-	domains/cvalue/cvalue_domain \
-	engine/subdivided_evaluation engine/evaluation engine/abstractions \
-	engine/recursion engine/transfer_stmt engine/transfer_specification \
-	partitioning/auto_loop_unroll \
-	partitioning/partition partitioning/partitioning_parameters \
-	partitioning/partitioning_index partitioning/trace_partitioning \
-	engine/mem_exec engine/iterator engine/initialization \
-	engine/compute_functions engine/analysis register \
-	api/general_requests \
-	utils/unit_tests \
-	api/values_request \
-	$(APRON_CMO) $(NUMERORS_CMO)
-PLUGIN_CMI:= values/abstract_value values/abstract_location \
-	domains/abstract_domain domains/simpler_domains
-PLUGIN_DEPENDENCIES:=Callgraph LoopAnalysis RteGen Server
-
-# These files are used by the GUI, but do not depend on Lablgtk
-VALUE_GUI_AUX:=gui_files/gui_types gui_files/gui_eval \
-		gui_files/gui_callstacks_filters
-PLUGIN_GUI_CMO:=$(VALUE_GUI_AUX) gui_files/gui_callstacks_manager \
-		gui_files/gui_red gui_files/register_gui
-
-PLUGIN_INTERNAL_TEST:= yes
-PLUGIN_TESTS_LIB=tests/float/fval_test.ml
-PLUGIN_DISTRIBUTED:=yes
-VALUE_TYPES:=$(addprefix src/plugins/value_types/,\
-		cilE cvalue precise_locs value_types widen_type)
-PLUGIN_TYPES_CMO:=$(VALUE_TYPES)
-PLUGIN_TYPES_TODOC:=$(addsuffix .mli,$(VALUE_TYPES))
-
-$(eval $(call include_generic_plugin_Makefile,$(PLUGIN_NAME)))
-
-##################
-# Occurrence     #
-##################
-
-PLUGIN_ENABLE:=$(ENABLE_OCCURRENCE)
-PLUGIN_NAME:=Occurrence
-PLUGIN_DISTRIBUTED:=yes
-PLUGIN_DIR:=src/plugins/occurrence
-PLUGIN_CMO:= options register
-PLUGIN_GUI_CMO:=register_gui
-PLUGIN_INTRO:=doc/code/intro_occurrence.txt
-PLUGIN_INTERNAL_TEST:=yes
-PLUGIN_DEPENDENCIES:=Eva
-$(eval $(call include_generic_plugin_Makefile,$(PLUGIN_NAME)))
-
-################################################
-# Runtime Error Annotation Generation analysis #
-################################################
-
-PLUGIN_ENABLE:=$(ENABLE_RTEGEN)
-PLUGIN_NAME:=RteGen
-PLUGIN_DIR:=src/plugins/rte
-PLUGIN_CMO:= options generator rte flags visit register
-PLUGIN_DISTRIBUTED:=yes
-PLUGIN_INTERNAL_TEST:=yes
-PLUGIN_TESTS_DIRS:=rte rte_manual
-PLUGIN_TESTS_LIB:=\
-  tests/rte/my_annotation/my_annotation.ml \
-  tests/rte/rte_api/rte_get_annot.ml \
-  tests/rte/compute_annot/compute_annot.ml \
-  tests/rte/my_annot_proxy/my_annot_proxy.ml
-$(eval $(call include_generic_plugin_Makefile,$(PLUGIN_NAME)))
-
-#################
-# From analysis #
-#################
-
-PLUGIN_ENABLE:=$(ENABLE_FROM_ANALYSIS)
-PLUGIN_NAME:=From
-PLUGIN_DIR:=src/plugins/from
-PLUGIN_CMO:= from_parameters from_compute \
-	functionwise callwise from_register
-PLUGIN_GUI_CMO:=from_register_gui
-PLUGIN_TESTS_DIRS:=idct test float
-PLUGIN_DISTRIBUTED:=yes
-PLUGIN_INTERNAL_TEST:=yes
-FROM_TYPES:=src/plugins/value_types/function_Froms
-PLUGIN_TYPES_CMO:=$(FROM_TYPES)
-PLUGIN_TYPES_TODOC:=$(addsuffix .mli,$(FROM_TYPES))
-PLUGIN_DEPENDENCIES:=Callgraph Eva Postdominators
-
-$(eval $(call include_generic_plugin_Makefile,$(PLUGIN_NAME)))
-
-##################
-# Users analysis #
-##################
-
-PLUGIN_ENABLE:=$(ENABLE_USERS)
-PLUGIN_NAME:=Users
-PLUGIN_DIR:=src/plugins/users
-PLUGIN_CMO:= users_register
-PLUGIN_NO_TEST:=yes
-PLUGIN_DISTRIBUTED:=yes
-PLUGIN_INTERNAL_TEST:=yes
-PLUGIN_DEPENDENCIES:=Callgraph Eva
-
-$(eval $(call include_generic_plugin_Makefile,$(PLUGIN_NAME)))
-
-########################
-# Constant propagation #
-########################
-
-PLUGIN_ENABLE:=$(ENABLE_CONSTANT_PROPAGATION)
-PLUGIN_NAME:=Constant_Propagation
-PLUGIN_DIR:=src/plugins/constant_propagation
-PLUGIN_TESTS_LIB:=tests/constant_propagation/introduction_of_non_explicit_cast.ml
-PLUGIN_CMO:= propagationParameters \
-	api
-PLUGIN_DISTRIBUTED:=yes
-PLUGIN_INTERNAL_TEST:=yes
-PLUGIN_DEPENDENCIES:=Eva
-
-$(eval $(call include_generic_plugin_Makefile,$(PLUGIN_NAME)))
-
-###################
-# Post-dominators #
-###################
-
-PLUGIN_ENABLE:=$(ENABLE_POSTDOMINATORS)
-PLUGIN_NAME:=Postdominators
-PLUGIN_DIR:=src/plugins/postdominators
-PLUGIN_CMO:= postdominators_parameters print compute
-PLUGIN_NO_TEST:=yes
-PLUGIN_DISTRIBUTED:=yes
-PLUGIN_INTERNAL_TEST:=yes
-$(eval $(call include_generic_plugin_Makefile,$(PLUGIN_NAME)))
-
-#########
-# inout #
-#########
-
-PLUGIN_ENABLE:=$(ENABLE_INOUT)
-PLUGIN_NAME:=Inout
-PLUGIN_DIR:=src/plugins/inout
-PLUGIN_CMO:= inout_parameters cumulative_analysis \
-	     operational_inputs outputs inputs derefs register
-PLUGIN_NO_TEST:=yes
-PLUGIN_DISTRIBUTED:=yes
-PLUGIN_INTERNAL_TEST:=yes
-INOUT_TYPES:=src/plugins/value_types/inout_type
-PLUGIN_TYPES_CMO:=$(INOUT_TYPES)
-PLUGIN_TYPES_TODOC:=$(addsuffix .mli,$(INOUT_TYPES))
-PLUGIN_DEPENDENCIES:=Callgraph Eva From
-
-$(eval $(call include_generic_plugin_Makefile,$(PLUGIN_NAME)))
-
-###################
-# Impact analysis #
-###################
-
-PLUGIN_ENABLE:=$(ENABLE_IMPACT)
-PLUGIN_NAME:=Impact
-PLUGIN_DIR:=src/plugins/impact
-PLUGIN_CMO:= options pdg_aux reason_graph compute_impact register
-PLUGIN_GUI_CMO:= register_gui
-PLUGIN_DISTRIBUTED:=yes
-PLUGIN_INTERNAL_TEST:=yes
-PLUGIN_DEPENDENCIES:=Inout Eva Pdg Slicing
-
-$(eval $(call include_generic_plugin_Makefile,$(PLUGIN_NAME)))
-
-##################################
-# PDG : program dependence graph #
-##################################
-
-PLUGIN_ENABLE:=$(ENABLE_PDG)
-PLUGIN_NAME:=Pdg
-PLUGIN_DIR:=src/plugins/pdg
-PLUGIN_TESTS_LIB:=tests/pdg/dyn_dpds.ml \
-                  tests/pdg/sets.ml
-PLUGIN_TESTS_DIRS:=pdg
-PLUGIN_CMO:= pdg_parameters \
-	    ctrlDpds \
-	    pdg_state \
-	    build \
-	    sets \
-	    annot \
-	    marks \
-	    register
-
-PDG_TYPES:=pdgIndex pdgTypes pdgMarks
-PDG_TYPES:=$(addprefix src/plugins/pdg_types/,$(PDG_TYPES))
-PLUGIN_TYPES_CMO:=$(PDG_TYPES)
-
-PLUGIN_INTRO:=doc/code/intro_pdg.txt
-PLUGIN_TYPES_TODOC:=$(addsuffix .mli,$(PDG_TYPES))
-PLUGIN_DEPENDENCIES:=Callgraph Eva From
-PLUGIN_DISTRIBUTED:=yes
-PLUGIN_INTERNAL_TEST:=yes
-
-$(eval $(call include_generic_plugin_Makefile,$(PLUGIN_NAME)))
-
-################################################
-# Scope : show different kinds of dependencies #
-################################################
-
-PLUGIN_ENABLE:=$(ENABLE_SCOPE)
-PLUGIN_NAME:=Scope
-PLUGIN_DIR:=src/plugins/scope
-PLUGIN_TESTS_LIB:=tests/scope/bts971.ml \
-                  tests/scope/zones.ml
-PLUGIN_CMO:= datascope zones defs
-PLUGIN_GUI_CMO:=dpds_gui
-PLUGIN_DEPENDENCIES:=Eva Inout
-PLUGIN_INTRO:=doc/code/intro_scope.txt
-PLUGIN_DISTRIBUTED:=yes
-PLUGIN_INTERNAL_TEST:=yes
-$(eval $(call include_generic_plugin_Makefile,$(PLUGIN_NAME)))
-
-#####################################
-# Sparecode : unused code detection #
-#####################################
-
-PLUGIN_ENABLE:=$(ENABLE_SPARECODE)
-PLUGIN_NAME:=Sparecode
-PLUGIN_DIR:=src/plugins/sparecode
-PLUGIN_CMO:= sparecode_params globs spare_marks transform register
-PLUGIN_INTRO:=doc/code/intro_sparecode.txt
-PLUGIN_DISTRIBUTED:=yes
-PLUGIN_INTERNAL_TEST:=yes
-PLUGIN_DEPENDENCIES:=Pdg Eva Users
-
-$(eval $(call include_generic_plugin_Makefile,$(PLUGIN_NAME)))
-
-###########
-# Slicing #
-###########
-
-PLUGIN_ENABLE:=$(ENABLE_SLICING)
-PLUGIN_NAME:=Slicing
-PLUGIN_DIR:=src/plugins/slicing
-PLUGIN_CMO:= slicingInternals \
-	    slicingTypes \
-	    slicingParameters \
-	    slicingState \
-	    slicingMacros \
-	    slicingMarks \
-	    slicingActions \
-	    fct_slice \
-	    printSlice \
-	    slicingProject \
-	    slicingTransform \
-	    slicingSelect \
-	    slicingCmds \
-	    api \
-	    register
-
-PLUGIN_GUI_CMO:=register_gui
-
-PLUGIN_INTRO:=doc/code/intro_slicing.txt
-PLUGIN_UNDOC:=register.ml # slicing_gui.ml
-
-PLUGIN_TESTS_DIRS:= slicing
-PLUGIN_TESTS_LIB:= tests/slicing/libSelect.ml tests/slicing/libAnim.ml \
-	tests/slicing/simple_intra_slice.ml tests/slicing/combine.ml \
-	tests/slicing/ex_spec_interproc.ml tests/slicing/horwitz.ml \
-	tests/slicing/mark_all_slices.ml tests/slicing/merge.ml \
-	tests/slicing/min_call.ml tests/slicing/select_by_annot.ml \
-	tests/slicing/select_simple.ml tests/slicing/simple_intra_slice.ml \
-	tests/slicing/slice_no_body.ml tests/slicing/switch.ml \
-	tests/slicing/adpcm.ml
-PLUGIN_DISTRIBUTED:=yes
-PLUGIN_INTERNAL_TEST:=yes
-PLUGIN_DEPENDENCIES:=Pdg Callgraph Eva Sparecode
-
-$(eval $(call include_generic_plugin_Makefile,$(PLUGIN_NAME)))
-
-#####################
-# External plug-ins #
-#####################
-
-define INCLUDE_PLUGIN
-FRAMAC_SHARE:=$(FRAMAC_ROOT_SRCDIR)/share
-FRAMAC_PLUGIN:=$(FRAMAC_ROOT_SRCDIR)/lib/plugins
-FRAMAC_PLUGIN_GUI:=$(FRAMAC_ROOT_SRCDIR)/lib/plugins/gui
-PLUGIN_DIR:=$(1)
-include $(1)/Makefile
-endef
-
-$(foreach p,$(EXTERNAL_PLUGINS),$(eval $(call INCLUDE_PLUGIN,$p)))
+# Part that can be shared for external plugins
+include share/Makefile.headers
 
 ###############################################################################
-#                                                                             #
-###########################                                                   #
-# End of plug-in sections #                                                   #
-###########################                                                   #
-#                                                                             #
-###############################################################################
-
-#####################
-# Generic variables #
-#####################
-
-CMX	= $(CMO:.cmo=.cmx)
-CMI	= $(CMO:.cmo=.cmi)
-
-ALL_CMO	= $(CMO) $(PLUGIN_CMO_LIST) $(STARTUP_CMO)
-ALL_CMX	= $(CMX) $(PLUGIN_CMX_LIST) $(STARTUP_CMX)
-
-FILES_FOR_OCAMLDEP+= $(addsuffix /*.mli,$(FRAMAC_SRC_DIRS)) \
-	$(addsuffix /*.ml,$(FRAMAC_SRC_DIRS))
-
-MODULES_TODOC+=$(filter-out $(MODULES_NODOC),\
-	$(MLI_ONLY) $(NO_MLI:.mli=.ml) \
-	$(filter-out $(NO_MLI),\
-	$(filter-out $(PLUGIN_TYPES_CMO_LIST:.cmo=.mli),$(CMO:.cmo=.mli))))
-
-################################
-# toplevel.{byte,opt} binaries #
+# Testing
 ################################
 
-ALL_BATCH_CMO= $(filter-out src/kernel_internals/runtime/gui_init.cmo,\
-	$(ALL_CMO))
-ALL_BATCH_CMX= $(filter-out src/kernel_internals/runtime/gui_init.cmx,\
-	$(ALL_CMX))
-
-bin/toplevel.byte$(EXE): $(ALL_BATCH_CMO) $(GEN_BYTE_LIBS) \
-			$(PLUGIN_DYN_CMO_LIST)
-	$(PRINT_LINKING) $@
-	$(OCAMLC) $(BLINKFLAGS) -o $@ $(BYTE_LIBS) $(ALL_BATCH_CMO)
-
-#Profiling version of toplevel.byte using ocamlprof
-bin/toplevel.prof$(EXE): $(ALL_BATCH_CMO) $(GEN_BYTE_LIBS) \
-			$(PLUGIN_DYN_CMO_LIST)
-	$(PRINT_OCAMLCP) $@
-	$(OCAMLCP) $(BLINKFLAGS) -o $@ $(BYTE_LIBS) $(ALL_BATCH_CMO)
-
-bin/toplevel.opt$(EXE): $(ALL_BATCH_CMX) $(GEN_OPT_LIBS) \
-			$(PLUGIN_DYN_CMX_LIST)
-	$(PRINT_LINKING) $@
-	$(OCAMLOPT) $(OLINKFLAGS) -o $@ $(OPT_LIBS) $(ALL_BATCH_CMX)
-
-LIB_KERNEL_CMO= $(filter-out src/kernel_internals/runtime/gui_init.cmo, $(CMO))
-LIB_KERNEL_CMX= $(filter-out src/kernel_internals/runtime/gui_init.cmx, $(CMX))
-
-lib/fc/frama-c.cma: $(LIB_KERNEL_CMO) $(GEN_BYTE_LIBS) lib/fc/META.frama-c
-	$(PRINT_LINKING) $@
-	$(MKDIR) $(FRAMAC_LIB)
-	$(OCAMLMKLIB) -o lib/fc/frama-c $(BYTE_LIBS) $(LIB_KERNEL_CMO)
-
-lib/fc/frama-c.cmxa: lib/fc/frama-c.cma $(GEN_OPT_LIBS) $(LIB_KERNEL_CMX)
-	$(MKDIR) $(FRAMAC_LIB)
-	$(PRINT_LINKING) $@
-	$(OCAMLMKLIB) -o lib/fc/frama-c $(OPT_LIBS) $(LIB_KERNEL_CMX)
-
-####################
-# (Ocaml) Toplevel #
-####################
-
-bin/toplevel.top$(EXE): $(filter-out src/kernel_internals/runtime/boot.ml,$(ALL_BATCH_CMO)) \
-			src/kernel_internals/runtime/toplevel_config.cmo \
-			$(GEN_BYTE_LIBS) $(PLUGIN_DYN_CMO_LIST)
-	$(PRINT_OCAMLMKTOP) $@
-	$(OCAMLMKTOP) $(BFLAGS) -warn-error -31 -custom -o $@ \
-	  -linkpkg $(BYTE_LIBS) $(ALL_BATCH_CMO) \
-	   src/kernel_internals/runtime/toplevel_config.cmo
-
-#######
-# GUI #
-#######
-
-ifneq ($(ENABLE_GUI),no)
-
-SINGLE_GUI_CMI = $(SINGLE_GUI_CMO:.cmo=.cmi)
-SINGLE_GUI_CMX = $(SINGLE_GUI_CMO:.cmo=.cmx)
-
-GUICMO += $(SINGLE_GUI_CMO) $(PLUGIN_GUI_CMO_LIST)
-
-MODULES_TODOC+= $(filter-out src/plugins/gui/book_manager.mli,\
-	$(SINGLE_GUI_CMO:.cmo=.mli))
-
-GUICMI = $(GUICMO:.cmo=.cmi)
-GUICMX = $(SINGLE_GUI_CMX) $(PLUGIN_GUI_CMX_LIST)
-
-$(GUICMI) $(GUICMO) bin/viewer.byte$(EXE): BFLAGS+= $(GUI_INCLUDES)
-$(GUICMX) bin/viewer.opt$(EXE): OFLAGS+= $(GUI_INCLUDES)
-
-$(PLUGIN_DYN_DEP_GUI_CMO_LIST): BFLAGS+= $(GUI_INCLUDES)
-$(PLUGIN_DYN_DEP_GUI_CMX_LIST): OFLAGS+= $(GUI_INCLUDES)
-
-.PHONY:gui
-
-gui-byte:: bin/viewer.byte$(EXE) share/Makefile.dynamic_config \
-           $(PLUGIN_META_LIST)
-
-gui-opt:: gui-byte bin/viewer.opt$(EXE)
-
-gui: gui-$(OCAMLBEST)
-
-ALL_GUI_CMO= $(ALL_CMO) $(GRAPH_GUICMO) $(GUICMO)
-ALL_GUI_CMX= $(patsubst %.cma,%.cmxa,$(ALL_GUI_CMO:.cmo=.cmx))
+# PTESTS is internal
+FRAMAC_PTESTS:=$(FRAMAC_PTESTS_SRC)/ptests.exe
 
-bin/viewer.byte$(EXE): BYTE_LIBS+= $(GRAPH_GUICMO)
-bin/viewer.byte$(EXE): $(filter-out $(GRAPH_GUICMO),$(ALL_GUI_CMO)) \
-			$(GEN_BYTE_LIBS) \
-			$(PLUGIN_DYN_CMO_LIST) $(PLUGIN_DYN_GUI_CMO_LIST)
-	$(PRINT_LINKING) $@
-	$(OCAMLC) $(BLINKFLAGS) $(THREAD) -o $@ $(BYTE_LIBS) \
-	  $(CMO) \
-	  $(filter-out \
-	    $(patsubst $(PLUGIN_GUI_LIB_DIR)/%,$(PLUGIN_LIB_DIR)/%,\
-		$(PLUGIN_GUI_CMO_LIST)),\
-	    $(PLUGIN_CMO_LIST)) \
-	  $(GUICMO) $(STARTUP_CMO)
+# WTESTS is internal
+FRAMAC_WTESTS:=$(FRAMAC_PTESTS_SRC)/wtests.exe
 
-bin/viewer.opt$(EXE): OPT_LIBS+= $(GRAPH_GUICMX)
-bin/viewer.opt$(EXE): $(filter-out $(GRAPH_GUICMX),$(ALL_GUI_CMX)) \
-			$(GEN_OPT_LIBS) \
-			$(PLUGIN_DYN_CMX_LIST) $(PLUGIN_DYN_GUI_CMX_LIST) \
-			$(PLUGIN_CMX_LIST) $(PLUGIN_GUI_CMX_LIST)
-	$(PRINT_LINKING) $@
-	$(OCAMLOPT) $(OLINKFLAGS) $(THREAD) -o $@ $(OPT_LIBS) \
-	  $(CMX) \
-	  $(filter-out \
-	    $(patsubst $(PLUGIN_GUI_LIB_DIR)/%,$(PLUGIN_LIB_DIR)/%,\
-	      $(PLUGIN_GUI_CMX_LIST)),\
-	    $(PLUGIN_CMX_LIST)) \
-	  $(GUICMX) $(STARTUP_CMX)
-endif
-
-#####################
-# Config Ocaml File #
-#####################
+# 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
 
-CONFIG_DIR=src/kernel_internals/runtime
-CONFIG_FILE=$(CONFIG_DIR)/fc_config.ml
-CONFIG_CMO=$(CONFIG_DIR)/fc_config.cmo
-GENERATED +=$(CONFIG_FILE)
-#Generated in Makefile.generating
+# Test aliasing definition allowing ./configure --disable-<plugin>
+PTEST_ALIASES:=@tests/ptests @src/plugins/ptests \
+  @src/kernel_internals/parsing/tests/ptests
 
-empty:=
-space:=$(empty) $(empty)
+# WP tests need WP cache
+PTEST_USE_WP_CACHE:=yes
 
-ifeq ($(ENABLE_GUI),no)
-CONFIG_CMO=$(ALL_CMO)
-CONFIG_PLUGIN_CMO=$(PLUGIN_CMO_LIST)
-else
-CONFIG_CMO=$(ALL_GUI_CMO)
-CONFIG_PLUGIN_CMO=$(PLUGIN_GUI_CMO_LIST)
-endif
-
-ifeq ($(HAS_DOT),yes)
-OPTDOT=Some \"$(DOT)\"
-else
-OPTDOT=None
-endif
+# Part that can be shared for external plugins
+include share/Makefile.testing
 
-COMPILATION_UNITS=\
-  $(foreach p,$(CONFIG_CMO),\"$(notdir $(patsubst %.cmo,%,$p))\"; )
-
-###################
-# Generating part #
-###################
-# It is in another file in order to have a dependency only on Makefile.generating.
-# It must be before `.depend` definition because it modifies $GENERATED.
-
-include Makefile.generating
-
-#########
-# Tests #
-#########
-
-ifeq ($(OCAMLBEST),opt)
-PTESTS_FILES=ptests_config.cmi ptests_config.cmx ptests_config.o
-else
-PTESTS_FILES=ptests_config.cmi ptests_config.cmo
-endif
-
-.PHONY: tests oracles btests tests_dist libc_tests plugins_ptests_config external_tests \
-	update_external_tests
-
-tests:: byte opt ptests
-	$(PRINT_EXEC) ptests
-	time -p $(PTESTS) $(PTESTS_OPTS) $(FRAMAC_PARALLEL) \
-		-make "$(MAKE)" $(PLUGIN_TESTS_LIST)
-
-external_tests: byte opt ptests
-tests:: external_tests
-
-update_external_tests: PTESTS_OPTS="-update"
-update_external_tests: external_tests
-
-oracles: byte opt ptests
-	$(PRINT_MAKING) oracles
-	./bin/ptests.$(OCAMLBEST)$(EXE) -make "$(MAKE)" $(PLUGIN_TESTS_LIST) \
-		> /dev/null 2>&1
-	./bin/ptests.$(OCAMLBEST)$(EXE) -make "$(MAKE)" -update \
-		$(PLUGIN_TESTS_LIST)
-
-btests: byte ./bin/ptests.byte$(EXE)
-	$(PRINT_EXEC) ptests -byte
-	time -p ./bin/ptests.byte$(EXE) -make "$(MAKE)" -byte \
-		$(PLUGIN_TESTS_LIST)
-
-tests_dist: dist ptests
-	$(PRINT_EXEC) ptests
-	time -p ./bin/ptests.$(OCAMLBEST)$(EXE) -make "$(MAKE)" \
-		$(PLUGIN_TESTS_LIST)
-
-# test only one test suite : make suite_tests
-%_tests: opt ptests
-	$(PRINT_EXEC) ptests
-	./bin/ptests.$(OCAMLBEST)$(EXE) -make "$(MAKE)" $($*_TESTS_OPTS) $*
-
-# full test suite
-wp_TESTS_OPTS=-j 1
-fulltests: tests wp_tests
-
-acsl_tests: byte
-	$(PRINT_EXEC) acsl_tests
-	find doc/speclang -name \*.c -exec ./bin/toplevel.byte$(EXE) {} \; > /dev/null
-
-LONELY_TESTS_DIR:=$(wildcard $(TEST_DIRS_AS_PLUGIN:%=tests/%))
-ifeq ($(strip $(LONELY_TESTS_DIR)),)
-  LONELY_TESTS_ML_FILES:=
-else
-  LONELY_TESTS_ML_FILES:=\
-    $(sort $(shell find $(TEST_DIRS_AS_PLUGIN:%=tests/%) -not -path '*/\.*' -name '*.ml'))
-endif
-$(foreach file,$(LONELY_TESTS_ML_FILES),\
-  $(eval $(file:%.ml=%.cmo): BFLAGS+=-I $(dir $(file))))
-$(foreach file,$(LONELY_TESTS_ML_FILES),\
-  $(eval $(file:%.ml=%.cmx): OFLAGS+=-I $(dir $(file))))
-$(foreach file,$(LONELY_TESTS_ML_FILES),\
-  $(eval $(file:%.ml=%.cmxs): OFLAGS+=-I $(dir $(file))))
-.PRECIOUS: $(LONELY_TESTS_ML_FILES:%.ml=%.cmx) \
-           $(LONELY_TESTS_ML_FILES:%.ml=%.cmxs) \
-           $(LONELY_TESTS_ML_FILES:%.ml=%.cmo) \
-           $(LONELY_TESTS_ML_FILES:%.ml=%.cmi)
-
-bin/ocamldep_transitive_closure: devel_tools/ocamldep_transitive_closure.ml
-	$(OCAMLOPT) -package ocamlgraph -package str -linkpkg -o $@ $<
-
-tests/crowbar/.%.depend: tests/crowbar/%.ml
-	$(OCAMLDEP) $(INCLUDES) $< > $@
-
-tests/crowbar/%: tests/crowbar/%.ml tests/crowbar/.%.depend .depend \
-                 bin/ocamldep_transitive_closure bin/toplevel.opt
-	$(OCAMLOPT) $(OLINKFLAGS) -w -42 -package crowbar -o $@ \
-        $(GEN_C_BINDINGS) \
-        $$(bin/ocamldep_transitive_closure -root tests/crowbar/$*.cmx \
-             -deps tests/crowbar/.$*.depend -deps .depend) \
-        $<
-
-tests/crowbar/full-link-%: tests/crowbar/%.ml lib/fc/frama-c.cmxa
-	$(OCAMLOPT) $(OLINKFLAGS) -ccopt "-Llib/fc" -w -42 -package crowbar -o $@ \
-	lib/fc/frama-c.cmxa $<
-
-crowbar-%: tests/crowbar/%
-	$<
-
-crowbar-afl-%: tests/crowbar/%
-	$(MKDIR) tests/crowbar/output-$*
-	afl-fuzz $(AFL_OPTS) -i tests/crowbar/input -o tests/crowbar/output-$* $< @@
-
-crowbar-afl-check-%: tests/crowbar/%
-	$(foreach file,$(wildcard tests/crowbar/output-$*/crashes/id*), \
-          $< $(file) >/dev/null 2>&1 || \
-          echo "$(file) leads to a real test failure";)
-
-##############
-# Emacs tags #
-##############
-
-.PHONY: tags
-# otags gives a better tagging of ocaml files than etags
-ifdef OTAGS
-tags:
-	$(OTAGS) -r src lib
-vtags:
-	$(OTAGS) -vi -r src lib
-else
-tags:
-	find . -name "*.ml[ily]" -o -name "*.ml" | sort -r | xargs \
-	etags "--regex=/[ \t]*let[ \t]+\([^ \t]+\)/\1/" \
-	      "--regex=/[ \t]*let[ \t]+rec[ \t]+\([^ \t]+\)/\1/" \
-	      "--regex=/[ \t]*and[ \t]+\([^ \t]+\)/\1/" \
-	      "--regex=/[ \t]*type[ \t]+\([^ \t]+\)/\1/" \
-	      "--regex=/[ \t]*exception[ \t]+\([^ \t]+\)/\1/" \
-	      "--regex=/[ \t]*val[ \t]+\([^ \t]+\)/\1/" \
-	      "--regex=/[ \t]*module[ \t]+\([^ \t]+\)/\1/"
-endif
-
-#################
-# Documentation #
-#################
-
-.PHONY: doc doc-distrib
-
-# private targets, useful for recompiling the doc without dependencies
-# (too long!)
-.PHONY: doc-kernel doc-index plugins-doc doc-update doc-tgz
-
-DOC_DEPEND=$(MODULES_TODOC) byte $(DOC_PLUGIN)
-ifneq ($(ENABLE_GUI),no)
-DOC_DEPEND+=bin/viewer.byte$(EXE)
-endif
-
-$(DOC_DIR)/docgen.cmo: $(DOC_DIR)/docgen.ml
-	$(PRINT_OCAMLC) $@
-	$(OCAMLC) -c -I +ocamldoc -I +compiler-libs -I $(CONFIG_DIR) $(DOC_DIR)/docgen.ml
-
-$(DOC_DIR)/docgen.cmxs: $(DOC_DIR)/docgen.ml
-	$(PRINT_PACKING) $@
-	$(OCAMLOPT) -o $@ -shared -I +ocamldoc -I +compiler-libs -I $(CONFIG_DIR) \
-	  $(DOC_DIR)/docgen.ml
-
-clean-doc::
-	$(PRINT_RM) "documentation generator"
-	$(RM) $(DOC_DIR)/docgen.cm*
-
-DOC_NOT_FOR_DISTRIB=yes
-plugins-doc:
-	$(QUIET_MAKE) \
-	 $(if $(DOC_NOT_FOR_DISTRIB),$(PLUGIN_DOC_LIST),\
-	   $(filter \
-	     $(addsuffix _DOC,$(PLUGIN_DISTRIBUTED_NAME_LIST)),\
-	     $(PLUGIN_DOC_LIST)))
-
-.PHONY: server-doc-md server-doc-html server-doc
-
-server-doc-md: byte
-	$(PRINT) 'Generating Markdown server documentation'
-	@rm -fr doc/server
-	@mkdir -p doc/server
-	./bin/frama-c.byte -server-doc doc/server
-
-server-doc-html: server-doc-md
-	$(PRINT) 'Generating HTML server documentation'
-	@find doc/server -name "*.md" -print -exec pandoc \
-			--standalone --toc --toc-depth=2 --to html \
-			--template doc/pandoc/template.html \
-			--metadata-file {}.json \
-			--lua-filter doc/pandoc/href.lua \
-			{} -o {}.html \;
-	@cp -f doc/pandoc/style.css doc/server/
-	$(PRINT) 'HTML server documentation ready:'
-	$(PRINT) '  open doc/server/readme.md.html'
-
-server-doc: server-doc-html
-
-# to make the documentation for one plugin only,
-# the name of the plugin should begin with a capital letter :
-# Example for the pdg doc : make Pdg_DOC
-# While working on the documentation of a plugin, it can also be useful
-# to use : make -o doc/code/kernel-doc.ocamldoc Plugin_DOC
-# to avoid redoing the global documentation each time.
-
-STDLIB_FILES:=\
-	array \
-	buffer \
-        bytes \
-	char \
-	format \
-	hashtbl \
-	int64 \
-	list \
-	map \
-	marshal \
-	obj \
-        parsing \
-	printf \
-	queue \
-	scanf \
-	set \
-	stack \
-	string \
-	sys \
-	weak \
-	ephemeron
-
-STDLIB_FILES:=$(patsubst %,$(OCAMLLIB)/%.mli,$(STDLIB_FILES))
-
-.PHONY: doc-kernel
-doc-kernel: $(DOC_DIR)/kernel-doc.ocamldoc
-
-$(DOC_DIR)/kernel-doc.ocamldoc: $(DOC_DEPEND)
-	$(PRINT_DOC) Kernel Documentation
-	$(MKDIR) $(DOC_DIR)/html
-	$(RM) $(DOC_DIR)/html/*.html
-	$(OCAMLDOC) $(DOC_FLAGS) \
-	  $(addprefix -passopt -stdlib ,$(STDLIB_FILES)) \
-	  -t "Frama-C Kernel" \
-	  -sort -css-style ../style.css \
-	  -g $(DOC_PLUGIN) \
-	  -d $(DOC_DIR)/html -dump $@ \
-	  $(MODULES_TODOC); \
-	  RES=$$?; \
-	  if test $$RES -ne 0; then \
-	    $(RM) $@; \
-	    exit $$RES; \
-	  fi
-
-DYN_MLI_DIR := src/plugins/print_api
-
-.PHONY: doc-dynamic
-doc-dynamic: doc-kernel
-	$(RM) $(DYN_MLI_DIR)/dynamic_plugins.mli
-	./bin/frama-c.byte \
-		-print_api $(call winpath,$(FRAMAC_ROOT_SRCDIR)/$(DYN_MLI_DIR))
-	$(PRINT_DOC) Dynamically registered plugins Documentation
-	$(MKDIR) $(DOC_DIR)/dynamic_plugins
-	$(RM) $(DOC_DIR)/dynamic_plugins/*.html
-	$(OCAMLDOC) $(DOC_FLAGS) -I $(FRAMAC_LIB) -I $(OCAMLLIB) \
-	  -passopt -docpath $(DOC_DIR)/html \
-	  -sort -css-style ../style.css \
-	  -load $(DOC_DIR)/kernel-doc.ocamldoc \
-	  -t " Dynamically registered plugins" \
-	  -g $(DOC_PLUGIN) \
-	  -d $(DOC_DIR)/dynamic_plugins \
-	  $(DYN_MLI_DIR)/dynamic_plugins.mli
-	$(ECHO) '<li><a href="dynamic_plugins/Dynamic_plugins.html">Dynamically registered plugins</a </li>' > $(DOC_DIR)/dynamic_plugins.toc
-
-doc-index: doc-kernel doc-dynamic plugins-doc
-	$(PRINT_MAKING) doc/code/index.html
-	$(CAT)  $(DOC_DIR)/toc_head.htm $(DOC_DIR)/*.toc \
-		$(DOC_DIR)/toc_tail.htm > $(DOC_DIR)/index.html
-
-doc-update: doc-kernel doc-dynamic plugins-doc doc-index
-
-doc:: doc-kernel doc-dynamic plugins-doc doc-index
-
-doc-kernel doc-dynamic plugins-doc doc-index: $(DOC_DEPEND)
-
-doc-tgz:
-	$(PRINT_MAKING) frama-c-api.tar.gz
-	cd $(DOC_DIR); \
-	  $(TAR) zcf tmp.tgz index.html *.txt \
-	   $(notdir $(wildcard $(DOC_DIR)/*.css $(DOC_DIR)/*.png \
-			       $(DOC_DIR)/dynamic_plugins*)) \
-	   html \
-	   $(foreach p,$(PLUGIN_DISTRIBUTED_NAME_LIST),\
-	     $(notdir $($(p)_DOC_DIR)))
-	$(MKDIR) frama-c-api
-	$(RM) -r frama-c-api/*
-	cd frama-c-api; $(TAR) zxf ../$(DOC_DIR)/tmp.tgz
-	$(TAR) zcf frama-c-api.tar.gz frama-c-api
-	$(RM) -r frama-c-api $(DOC_DIR)/tmp.tgz
-
-doc-distrib:
-	$(QUIET_MAKE) clean-doc
-	$(QUIET_MAKE) doc DOC_NOT_FOR_DISTRIB=
-	$(QUIET_MAKE) doc-tgz
-
-#find src -name "*.ml[i]" -o -name "*.ml" -maxdepth 3 | sort -r | xargs
-dots: $(ALL_CMO)
-	$(PRINT_DOC) callgraph
-	$(OCAMLDOC) $(DOC_FLAGS) $(INCLUDES) -o doc/call_graph.dot \
-	  -dot -dot-include-all -dot-reduce $(MODULES_TODOC)
-	$(QUIET_MAKE) doc/call_graph.svg
-	$(QUIET_MAKE) doc/call_graph.ps
-
-# pandoc is required to regenerate the manpage
-man/frama-c.1: man/frama-c.1.header man/frama-c.1.md
-	$(PRINT) 'generating $@'
-	$(RM) $@
-	pandoc -s -t man -H $^ | tail -n +5 > man/frama-c.1
-	$(CHMOD_RO) $@
-
-# Checking consistency with the current implementation
-######################################################
-
-DOC_DEV_DIR = doc/developer
-CHECK_API_DIR=$(DOC_DEV_DIR)/check_api
-
-$(CHECK_API_DIR)/check_code.cmo: $(CHECK_API_DIR)/check_code.ml
-	$(PRINT_OCAMLC) $@
-	$(OCAMLC) -c -I +ocamldoc str.cma $(CHECK_API_DIR)/check_code.ml
-
-$(CHECK_API_DIR)/check_code.cmxs: $(CHECK_API_DIR)/check_code.ml
-	$(PRINT_PACKING) $@
-	$(OCAMLOPT) -o $@ -shared -I +ocamldoc \
-		str.cmxa $(CHECK_API_DIR)/check_code.ml
-
-CHECK_CODE=$(CHECK_API_DIR)/check_code.cmxs
-
-.PHONY: check-devguide
-check-devguide: $(CHECK_CODE) $(DOC_DEPEND) $(DOC_DIR)/kernel-doc.ocamldoc
-	$(PRINT) 'Checking     developer guide consistency'
-	$(MKDIR) $(CHECK_API_DIR)/html
-	$(OCAMLDOC) $(DOC_FLAGS) -I $(OCAMLLIB) \
-	  -g $(CHECK_CODE) \
-	  -passopt -docdevpath -passopt "`pwd`/$(CHECK_API_DIR)" \
-	  -load $(DOC_DIR)/kernel-doc.ocamldoc \
-	  -d $(CHECK_API_DIR)/html
-	$(RM) -r  $(CHECK_API_DIR)/html
-	$(MAKE) --silent -C $(CHECK_API_DIR) main.idx
-	$(MAKE) --silent -C $(CHECK_API_DIR) >$(CHECK_API_DIR)/summary.txt
-	$(ECHO) see all the information displayed here \
-		in $(CHECK_API_DIR)/summary.txt
-	$(RM) code_file
-################################
-# Code prettyfication and lint #
+###############################################################################
+# Linters
 ################################
 
-# We're interested by any .ml[i]? file in src, except for scripts in test
-# directories, and generated files (in particular lexers and parsers)
-# Note: the find command below is *very* ugly, but it should be POSIX-compliant.
-
-ALL_ML_FILES:=$(shell find src -name '*.ml' -print -o -name '*.mli' -print -o -path '*/tests' -prune '!' -name '*')
-ALL_ML_FILES+=ptests/ptests.ml
-MANUAL_ML_FILES:=$(filter-out $(GENERATED) $(PLUGIN_GENERATED_LIST), $(ALL_ML_FILES))
-
-# Allow control of files to be linted/fixed by external sources
-# (e.g. pre-commit hook that will concentrate on files which have changed)
-
-sinclude .Makefile.lint
+# Code prettyfication and lint
+include share/Makefile.linting
 
-HAS_GIT_FILE:=$(wildcard .git/HEAD)
-
-ifeq ("$(HAS_GIT_FILE)","")
-LINT_OTHER_SOURCES:=
-else
-LINT_OTHER_SOURCES:=\
-  $(filter-out \
-    $(shell git ls-tree --name-only HEAD src/plugins/*), \
-    $(wildcard src/plugins/*))
-endif
-
-$(foreach dir,$(LINT_OTHER_SOURCES),$(eval sinclude $(dir)/.Makefile.lint))
-
-ML_LINT_MISSING:=$(filter-out $(MANUAL_ML_FILES), $(ML_LINT_KO))
-
-# By default, also checks files with unknown status:
-# this requires new files to pass lint checker from the beginning
-
-ML_LINT_CHECK?=$(filter-out $(ML_LINT_KO), $(MANUAL_ML_FILES))
-
-# this NEWLINE variable containing a literal newline character is used to avoid
-# the error "argument list too long", in some instances of "foreach".
-# For details, see https://stackoverflow.com/questions/7039811
-define NEWLINE
-
-
-endef
-
-# pre-requisite intentionally left blank: this target should only be used
-# if the file is not present to generate it once and forall,
-# and be edited manually afterwards
-# double colon here tells make not to attempt updating the .Makefile.lint
-# if it does not exist, but just to ignore it.
-.Makefile.lint::
-	echo "ML_LINT_KO:=" >> $@
-	$(foreach file,$(sort $(MANUAL_ML_FILES)), \
-            if ! $(MAKE) ML_LINT_CHECK=$(file) lint; \
-            then echo "ML_LINT_KO+=$(file)" >> $@; fi;$(NEWLINE) )
-
-$(foreach dir,$(LINT_OTHER_SOURCES),\
-  $(eval $(dir)/.Makefile.lint:: ; \
-     $(foreach file, $(sort $(filter $(dir)/%, $(MANUAL_ML_FILES))), \
-            if ! $$(MAKE) ML_LINT_CHECK=$(file) lint; \
-            then echo "ML_LINT_KO+=$(file)" >> $$@; fi; )))
-
-.PHONY: stats-lint
-stats-lint:
-	echo \
-         "scale = 2; bad = $(words $(ML_LINT_MISSING)); \
-          all = $(words $(sort $(MANUAL_ML_FILES))); \
-	  fail = $(words $(ML_LINT_KO)); \
-          \"lint coverage: \"; \
-          ((all - fail) * 100) / all; " | bc
-	echo "number of files supposed to pass lint: $(words $(ML_LINT_CHECK))"
-	echo "number of files supposed to fail lint: $(words $(ML_LINT_KO))"
-ifneq ($(strip $(ML_LINT_MISSING)),)
-	echo "number of files missing from src/ : $(words $(ML_LINT_MISSING))"
-	$(foreach file, $(ML_LINT_MISSING), echo $(file);)
-	exit 1
-endif
-
-INDENT_TARGET= $(patsubst %,%.indent,$(ML_LINT_CHECK))
-
-LINT_TARGET= $(patsubst %,%.lint,$(ML_LINT_CHECK))
-
-FIX_SYNTAX_TARGET=$(patsubst %,%.fix-syntax,$(ML_LINT_CHECK))
-
-.PHONY: $(INDENT_TARGET) $(LINT_TARGET) $(FIX_SYNTAX_TARGET) \
-        indent lint fix-syntax
-
-indent: $(INDENT_TARGET)
-
-lint: $(LINT_TARGET)
-
-check-ocp-indent-version:
-	if command -v ocp-indent >/dev/null; then \
-		$(eval ocp_version_major := $(shell ocp-indent --version | $(SED) -E "s/^([0-9]+)\.[0-9]+\..*/\1/")) \
-		$(eval ocp_version_minor := $(shell ocp-indent --version | $(SED) -E "s/^[0-9]+\.([0-9]+)\..*/\1/")) \
-		if [ "$(ocp_version_major)" -lt 1 -o "$(ocp_version_minor)" -lt 7 ]; then \
-			echo "error: ocp-indent >=1.7.0 required for linting (got $(ocp_version_major).$(ocp_version_minor))"; \
-			exit 1; \
-		fi; \
-	else \
-		exit 1; \
-	fi;
-
-fix-syntax: $(FIX_SYNTAX_TARGET)
-
-$(INDENT_TARGET): %.indent: % check-ocp-indent-version
-	ocp-indent -i $<
-
-$(LINT_TARGET): %.lint: % check-ocp-indent-version
-	# See SO 1825552 on mixing grep and \t (and cry)
-	# For OK_NL, we have three cases:
-	# - for empty files, the computation boils down to 0 - 0 == 0
-	# - for non-empty files with a proper \n at the end, to 1 - 1 == 0
-	# - for empty files without \n, to 1 - 0 == 1 that will be catched
-	OK_TAB=$$(grep -c -e "$$(printf '^ *\t')" $<) ; \
-        OK_SPACE=$$(grep -c -e '[[:blank:]]$$' $<) ; \
-        OK_NL=$$(($$(tail -c -1 $< | wc -c) - $$(tail -n -1 $< | wc -l))) ; \
-        OK_EMPTY=$$(tail -n -1 $< | grep -c -e '^[[:blank:]]*$$') ; \
-        ERROR=$$(($$OK_TAB + $$OK_SPACE + $$OK_NL + $$OK_EMPTY)) ; \
-        if test $$ERROR -gt 0; then \
-          echo "File $< does not pass syntactic checks:"; \
-          echo "$$OK_TAB lines indented with tabulation instead of spaces"; \
-          echo "$$OK_SPACE lines with spaces at end of line"; \
-          test $$OK_NL -eq 0 || echo "No newline at end of file"; \
-          test $$OK_EMPTY -eq 0 || echo "Empty line(s) at end of file"; \
-          echo "Please run make ML_LINT_CHECK=$< fix-syntax"; \
-          exit 1 ; \
-        fi
-	ocp-indent $< > $<.tmp;
-	if cmp -s $< $<.tmp; \
-        then rm -f $<.tmp; \
-        else \
-          echo "File $< is not indented correctly."; \
-          echo "Please run make ML_LINT_CHECK=$< indent";\
-          rm $<.tmp; \
-          exit 1; \
-        fi
-
-$(FIX_SYNTAX_TARGET): %.fix-syntax: %
-	$(ISED) -e 's/^ *\t\+/ /' $<
-	$(ISED) -e 's/\(.*[^[:blank:]]\)[[:blank:]]\+$$/\1/' $<
-	$(ISED) -e 's/^[ \t]\+$$//' $<
-	if test \( $$(tail -n -1 $< | wc -l) -eq 0 \) -a \( $$(wc -c $< | cut -d " " -f 1) -gt 0 \) ; then \
-          echo "" >> $<; \
-        else \
-          while tail -n -1 $< | grep -l -e '^[ \t]*$$'; do \
-            head -n -1 $< > $<.tmp; \
-            mv $<.tmp $<; \
-          done; \
-        fi
-
-# Avoid a UTF-8 locale at all cost: in such setting, sed does not work
-# reliably if you happen to have latin-1 encoding somewhere,
-# which is still unfortunately the case in some dark corners of the platform
-%.fix-syntax: LC_ALL = C
-
-################
-# Installation #
-################
-
-#       line below does not work if INCLUDES contains twice the same directory
-#       Do not attempt to copy gui interfaces if gui is disabled
-#Byte
-ALL_BATCH_CMO_FIXED=$(filter-out src/kernel_internals/runtime/gui_init.cmo,$(CMO) $(STARTUP_CMO))
-LIB_BYTE_TO_INSTALL=\
-	$(MLI_ONLY:.mli=.cmi) \
-	$(ALL_BATCH_CMO_FIXED:.cmo=.cmi) \
-	$(ALL_BATCH_CMO_FIXED) \
-	$(filter-out %.o,$(GEN_BYTE_LIBS:.cmo=.cmi)) \
-	$(GEN_BYTE_LIBS)
-
-#Byte GUI
-ifneq ("$(ENABLE_GUI)","no")
-LIB_BYTE_TO_INSTALL+=$(SINGLE_GUI_CMI) $(SINGLE_GUI_CMO)
-endif
-
-#Opt
-ifeq ("$(OCAMLBEST)","opt")
-ALL_BATCH_CMX_FIXED= $(filter-out src/kernel_internals/runtime/gui_init.cmx,\
-	$(CMX) $(STARTUP_CMX))
-LIB_OPT_TO_INSTALL +=\
-	$(ALL_BATCH_CMX) \
-	$(filter %.a,$(ALL_BATCH_CMX_FIXED:.cmxa=.a)) \
-	$(filter %.o,$(ALL_BATCH_CMX_FIXED:.cmx=.o)) \
-	$(filter-out %.o,$(GEN_OPT_LIBS)) \
-	$(filter-out $(GEN_BYTE_LIBS),$(filter %.o,$(GEN_OPT_LIBS:.cmx=.o)))
-
-#Opt GUI
-ifneq ("$(ENABLE_GUI)","no")
-LIB_OPT_TO_INSTALL += $(SINGLE_GUI_CMX) $(SINGLE_GUI_CMX:.cmx=.o)
-endif
-
-endif
-
-clean-install:
-	$(PRINT_RM) "Installation directory"
-	$(RM) -r $(FRAMAC_LIBDIR)
-
-install-lib-byte: clean-install
-	$(PRINT_INSTALL) kernel API
-	$(MKDIR) $(FRAMAC_LIBDIR)
-	$(CP) $(LIB_BYTE_TO_INSTALL) $(FRAMAC_LIBDIR)
-	$(CP) $(addprefix lib/fc/,dllframa-c$(DLLEXT) libframa-c.a frama-c.cma META.frama-c) $(FRAMAC_LIBDIR)
-
-install-lib-opt: install-lib-byte
-	$(CP) $(LIB_OPT_TO_INSTALL) $(FRAMAC_LIBDIR)
-	$(CP) $(addprefix lib/fc/,frama-c.a frama-c.cmxa) $(FRAMAC_LIBDIR)
-
-install-doc-code:
-	$(PRINT_INSTALL) API documentation
-	$(MKDIR) $(FRAMAC_DATADIR)/doc/code
-	(cd doc ; tar cf - --exclude='.svn' --exclude='*.toc' \
-			--exclude='*.htm' --exclude='*.txt' \
-			--exclude='*.ml' \
-			code \
-		| (cd $(FRAMAC_DATADIR)/doc ; tar xf -))
-
-.PHONY: install
-install:: install-lib-$(OCAMLBEST)
-	$(PRINT_MAKING) destination directories
-	$(MKDIR) $(BINDIR)
-	$(MKDIR) $(MANDIR)/man1
-	$(MKDIR) $(FRAMAC_PLUGINDIR)/top
-	$(MKDIR) $(FRAMAC_PLUGINDIR)/gui
-	$(MKDIR) $(FRAMAC_DATADIR)/theme/default
-	$(MKDIR) $(FRAMAC_DATADIR)/theme/colorblind
-	$(MKDIR) $(FRAMAC_DATADIR)/theme/flat
-	$(MKDIR) $(FRAMAC_DATADIR)/libc/sys
-	$(MKDIR) $(FRAMAC_DATADIR)/libc/netinet
-	$(MKDIR) $(FRAMAC_DATADIR)/libc/net
-	$(MKDIR) $(FRAMAC_DATADIR)/libc/arpa
-	$(PRINT_INSTALL) shared files
-	$(CP) \
-	  $(wildcard share/*.c share/*.h) \
-	  share/Makefile.dynamic share/Makefile.plugin.template \
-	  share/Makefile.config share/Makefile.common share/Makefile.generic \
-	  share/configure.ac share/autocomplete_frama-c share/_frama-c \
-	  $(FRAMAC_DATADIR)
-	$(MKDIR) $(FRAMAC_DATADIR)/analysis-scripts
-	$(CP) \
-	  share/analysis-scripts/analysis.mk \
-	  share/analysis-scripts/benchmark_database.py \
-	  share/analysis-scripts/cmd-dep.sh \
-	  share/analysis-scripts/concat-csv.sh \
-	  share/analysis-scripts/clone.sh \
-	  share/analysis-scripts/creduce.sh \
-	  share/analysis-scripts/epilogue.mk \
-	  share/analysis-scripts/fc_stubs.c \
-	  share/analysis-scripts/find_fun.py \
-	  share/analysis-scripts/flamegraph.pl \
-	  share/analysis-scripts/frama_c_results.py \
-	  share/analysis-scripts/function_finder.py \
-	  share/analysis-scripts/git_utils.py \
-	  share/analysis-scripts/list_files.py \
-	  share/analysis-scripts/make_template.py \
-	  share/analysis-scripts/make_wrapper.py \
-	  share/analysis-scripts/parse-coverage.sh \
-	  share/analysis-scripts/prologue.mk \
-	  share/analysis-scripts/README.md \
-	  share/analysis-scripts/results_display.py \
-	  share/analysis-scripts/summary.py \
-	  share/analysis-scripts/template.mk \
-	  $(FRAMAC_DATADIR)/analysis-scripts
-	$(MKDIR) $(FRAMAC_DATADIR)/compliance
-	$(CP) share/compliance/c11_functions.json \
-	  share/compliance/glibc_functions.json \
-	  share/compliance/nonstandard_identifiers.json \
-	  share/compliance/posix_identifiers.json \
-	  $(FRAMAC_DATADIR)/compliance
-	$(MKDIR) $(FRAMAC_DATADIR)/emacs
-	$(CP) $(wildcard share/emacs/*.el) $(FRAMAC_DATADIR)/emacs
-	$(CP) share/frama-c.rc $(ICONS) $(FRAMAC_DATADIR)
-	$(CP) $(THEME_ICONS_DEFAULT) $(FRAMAC_DATADIR)/theme/default
-	$(CP) $(THEME_ICONS_COLORBLIND) $(FRAMAC_DATADIR)/theme/colorblind
-	$(CP) $(THEME_ICONS_FLAT) $(FRAMAC_DATADIR)/theme/flat
-	if [ -d $(EMACS_DATADIR) ]; then \
-	  $(CP) $(wildcard share/emacs/*.el) $(EMACS_DATADIR); \
-	fi
-	$(CP) share/Makefile.dynamic_config.external \
-	      $(FRAMAC_DATADIR)/Makefile.dynamic_config
-	$(PRINT_INSTALL) C standard library
-	$(CP) $(wildcard share/libc/*.c share/libc/*.i share/libc/*.h) \
-	      $(FRAMAC_DATADIR)/libc
-	$(CP) share/libc/sys/*.[ch] $(FRAMAC_DATADIR)/libc/sys
-	$(CP) share/libc/arpa/*.[ch] $(FRAMAC_DATADIR)/libc/arpa
-	$(CP) share/libc/net/*.[ch] $(FRAMAC_DATADIR)/libc/net
-	$(CP) share/libc/netinet/*.[ch] $(FRAMAC_DATADIR)/libc/netinet
-	$(PRINT_INSTALL) binaries
-	$(CP) bin/toplevel.$(OCAMLBEST) $(BINDIR)/frama-c$(EXE)
-	$(CP) bin/toplevel.byte$(EXE) $(BINDIR)/frama-c.byte$(EXE)
-	if [ -x bin/toplevel.top ] ; then \
-	  $(CP) bin/toplevel.top $(BINDIR)/frama-c.toplevel$(EXE); \
-	fi
-	if [ -x bin/viewer.$(OCAMLBEST) ] ; then \
-	  $(CP) bin/viewer.$(OCAMLBEST) $(BINDIR)/frama-c-gui$(EXE);\
-	fi
-	if [ -x bin/viewer.byte$(EXE) ] ; then \
-	  $(CP) bin/viewer.byte$(EXE) $(BINDIR)/frama-c-gui.byte$(EXE); \
-	fi
-	$(CP) bin/ptests.$(OCAMLBEST)$(EXE) \
-	      $(BINDIR)/ptests.$(OCAMLBEST)$(EXE)
-	if [ -x bin/fc-config$(EXE) ] ; then \
-		$(CP) bin/fc-config$(EXE) $(BINDIR)/frama-c-config$(EXE); \
-	fi
-	if [ -x bin/frama-c-script ] ; then \
-		$(CP) bin/frama-c-script $(BINDIR)/frama-c-script; \
-	fi
-	$(PRINT_INSTALL) config files
-	$(CP) $(addprefix ptests/,$(PTESTS_FILES)) $(FRAMAC_LIBDIR)
-	$(PRINT_INSTALL) API documentation
-	$(MKDIR) $(FRAMAC_DATADIR)/doc/code
-	$(CP) $(wildcard $(DOC_GEN_FILES)) $(FRAMAC_DATADIR)/doc/code
-	$(PRINT_INSTALL) plug-ins
-	if [ -d "$(FRAMAC_PLUGIN)" ]; then \
-	  $(CP)  $(PLUGIN_DYN_CMI_LIST) $(PLUGIN_META_LIST) \
-		 $(FRAMAC_PLUGINDIR); \
-	  $(CP)  $(PLUGIN_DYN_CMO_LIST) $(FRAMAC_PLUGINDIR)/top; \
-	  if [ "$(OCAMLBEST)" = "opt" ]; then \
-	    $(CP) $(PLUGIN_DYN_CMX_LIST) $(FRAMAC_PLUGINDIR)/top; \
-	  fi; \
-	fi
-	$(PRINT_INSTALL) gui plug-ins
-	if [ -d "$(FRAMAC_PLUGIN_GUI)" -a "$(PLUGIN_DYN_GUI_EXISTS)" = "yes" ]; \
-	then \
-	  $(CP) $(patsubst %.cma,%.cmi,$(PLUGIN_DYN_GUI_CMO_LIST:.cmo=.cmi)) \
-		$(PLUGIN_DYN_GUI_CMO_LIST) $(FRAMAC_PLUGINDIR)/gui; \
-	  if [ "$(OCAMLBEST)" = "opt" ]; then \
-	    $(CP) $(PLUGIN_DYN_GUI_CMX_LIST) $(FRAMAC_PLUGINDIR)/gui; \
-	  fi; \
-	fi
-	$(PRINT_INSTALL) man pages
-	$(CP) man/frama-c.1 $(MANDIR)/man1/frama-c.1
-	$(CP) man/frama-c.1 $(MANDIR)/man1/frama-c-gui.1
-
-.PHONY: uninstall
-uninstall::
-	$(PRINT_RM) installed binaries
-	$(RM) $(BINDIR)/frama-c* $(BINDIR)/ptests.$(OCAMLBEST)$(EXE)
-	$(PRINT_RM) installed shared files
-	$(RM) -R $(FRAMAC_DATADIR)
-	$(PRINT_RM) installed libraries
-	$(RM) -R $(FRAMAC_LIBDIR) $(FRAMAC_PLUGINDIR)
-	$(PRINT_RM) installed man files
-	$(RM) $(MANDIR)/man1/frama-c.1 $(MANDIR)/man1/frama-c-gui.1
-
-################################
-# File headers: license policy #
+###############################################################################
+# Frama-C Documentation
 ################################
 
-
-# Generating headers
-####################
-
-# Default header specification files
-HEADER_SPEC := $(DEFAULT_HEADER_SPEC)
-# The list can be extended by external plugins using PLUGIN_HEADER_SPEC variable
-HEADER_SPEC += $(PLUGIN_HEADER_SPEC_LIST)
-# Default list of header specification files can be overloaded.
-HEADER_SPEC_FILE?=$(HEADER_SPEC)
-
-# Default directory (containing subdirectories open-source and close-source)
-HEADER_DIRS := $(DEFAULT_HEADER_DIRS)
-# The list can be extended by external plugins using PLUGIN_HEADER_DIRS variable
-HEADER_DIRS += $(PLUGIN_HEADER_DIRS_LIST)
-# Takes into account the kind of distribution (open-souce/close-source)
-DISTRIB_HEADER_DIRS?=$(addsuffix /$(DISTRIB_HEADERS),$(HEADER_DIRS))
-
-# List of distributed files allowed to have no entry into the HEADER_SPEC_FILE
-HEADER_EXCEPTIONS := $(DEFAULT_HEADER_EXCEPTIONS)
-HEADER_EXCEPTIONS += opam/files $(wildcard $(PLUGIN_HEADER_EXCEPTIONS_LIST))
-
-# List of headers that cannot be part of an open-source distribution
-CEA_PROPRIETARY_HEADERS := $(DEFAULT_CEA_PROPRIETARY_HEADERS)
-CEA_PROPRIETARY_HEADERS += $(PLUGIN_CEA_PROPRIETARY_HEADERS_LIST)
-
-# List of files that cannot be part of an open-source distribution
-CEA_PROPRIETARY_FILES := $(DEFAULT_CEA_PROPRIETARY_FILES)
-CEA_PROPRIETARY_FILES += $(PLUGIN_CEA_PROPRIETARY_FILES_LIST)
-
-HDRCK=./headers/hdrck$(EXE)
-
-HDRCK_EXTRA?=$(STRICT_HEADERS)
-# Can be set to "-exit-on-warning"
-ifeq ($(HDRCK_EXTRA),no)
-HDRCK_EXTRA:=""
-else
-ifeq ($(HDRCK_EXTRA),yes)
-HDRCK_EXTRA:="-exit-on-warning"
-endif
-endif
-
-.PHONY: headers
-
-# OPEN_SOURCE: set it to 'no' if you want to apply close source headers.
-# STRICT_HEADERS: set it to 'yes' if you want to consider warnings as errors
-headers:: $(HDRCK)
-	$(PRINT) "|$(OPEN_SOURCE)|$(SPECIFIED_OPEN_SOURCE)|"
-	$(PRINT) "Applying $(HDRCK_DISTRIB_HEADERS) headers (OPEN_SOURCE=$(HDRCK_OPEN_SOURCE))..."
-	$(PRINT) "- HEADER_SPEC_FILE=$(HEADER_SPEC_FILE)"
-	$(PRINT) "- DISTRIB_HEADER_DIRS=$(HDRCK_DISTRIB_HEADER_DIRS)"
-	$(HDRCK) \
-		$(HDRCK_EXTRA) \
-		-update -C . \
-		$(addprefix -header-dirs ,$(HDRCK_DISTRIB_HEADER_DIRS)) \
-		-headache-config-file ./headers/headache_config.txt \
-		$(HEADER_SPEC_FILE)
-
-hdrck: $(HDRCK)
-
-$(HDRCK): headers/hdrck.ml
-	$(PRINT_MAKING)	$@
-ifeq ($(OCAMLBEST),opt)
-	$(OCAMLOPT) str.cmxa unix.cmxa $< -o $@
-else
-	$(OCAMLC) str.cma unix.cma $< -o $@
-endif
-
-hdrck-clean:
-	$(RM) headers/hdrck headers/hdrck.o
-	$(RM) headers/hdrck.cmx headers/hdrck.cmi headers/hdrck.cmp
-
-clean:: hdrck-clean
-
-CURRENT_HEADERS?=open-source
-CURRENT_HEADER_DIRS?=$(addsuffix /$(CURRENT_HEADERS),$(HEADER_DIRS))
-
-# OPEN_SOURCE: set it to 'yes' if you want to check open source headers
-# STRICT_HEADERS: set it to 'yes' if you want to consider warnings as errors
-# The target check-headers does the following checks:
-# 1. Checks entries of HEADER_SPEC_FILE
-# 2. Checks that every DISTRIB_FILES (except HEADER_EXCEPTIONS) have an entry
-#    inside HEADER_SPEC_FILE
-# 3. Checks that all these files are not under DISTRIB_PROPRIETARY_HEADERS
-#    licences
-# Also check that distributed files are not encoded in ISO-8859. Do this first,
-# because identical headers but with different encodings are not exactly
-# easy to distinguish
-.PHONY: check-headers
-check-headers: $(HDRCK)
-	$(PRINT) "Checking $(DISTRIB_HEADERS) headers (OPEN_SOURCE=$(OPEN_SOURCE), CURRENT_HEADERS=$(CURRENT_HEADERS))..."
-	$(PRINT) "- HEADER_SPEC_FILE=$(HEADER_SPEC_FILE)"
-	$(PRINT) "- CURRENT_HEADER_DIRS=$(CURRENT_HEADER_DIRS)"
-	$(PRINT) "- FORBIDDEN_HEADERS=$(DISTRIB_PROPRIETARY_HEADERS)"
-	 # Workaround to avoid "argument list too long" in make 3.82+ without
-	 # using 'file' built-in, only available on make 4.0+
-	 # for make 4.0+, using the 'file' function could be a better solution,
-	 # although it seems to segfault in 4.0 (but not in 4.1)
-	$(RM) file_list_to_check.tmp file_list_exceptions.tmp
-	@$(foreach file,$(DISTRIB_FILES),\
-			echo $(file) >> file_list_to_check.tmp$(NEWLINE))
-	@$(foreach file,$(HEADER_EXCEPTIONS),\
-			echo $(file) >> file_list_exceptions.tmp$(NEWLINE))
-
-	@if command -v file >/dev/null 2>/dev/null; then \
-		echo "Checking that distributed files do not use iso-8859..."; \
-		file --mime-encoding -f file_list_to_check.tmp | \
-			grep "iso-8859" \
-			| $(SED) "s/^/error: invalid encoding in /" \
-			| ( ! grep "error: invalid encoding" ); \
-	else echo "command 'file' not found, skipping encoding checks"; \
-	fi
-	$(HDRCK) \
-		$(HDRCK_EXTRA) \
-		$(addprefix -header-dirs ,$(CURRENT_HEADER_DIRS)) \
-		$(addprefix -forbidden-headers ,$(DISTRIB_PROPRIETARY_HEADERS)) \
-		-headache-config-file ./headers/headache_config.txt \
-		-distrib-file file_list_to_check.tmp \
-		-header-except-file file_list_exceptions.tmp \
-		$(HEADER_SPEC_FILE)
-	$(RM) file_list_to_check.tmp file_list_exceptions.tmp
-
-########################################################################
-# Makefile is rebuilt whenever Makefile.in or configure.in is modified #
-########################################################################
-
-share/Makefile.config: share/Makefile.config.in config.status
-	$(PRINT_MAKING) $@
-	./config.status --file $@
-
-share/Makefile.dynamic_config: share/Makefile.dynamic_config.internal
-	$(PRINT_MAKING) $@
-	$(RM) $@
-	$(CP) $< $@
-	$(CHMOD_RO) $@
-
-config.status: configure
-	$(PRINT_MAKING) $@
-	./config.status --recheck
-
-configure: configure.in .force-reconfigure
-	$(PRINT_MAKING) $@
-	autoconf -f
-
-# If 'make clean' has to be performed after 'svn update':
-# change '.make-clean-stamp' before 'svn commit'
-.make-clean: .make-clean-stamp
-	$(TOUCH) $@
-	$(QUIET_MAKE) clean
-
-include .make-clean
-
-# force "make clean" to be executed for all users of SVN
-force-clean:
-	expr `$(CAT) .make-clean-stamp` + 1 > .make-clean-stamp
-
-# force a reconfiguration for all svn users
-force-reconfigure:
-	expr `$(CAT) .force-reconfigure` + 1 > .force-reconfigure
-
-.PHONY: force-clean force-reconfigure
-
-############
-# cleaning #
-############
-
-clean-journal:
-	$(PRINT_RM) journal
-	$(RM) frama_c_journal*
-
-clean-tests:
-	$(PRINT_RM) tests
-	$(RM) tests/*/*.byte$(EXE) tests/*/*.opt$(EXE) tests/*/*.cm* \
-		tests/dynamic/.cm* tests/*/*~ tests/*/#*
-	$(RM) tests/*/result/*.*
-
-clean-doc:: $(PLUGIN_LIST:=_CLEAN_DOC)
-	$(PRINT_RM) documentation
-	$(RM) -r $(DOC_DIR)/html
-	$(RM) $(DOC_DIR)/docgen.cm* $(DOC_DIR)/*~
-	$(RM) doc/db/*~ doc/db/ocamldoc.sty doc/db/db.tex
-	$(RM) doc/training/*/*.cm*
-	if [ -f doc/developer/Makefile ]; then \
-	  $(MAKE) --silent -C doc/developer clean; \
-	fi
-
-clean-gui::
-	$(PRINT_RM) gui
-	$(RM) src/*/*/*_gui.cm* src/*/*/*_gui.o \
-	      src/plugins/gui/*.cm* src/plugins/gui/*.o
-
-clean:: $(PLUGIN_LIST:=_CLEAN) \
-		clean-tests clean-journal clean-check-libc
-	$(PRINT_RM) lib/plugins
-	$(RM) $(addprefix $(PLUGIN_LIB_DIR)/,*.mli *.cm* *.o META.*)
-	$(RM) $(addprefix $(PLUGIN_TOP_LIB_DIR)/,*.mli *.cm* *.o *.a)
-	$(RM) $(addprefix $(PLUGIN_GUI_LIB_DIR)/,*.mli *.cm* *.o *.a)
-	$(PRINT_RM) local installation
-	$(RM) lib/*.cm* lib/*.o lib/fc/*.cm* lib/fc/*.o lib/gui/*.cm* lib/*.cm*
-	$(PRINT_RM) other sources
-	for d in . $(SRC_DIRS) src/plugins/gui share; do \
-	  $(RM) $$d/*.cm* $$d/*.o $$d/*.a $$d/*.annot $$d/*~ $$d/*.output \
-		$$d/*.annot $$d/\#*; \
-	done
-	$(PRINT_RM) generated files
-	$(RM) $(GENERATED)
-	$(PRINT_RM) binaries
-	$(RM) bin/toplevel.byte$(EXE) bin/viewer.byte$(EXE) \
-		bin/ptests.byte$(EXE) bin/*.opt$(EXE) bin/toplevel.top$(EXE)
-	$(RM) bin/fc-config$(EXE)
-
-smartclean:
-	$(MAKE) -f share/Makefile.clean smartclean
-
-# Do NOT use :: for this rule: it is mandatory to remove share/Makefile.config
-# as the very last step performed by make (who'll otherwise try to regenerate
-# it in the middle of cleaning)
-dist-clean distclean: clean clean-doc \
-	              $(PLUGIN_LIST:=_DIST_CLEAN)
-	$(PRINT_RM) config
-	$(RM) share/Makefile.config
-	$(RM) config.cache config.log config.h
-	$(RM) -r autom4te.cache
-	$(PRINT_RM) documentation
-	$(RM) $(DOC_DIR)/kernel-doc.ocamldoc
-	$(PRINT_RM) dummy plug-ins
-	$(RM) src/dummy/*/*.cm* src/dummy/*/*.o src/dummy/*/*.a \
-		src/dummy/*/*.annot src/dummy/*/*~ src/dummy/*/*.output \
-		src/dummy/*/*.annot src/dummy/*/\#*
-
-
-ifeq ($(OCAMLWIN32),yes)
-# Use Win32 typical resources
-share/frama-c.rc: share/frama-c.WIN32.rc
-	$(PRINT_MAKING) $@
-	$(CP) $^ $@
-else
-# Use Unix typical resources
-share/frama-c.rc: share/frama-c.Unix.rc
-	$(PRINT_MAKING) $@
-	$(CP) $^ $@
-endif
-
-GENERATED+=share/frama-c.rc
-
-##########
-# Depend #
-##########
-
-PLUGIN_DEP_LIST:=$(PLUGIN_LIST)
-
-.PHONY: depend
-
-# in case .depend is absent, we will make it. Otherwise, it will be left
-# untouched. Only make depend will force a recomputation of dependencies
-.depend: $(GENERATED) share/Makefile.dynamic_config
-	$(MAKE) depend
-
-depend:: $(GENERATED) share/Makefile.dynamic_config
-	$(PRINT_MAKING) .depend
-	$(RM) .depend
-	$(OCAMLDEP) $(INCLUDES) $(FILES_FOR_OCAMLDEP) > .depend
-	$(OCAMLDEP) $(INCLUDES) $(TEST_DIRS_AS_PLUGIN:%=-I tests/%) \
-          $(LONELY_TESTS_ML_FILES) >> .depend
-	$(CHMOD_RO) .depend
-
-#Used by internal plugins to wait until the *.mli of all the plugins are in
-# $(PLUGIN_LIB_DIR) before computing their .depend. Otherwise ocamldep doesn't
-# mark inter-plugin dependencies
-$(PLUGIN_LIB_DIR)/.placeholders_ready:
-	touch $@
-
-ifneq ($(MAKECMDGOALS),clean)
-ifneq ($(MAKECMDGOALS),distclean)
-ifneq ($(MAKECMDGOALS),smartclean)
-ifneq ($(MAKECMDGOALS),depend)
-sinclude .depend
-endif
-endif
-endif
-endif
-
-#####################
-# ptest development #
-#####################
-
-.PHONY: ptests
-
-PTESTS_SRC=ptests/ptests_config.ml ptests/ptests.ml
-
-# Do not generate tests/ptests_config if we are compiling a distribution
-# that does not contain a 'tests' dir
-PTESTS_CONFIG:= $(shell if test -d tests; then echo tests/ptests_config; fi)
-
-ifneq ("$(PTESTS_CONFIG)","")
-GENERATED_TESTS:=tests/spec/preprocess_dos.c
-else
-GENERATED_TESTS:=
-endif
-
-tests/spec/preprocess_dos.c: tests/spec/preprocess_dos.c.in \
-                             Makefile share/Makefile.config
-	$(RM) $@
-	$(SED) -e "s|@UNIX2DOS@|$(PP_DOS_UNIX2DOS)|g" \
-               -e "s|@DONTRUN@|$(PP_DOS_DONTRUN)|g" \
-               $< > $@
-	$(CHMOD_RO) $@
-
-ifneq ("$(HAS_UNIX2DOS)","no")
-tests/spec/preprocess_dos.c: PP_DOS_UNIX2DOS=$(UNIX2DOS)
-tests/spec/preprocess_dos.c: PP_DOS_DONTRUN=
-else
-tests/spec/preprocess_dos.c: PP_DOS_UNIX2DOS=unix2dos
-tests/spec/preprocess_dos.c: PP_DOS_DONTRUN=DONTRUN: no unix2dos found
-endif
-
-ptests: bin/ptests.$(OCAMLBEST)$(EXE) $(PTESTS_CONFIG) $(GENERATED_TESTS)
-
-bin/ptests.byte$(EXE): $(PTESTS_SRC)
-	$(PRINT_LINKING) $@
-	$(OCAMLC) -I ptests -dtypes -thread -g -o $@ \
-	    unix.cma threads.cma str.cma dynlink.cma $^
-
-bin/ptests.opt$(EXE): $(PTESTS_SRC)
-	$(PRINT_LINKING) $@
-	$(OCAMLOPT) -I ptests -dtypes -thread -o $@ \
-	    unix.cmxa threads.cmxa str.cmxa dynlink.cmxa $^
-
-GENERATED+=ptests/ptests_config.ml tests/ptests_config $(GENERATED_TESTS)
-
-#######################
-# Source distribution #
-#######################
-
-.PHONY: src-distrib
-
-STANDALONE_PLUGINS_FILES = \
-	$(addprefix src/dummy/hello_world/,hello_world.ml Makefile) \
-	$(addprefix src/dummy/untyped_metrics/,count_for.ml Makefile)
-
-DISTRIB_FILES += $(wildcard $(PLUGIN_DISTRIBUTED_LIST)                   \
-                    $(PLUGIN_DIST_EXTERNAL_LIST)                         \
-                    $(PLUGIN_DIST_DOC_LIST) $(STANDALONE_PLUGINS_FILES))
-DISTRIB_FILES:=$(filter-out $(GENERATED) $(PLUGIN_GENERATED_LIST),\
-                  $(DISTRIB_FILES))
-
-DISTRIB_TESTS += $(wildcard $(PLUGIN_DIST_TESTS_LIST)) 
-
-
-SPECIFIED_OPEN_SOURCE:=$(OPEN_SOURCE)
-OPEN_SOURCE  ?= no
-
-ifneq ($(OPEN_SOURCE),yes)
-# close source version
-DISTRIB_HEADERS:=close-source
-DISTRIB_PROPRIETARY_HEADERS:=
-else
-# open source version
-DISTRIB_HEADERS:=open-source
-# for checking that distributed files aren't under proprietary licence.
-DISTRIB_PROPRIETARY_HEADERS:=$(CEA_PROPRIETARY_HEADERS)
-# DISTRIB_TESTS contents files that can be distributed without header checking
-DISTRIB_TESTS:=$(filter-out $(CEA_PROPRIETARY_FILES) ,\
-                  $(DISTRIB_TESTS))
-# DISTRIB_FILES contents files that can be distributed with header checking
-DISTRIB_FILES:=$(filter-out $(CEA_PROPRIETARY_FILES) ,\
-                  $(DISTRIB_FILES))
-endif
-
-# Set some variables for `headers`target.
-ifeq ($(OPEN_SOURCE),$(SPECIFIED_OPEN_SOURCE))
-# The OPEN_SOURCE variable is specified. So, use it for `make headers`
-HDRCK_OPEN_SOURCE=$(SPECIFIED_OPEN_SOURCE)
-HDRCK_DISTRIB_HEADERS=$(DISTRIB_HEADERS)
-HDRCK_DISTRIB_HEADER_DIRS=$(DISTRIB_HEADER_DIRS)
-else
-# The OPEN_SOURCE variable is unspecified. So, use open-source default for `make headers`
-HDRCK_OPEN_SOURCE=unspecified
-HDRCK_DISTRIB_HEADERS=open-source
-HDRCK_DISTRIB_HEADER_DIRS?=$(addsuffix /$(HDRCK_DISTRIB_HEADERS),$(HEADER_DIRS))
-endif
-
-# Variables governing the name of the generated .tar.gz.
-# Optionally define them as empty to silence warnings about undefined variables
-CLIENT ?=
-
-DISTRIB_DIR=tmp
-ifeq ("$(CLIENT)","")
-VERSION_NAME:=$(VERSION)
-else
-VERSION_NAME:=$(VERSION)-$(CLIENT)
-endif
-
-DISTRIB?=frama-c-$(VERSION_NAME)-$(VERSION_CODENAME)
-CLIENT_DIR=$(DISTRIB_DIR)/$(DISTRIB)
-
-
-# useful parameters:
-# CLIENT: name of the client (in the version number, the archive name, etc)
-# DISTRIB: name of the generated tarball and of the root tarball directory
-# OPEN_SOURCE: set it to 'yes' if you want to exclude close source files
-# note: make headers has to be applied...
-src-distrib: $(HDRCK) check-headers
-ifeq ("$(CLIENT)","")
-	$(PRINT_BUILD) "$(DISTRIB_HEADERS) tarball $(DISTRIB) (OPEN_SOURCE=$(OPEN_SOURCE))"
-else
-	$(PRINT_BUILD) "$(DISTRIB_HEADERS) tarball $(DISTRIB) for $(CLIENT) (OPEN_SOURCE=$(OPEN_SOURCE))"
-endif
-	$(RM) -r $(CLIENT_DIR)
-	$(MKDIR) -p $(CLIENT_DIR)
-	@#Workaround to avoid "argument list too long" in make 3.82+ without
-	@#using 'file' built-in, only available on make 4.0+
-	@#for make 4.0+, using the 'file' function could be a better solution,
-	@#although it seems to segfault in 4.0 (but not in 4.1)
-	$(RM) file_list_to_archive.tmp
-	@$(foreach file,$(DISTRIB_FILES) $(DISTRIB_TESTS),\
-			echo $(file) | $(SED) 's/@/ /g' >> file_list_to_archive.tmp$(NEWLINE))
-	$(TAR) -cf - --files-from file_list_to_archive.tmp | $(TAR) -C $(CLIENT_DIR) -xf -
-	$(RM) file_list_to_archive.tmp
-	$(PRINT_MAKING) files
-	(cd $(CLIENT_DIR) ; \
-	   echo "$(VERSION_NAME)" > VERSION && \
-	   DISTRIB_CONF=yes autoconf > ../../.log.autoconf 2>&1)
-	$(MKDIR) $(CLIENT_DIR)/bin
-	$(MKDIR) $(CLIENT_DIR)/lib/plugins
-	$(MKDIR) $(CLIENT_DIR)/lib/gui
-	$(RM) ../$(DISTRIB).tar.gz
-	$(PRINT) "Updating files to archive with $(DISTRIB_HEADERS) headers"
-	$(HDRCK) \
-		$(HDRCK_EXTRA) \
-		-update -C $(CLIENT_DIR) \
-		$(addprefix -header-dirs ,$(DISTRIB_HEADER_DIRS)) \
-		-headache-config-file ./headers/headache_config.txt \
-		$(HEADER_SPEC_FILE)
-	$(PRINT_TAR) $(DISTRIB).tar.gz
-	(cd $(DISTRIB_DIR); $(TAR) cf - \
-			--numeric-owner --owner=0 --group=0 --sort=name \
-			--mtime="$$(date +"%F") Z" --mode='a+rw' \
-			--exclude "*autom4te.cache*" \
-			$(DISTRIB) | gzip -9 -n > ../$(DISTRIB).tar.gz \
-	)
-	$(PRINT_RM) $(DISTRIB_DIR)
-	$(RM) -r $(DISTRIB_DIR)
-
-doc-companions:
-	$(MAKE) -C doc/developer archives VERSION=$(VERSION)-$(VERSION_CODENAME)
-	$(MV) doc/developer/hello-$(VERSION)-$(VERSION_CODENAME).tar.gz hello-$(VERSION)-$(VERSION_CODENAME).tar.gz
-	$(ECHO) "The documentation companion hello-$(VERSION)-$(VERSION_CODENAME).tar.gz has been generated."
-
-clean-distrib: dist-clean
-	$(PRINT_RM) distrib
-	$(RM) -r $(DISTRIB_DIR) $(DISTRIB).tar.gz
-
-create_lib_to_install_list = $(addprefix $(FRAMAC_LIB)/,$(call map,notdir,$(1)))
-
-byte:: bin/toplevel.byte$(EXE) lib/fc/frama-c.cma share/Makefile.dynamic_config \
-	$(call create_lib_to_install_list,$(LIB_BYTE_TO_INSTALL)) \
-      $(PLUGIN_META_LIST) lib/fc/META.frama-c
-
-opt:: bin/toplevel.opt$(EXE) lib/fc/frama-c.cmxa share/Makefile.dynamic_config \
-	$(call create_lib_to_install_list,$(LIB_OPT_TO_INSTALL)) \
-	$(filter %.o %.cmi,\
-	   $(call create_lib_to_install_list,$(LIB_BYTE_TO_INSTALL))) \
-      $(PLUGIN_META_LIST) lib/fc/META.frama-c
-
-top: bin/toplevel.top$(EXE) \
-	$(call create_lib_to_install_list,$(LIB_BYTE_TO_INSTALL)) \
-      $(PLUGIN_META_LIST)
-
-##################
-# Copy in lib/fc #
-##################
-
-define copy_in_lib
-$(FRAMAC_LIB)/$(notdir $(1)): $(1)
-	$(MKDIR) $(FRAMAC_LIB)
-	$(CP) $$< $$@
-
-endef
-$(eval $(foreach file,$(LIB_BYTE_TO_INSTALL),$(call copy_in_lib,$(file))))
-$(eval $(foreach file,$(LIB_OPT_TO_INSTALL),$(call copy_in_lib,$(file))))
-
-################
-# Generic part #
-################
-
-$(NON_OPAQUE_DEPS:%=%.cmx): OFLAGS := $(OFLAGS) -w -58
-
-$(CROWBAR_AFL_TARGET:%=%.cmx): OFLAGS:=$(OFLAGS) -afl-instrument
-
-include share/Makefile.generic
+include share/Makefile.documentation
 
 ###############################################################################
 # Local Variables:

Makefile.generating

-##########################################################################
-#                                                                        #
-#  This file is part of Frama-C.                                         #
-#                                                                        #
-#  Copyright (C) 2007-2020                                               #
-#    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).            #
-#                                                                        #
-##########################################################################
-
-ptests/ptests_config.ml: Makefile.generating share/Makefile.config
-	$(PRINT_MAKING) $@
-	$(RM) $@
-	$(TOUCH) $@
-	$(CHMOD_RO) $@
-
-tests/ptests_config: Makefile.generating share/Makefile.config
-	$(PRINT_MAKING) $@
-	$(RM) $@
-	$(TOUCH) $@
-	$(ECHO) "DEFAULT_SUITES=$(PLUGIN_TESTS_LIST)" >> $@
-	$(ECHO) "TOPLEVEL_PATH=bin/toplevel.$(OCAMLBEST)$(EXE)" >> $@
-	$(ECHO) "OCAMLRUNPARAM=" >> $@
-	$(ECHO) "FRAMAC_SESSION=." >> $@
-	$(ECHO) "FRAMAC_SHARE=./share" >> $@
-	$(ECHO) "FRAMAC_PLUGIN=./lib/plugins" >> $@
-	$(ECHO) "FRAMAC_PLUGIN_GUI=./lib/plugins/gui" >> $@
-	$(ECHO) "FRAMAC_LIB=./lib/fc" >> $@
-	$(CHMOD_RO) $@
-
-ALL_LIBRARY_NAMES=$(shell ocamlfind query -r -p-format $(LIBRARY_NAMES) $(LIBRARY_NAMES_GUI))
-MAJOR_VERSION=$(shell $(SED) -E 's/^([0-9]+)\..*/\1/' VERSION)
-MINOR_VERSION=$(shell $(SED) -E 's/^[0-9]+\.([0-9]+).*/\1/' VERSION)
-
-$(CONFIG_FILE): $(CONFIG_FILE).in VERSION VERSION_CODENAME share/Makefile.config Makefile.generating configure.in
-	$(SED) \
-	  -e "s|@VERSION@|$(VERSION)|" \
-          -e "s|@VERSION_CODENAME@|$(VERSION_CODENAME)|" \
-          -e "s|@CURR_DATE@|$$(LC_ALL=C date)|" \
-          -e "s|@LABLGTK@|$(LABLGTK)|" \
-	  -e "s|@OCAMLC@|$(OCAMLC)|" \
-          -e "s|@OCAMLOPT@|$(OCAMLOPT)|" \
-	  -e "s|@WARNINGS@|$(WARNINGS)|" \
-          -e "s|@FRAMAC_DATADIR@|$(FRAMAC_DATADIR)|" \
-	  -e "s|@FRAMAC_LIBDIR@|$(FRAMAC_LIBDIR)|" \
-	  -e "s|@FRAMAC_ROOT_SRCDIR@|$(FRAMAC_ROOT_SRCDIR)|" \
-	  -e "s|@FRAMAC_PLUGINDIR@|$(FRAMAC_PLUGINDIR)|" \
-	  -e "s|@FRAMAC_DEFAULT_CPP@|$(FRAMAC_DEFAULT_CPP)|" \
-          -e "s|@FRAMAC_DEFAULT_CPP_ARGS@|$(FRAMAC_DEFAULT_CPP_ARGS)|" \
-	  -e "s|@FRAMAC_GNU_CPP@|$(FRAMAC_GNU_CPP)|" \
-          -e "s|@DEFAULT_CPP_KEEP_COMMENTS@|$(DEFAULT_CPP_KEEP_COMMENTS)|" \
-          -e "s|@DEFAULT_CPP_SUPPORTED_ARCH_OPTS@|$(DEFAULT_CPP_SUPPORTED_ARCH_OPTS)|" \
-          -e "s|@COMPILATION_UNITS@|$(COMPILATION_UNITS)|" \
-          -e "s|@LIBRARY_NAMES@|$(foreach p,$(ALL_LIBRARY_NAMES),\"$p\";)|" \
-	  -e "s|@OPTDOT@|$(OPTDOT)|" \
-          -e "s|@EXE@|$(EXE)|" \
-          -e "s|@MAJOR_VERSION@|$(MAJOR_VERSION)|" \
-          -e "s|@MINOR_VERSION@|$(MINOR_VERSION)|" \
-          $< > $@.tmp
-	@touch -r $@.tmp $<
-	$(CP_IF_DIFF) $@.tmp $@
-	$(RM) $@.tmp
-	$(CHMOD_RO) $@
-
-ifeq ("$(LOCAL_MACHDEP)","yes")
-
-MACHDEP_PATH=share
-
-# Create the machine dependency module
-# If the cl command cannot be run then the MSVC part will be identical to GCC
-.PHONY : machdep $(MACHDEP_PATH)/local_machdep.ml
-machdep: $(MACHDEP_PATH)/local_machdep.ml
-bin/machdep.exe: machdep
-
-config.h: 
-	$(PRINT_MAKING) $@
-	$(ECHO) "missing config.h file generated at configure stage using --enable-localmachdep option."
-	exit 1;
-
-$(MACHDEP_PATH)/local_machdep.ml: \
-  $(MACHDEP_PATH)/machdep.c config.h Makefile.generating
-	$(PRINT_MAKING) $@
-	$(RM) $@
-	$(ECHO) "(* This module was generated automatically by code in Makefile and machdep.c *)" >$@
-# Now generate the type definition
-	$(ECHO) "open Cil_types" >> $@
-	if $(CC) -D_GNUCC $< -o bin/machdep.exe ;then \
-	    $(ECHO) "machdep.exe created successfully."; \
-	else \
-	    $(RM) $@; exit 1; \
-	fi
-	$(ECHO) "let gcc = {" >>$@
-	./bin/machdep.exe >>$@
-	$(ECHO) "	 underscore_name = $(UNDERSCORE_NAME) ;" >> $@
-	$(ECHO) "}"          >>$@
-	if cl /D_MSVC $< /Febin/machdep.exe /Fobin/machdep.obj ;then \
-	   $(ECHO) "let hasMSVC = true" >>$@; \
-	else \
-	   $(ECHO) "let hasMSVC = false" >>$@; \
-	fi
-	$(ECHO) "let msvc = {" >>$@
-	./bin/machdep.exe >>$@
-	$(ECHO) "	 underscore_name = true ;" >> $@
-	$(ECHO) "}"          >>$@
-	$(ECHO) \
-	  "let gccHas__builtin_va_list = $(HAVE_BUILTIN_VA_LIST)" >>$@
-	$(ECHO) \
-	  "$@ generated. You may have this file merged into Frama-C by developers."
-	$(CHMOD_RO) $@
-
-endif
-
-# transitioning.ml
-
-GENERATED+= src/libraries/utils/json.ml src/libraries/stdlib/transitioning.ml
-
-src/libraries/stdlib/transitioning.ml: \
-  src/libraries/stdlib/transitioning.ml.in \
-  Makefile.generating share/Makefile.config
-	$(PRINT_MAKING) $@
-	rm -f $@
-	cat $< > $@
-	$(CHMOD_RO) $@
-
-##################
-# Frama-C-config #
-##################
-
-src/kernel_internals/runtime/frama_c_config.ml: src/kernel_internals/runtime/fc_config.ml \
-	src/kernel_internals/runtime/frama_c_config.ml.in Makefile.generating
-	$(PRINT_MAKING) $@
-	$(RM) $@
-	$(ECHO) "module Filepath = struct let add_symbolic_dir _ _ = () end" >> $@
-	$(ECHO) "module Fc_config = struct" >> $@
-	$(CAT) src/kernel_internals/runtime/fc_config.ml >> $@
-	$(ECHO) "end" >> $@
-	$(CAT) src/kernel_internals/runtime/frama_c_config.ml.in >> $@
-	$(CHMOD_RO) $@
-
-GENERATED+= src/kernel_internals/runtime/frama_c_config.ml
-
-bin/fc-config$(EXE): src/kernel_internals/runtime/frama_c_config.ml
-ifeq ($(OCAMLBEST),opt)
-	$(OCAMLOPT) str.cmxa $< -o $@
-else
-	$(OCAMLC) str.cma $< -o $@
-endif
-
-# Merlin #
-
-.PHONY:merlin
-.merlin merlin: share/Makefile.config Makefile.generating
-#create Merlin file
-	$(PRINT_MAKING) $@
-	echo "FLG -c $(FLAGS) $(FRAMAC_USER_MERLIN_FLAGS)" > .merlin
-	for PKG in $(LIBRARY_NAMES); do echo PKG $$PKG >> .merlin; done
-	for PKG in $(LIBRARY_NAMES_GUI); do echo PKG $$PKG >> .merlin; done
-	for PKG in $(MERLIN_PACKAGES); do echo PKG $$PKG >> .merlin; done
-	echo "B lib/plugins" >> .merlin
-	echo "B lib/plugins/gui" >> .merlin
-	find src \( -name '.*' -o -name tests -o -name doc -o -name '*.cache' \) -prune \
-	      -o \( -type d -exec printf "B %s\n" {} \; -exec printf "S %s\n" {} \; \) >> .merlin
-
-ifeq ("$(DEVELOPMENT)","yes")
-all:: .merlin
-endif
-
-lib/fc/META.frama-c: share/META.frama-c share/Makefile.config Makefile.generating
-	$(MKDIR) lib/fc/
-	$(SED) "s/@REQUIRES/$(LIBRARY_NAMES)/" $< > $@
-
-GENERATED += lib/fc/META.frama-c
-
-
-# Local Variables:
-# mode: makefile
-# End:

README.md

 ![Frama-C](share/frama-c.png?raw=true)
 
-[Frama-C](http://frama-c.com) is a platform dedicated to the analysis of
+[Frama-C](https://frama-c.com) is a platform dedicated to the analysis of
 source code written in C.
 
 ## A Collaborative Platform
@@ -12,7 +12,6 @@ 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**);
@@ -23,28 +22,45 @@ Thanks to this approach, Frama-C provides sophisticated tools, including:
   (**From**, **Impact**, **Metrics**, **Occurrence**, **Scope**, etc.).
 
 These plug-ins share a common language and can exchange information via
-**[ACSL](http://frama-c.com/acsl.html)** (*ANSI/ISO C Specification Language*)
+**[ACSL](https://frama-c.com/acsl.html)** (*ANSI/ISO C Specification Language*)
 properties. Plug-ins can also collaborate via their APIs.
 
 ## Installation
 
-For more detailed information about installing opam/Frama-C,
-see [INSTALL.md](INSTALL.md).
-
-Frama-C is available through [opam](http://opam.ocaml.org/), the
-OCaml package manager. This is the preferred installation method. Be sure
-to install opam v2.0 or higher. Then the following sequence of commands
-should install frama-c and its gui:
+Frama-C is available through [opam](https://opam.ocaml.org/), the
+OCaml package manager. If you have it, simply run:
 
-    opam init
-    opam install depext
-    opam depext frama-c
     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.
@@ -54,18 +70,20 @@ Frama-C can be run from the command-line, or via its graphical interface.
 The recommended usage for simple files is one of the following lines:
 
     frama-c file.c -<plugin> [options]
-    frama-c-gui file.c
+    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 GUI.
+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 several
+(`-<plugin>-help` or `-<plugin>-h`) that describes its own
 options.
 
 Finally, the list of options governing the behavior of Frama-C's kernel itself
@@ -75,44 +93,47 @@ is available through
 
 #### Complex scenarios
 
-For more complex usage scenarios (lots of files and directories,
-with several preprocessing directives), we recommend splitting Frama-C's usage
-in two parts:
+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 typically involves giving extra arguments to the C preprocessor,
-so the `-cpp-extra-args` option is often useful, as in the example below:
+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 *.h -cpp-extra-args="-D<define> -I<include>" -save parsed.sav
+    frama-c *.c -cpp-extra-args="-D<define> -I<include>" -save parsed.sav
 
-The results are then loaded into Frama-C for further analyses or for inspection
+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]
-    frama-c-gui -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> http://frama-c.com/download.html
+  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](http://stackoverflow.com/questions/tagged/frama-c) has several
+- [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](http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss)
+- 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.
-
-- The [Frama-C wiki](https://bts.frama-c.com/dokuwiki/doku.php?id=mantis:frama-c:start)
-  has some useful information, although it is not entirely up-to-date.
-
-- The [Frama-C blog](http://pub.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.
+  These [contribution guidelines](CONTRIBUTING.md) detail how to submit
+  issues or create merge requests.