.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/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>
\ No newline at end of file
+<mounir.assaf@cea.fr> <mounir.assaf@cea.Fr>

.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;
 

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.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.