diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 3661466d0917085a1a23043c43d51072442a2891..0a827b81ef53e13958a4c524eb3340285334cec0 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -191,11 +191,18 @@ frama-c-ocaml-4.09:
only:
- schedules
-frama-c-ocaml-4.10:
+frama-c-ocaml-4.12:
variables:
- OCAML: "4_10"
+ OCAML: "4_12"
<<: *frama-c-ocaml
+# check compatibility with future OCaml version
+frama-c-ocaml-4.13:
+ variables:
+ OCAML: "4_13"
+ <<: *frama-c-ocaml
+ allow_failure: true
+
caveat-importer:
stage: tests
diff --git a/Makefile b/Makefile
index 92ef5cef19d044f71cc5fc75009be091bc127b3d..2a2deee009cc7689efb5546f0152270fca641318 100644
--- a/Makefile
+++ b/Makefile
@@ -1426,7 +1426,7 @@ else
$(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))))
+ $(eval $(file:%.ml=%.cmo): BFLAGS+=-w -70 -I $(dir $(file))))
$(foreach file,$(LONELY_TESTS_ML_FILES),\
$(eval $(file:%.ml=%.cmx): OFLAGS+=-I $(dir $(file))))
$(foreach file,$(LONELY_TESTS_ML_FILES),\
diff --git a/headers/header_spec.txt b/headers/header_spec.txt
index a4e5710b9a2d44bc536f923227f81f97ec83cff3..7a47b2372ac463babda41ffa1acc5d37227c1bca 100644
--- a/headers/header_spec.txt
+++ b/headers/header_spec.txt
@@ -388,6 +388,7 @@ src/kernel_internals/parsing/logic_preprocess.mli: CEA_INRIA_LGPL
src/kernel_internals/parsing/logic_preprocess.mll: CEA_INRIA_LGPL
src/kernel_internals/runtime/README.md: .ignore
src/kernel_internals/runtime/boot.ml: CEA_LGPL
+src/kernel_internals/runtime/boot.mli: CEA_LGPL
src/kernel_internals/runtime/dump_config.ml: CEA_LGPL
src/kernel_internals/runtime/dump_config.mli: CEA_LGPL
src/kernel_internals/runtime/fc_config.ml.in: CEA_LGPL
@@ -756,9 +757,11 @@ src/plugins/aorai/aorai_metavariables.mli: AORAI_LGPL
src/plugins/aorai/aorai_option.ml: AORAI_LGPL
src/plugins/aorai/aorai_option.mli: AORAI_LGPL
src/plugins/aorai/aorai_register.ml: AORAI_LGPL
+src/plugins/aorai/aorai_register.mli: AORAI_LGPL
src/plugins/aorai/aorai_utils.ml: AORAI_LGPL
src/plugins/aorai/aorai_utils.mli: AORAI_LGPL
src/plugins/aorai/aorai_visitors.ml: AORAI_LGPL
+src/plugins/aorai/aorai_visitors.mli: AORAI_LGPL
src/plugins/aorai/bool3.ml: AORAI_LGPL
src/plugins/aorai/bool3.mli: AORAI_LGPL
src/plugins/aorai/configure.ac: AORAI_LGPL
@@ -769,17 +772,23 @@ src/plugins/aorai/logic_simplification.mli: AORAI_LGPL
src/plugins/aorai/ltl_output.ml: AORAI_LGPL
src/plugins/aorai/ltl_output.mli: AORAI_LGPL
src/plugins/aorai/ltlast.mli: AORAI_LGPL
+src/plugins/aorai/ltllexer.mli: AORAI_LGPL
src/plugins/aorai/ltllexer.mll: AORAI_LGPL
src/plugins/aorai/ltlparser.mly: AORAI_LGPL
src/plugins/aorai/path_analysis.ml: AORAI_LGPL
+src/plugins/aorai/path_analysis.mli: AORAI_LGPL
src/plugins/aorai/promelaast.mli: AORAI_LGPL
+src/plugins/aorai/promelalexer.mli: AORAI_LGPL
src/plugins/aorai/promelalexer.mll: AORAI_LGPL
+src/plugins/aorai/promelalexer_withexps.mli: AORAI_LGPL
src/plugins/aorai/promelalexer_withexps.mll: AORAI_LGPL
src/plugins/aorai/promelaoutput.ml: AORAI_LGPL
src/plugins/aorai/promelaoutput.mli: AORAI_LGPL
src/plugins/aorai/promelaparser.mly: AORAI_LGPL
src/plugins/aorai/promelaparser_withexps.mly: AORAI_LGPL
src/plugins/aorai/utils_parser.ml: AORAI_LGPL
+src/plugins/aorai/utils_parser.mli: AORAI_LGPL
+src/plugins/aorai/yalexer.mli: AORAI_LGPL
src/plugins/aorai/yalexer.mll: AORAI_LGPL
src/plugins/aorai/yaparser.mly: AORAI_LGPL
src/plugins/callgraph/Callgraph.mli: CEA_LGPL_OR_PROPRIETARY
@@ -792,6 +801,7 @@ src/plugins/callgraph/journalize.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/callgraph/options.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/callgraph/options.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/callgraph/register.ml: CEA_LGPL_OR_PROPRIETARY
+src/plugins/callgraph/register.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/callgraph/services.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/callgraph/services.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/callgraph/subgraph.ml: CEA_LGPL_OR_PROPRIETARY
@@ -815,6 +825,7 @@ src/plugins/dive/dive_graph.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/dive/dive_types.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/dive/Dive.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/dive/main.ml: CEA_LGPL_OR_PROPRIETARY
+src/plugins/dive/main.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/dive/Makefile.in: CEA_LGPL_OR_PROPRIETARY
src/plugins/dive/node_kind.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/dive/node_kind.mli: CEA_LGPL_OR_PROPRIETARY
@@ -913,7 +924,9 @@ src/plugins/impact/options.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/impact/pdg_aux.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/impact/pdg_aux.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/impact/reason_graph.ml: CEA_LGPL_OR_PROPRIETARY
+src/plugins/impact/reason_graph.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/impact/register.ml: CEA_LGPL_OR_PROPRIETARY
+src/plugins/impact/register.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/impact/register_gui.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/impact/register_gui.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/inout/Inout.mli: CEA_LGPL_OR_PROPRIETARY
@@ -927,9 +940,11 @@ src/plugins/inout/inout_parameters.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/inout/inputs.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/inout/inputs.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/inout/operational_inputs.ml: CEA_LGPL_OR_PROPRIETARY
+src/plugins/inout/operational_inputs.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/inout/outputs.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/inout/outputs.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/inout/register.ml: CEA_LGPL_OR_PROPRIETARY
+src/plugins/inout/register.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/loop_analysis/.gitignore: .ignore
src/plugins/loop_analysis/Makefile.in: CEA_LGPL_OR_PROPRIETARY
src/plugins/loop_analysis/LoopAnalysis.mli: CEA_LGPL_OR_PROPRIETARY
@@ -941,10 +956,11 @@ src/plugins/loop_analysis/options.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/loop_analysis/options.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/loop_analysis/region_analysis.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/loop_analysis/region_analysis.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/loop_analysis/region_analysis_sig.ml: CEA_LGPL_OR_PROPRIETARY
+src/plugins/loop_analysis/region_analysis_sig.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/loop_analysis/region_analysis_stmt.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/loop_analysis/region_analysis_stmt.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/loop_analysis/register.ml: CEA_LGPL_OR_PROPRIETARY
+src/plugins/loop_analysis/register.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/markdown-report/configure.ac: CEA_LGPL
src/plugins/markdown-report/eva_info.ml: CEA_LGPL
src/plugins/markdown-report/eva_info.mli: CEA_LGPL
@@ -961,9 +977,11 @@ src/plugins/markdown-report/parse_remarks.mli: CEA_LGPL
src/plugins/markdown-report/sarif_gen.ml: CEA_LGPL
src/plugins/markdown-report/sarif_gen.mli: CEA_LGPL
src/plugins/markdown-report/sarif.ml: CEA_LGPL
+src/plugins/markdown-report/sarif.mli: CEA_LGPL
src/plugins/markdown-report/share/acsl.xml: CEA_LGPL
src/plugins/metrics/Metrics.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/metrics/css_html.ml: CEA_LGPL_OR_PROPRIETARY
+src/plugins/metrics/css_html.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/metrics/metrics_acsl.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/metrics/metrics_acsl.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/metrics/metrics_base.ml: CEA_LGPL_OR_PROPRIETARY
@@ -979,13 +997,16 @@ src/plugins/metrics/metrics_gui.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/metrics/metrics_parameters.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/metrics/metrics_parameters.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/metrics/register.ml: CEA_LGPL_OR_PROPRIETARY
+src/plugins/metrics/register.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/metrics/register_gui.ml: CEA_LGPL_OR_PROPRIETARY
+src/plugins/metrics/register_gui.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/nonterm/.gitignore: .ignore
src/plugins/nonterm/Makefile.in: CEA_LGPL_OR_PROPRIETARY
src/plugins/nonterm/Nonterm.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/nonterm/README.md: .ignore
src/plugins/nonterm/configure.ac: CEA_LGPL_OR_PROPRIETARY
src/plugins/nonterm/nonterm_run.ml: CEA_LGPL_OR_PROPRIETARY
+src/plugins/nonterm/nonterm_run.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/obfuscator/.gitignore: .ignore
src/plugins/obfuscator/Makefile.in: CEA_LGPL_OR_PROPRIETARY
src/plugins/obfuscator/Obfuscator.mli: CEA_LGPL_OR_PROPRIETARY
@@ -997,12 +1018,14 @@ src/plugins/obfuscator/obfuscate.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/obfuscator/obfuscator_kind.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/obfuscator/obfuscator_kind.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/obfuscator/obfuscator_register.ml: CEA_LGPL_OR_PROPRIETARY
+src/plugins/obfuscator/obfuscator_register.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/obfuscator/options.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/obfuscator/options.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/occurrence/Occurrence.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/occurrence/options.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/occurrence/options.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/occurrence/register.ml: CEA_LGPL_OR_PROPRIETARY
+src/plugins/occurrence/register.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/occurrence/register_gui.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/occurrence/register_gui.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/instantiate/basic_blocks.ml: CEA_LGPL_OR_PROPRIETARY
@@ -1035,6 +1058,7 @@ src/plugins/instantiate/string/memset.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/instantiate/options.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/instantiate/options.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/instantiate/register.ml: CEA_LGPL_OR_PROPRIETARY
+src/plugins/instantiate/register.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/instantiate/transform.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/instantiate/transform.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/pdg/Pdg.mli: CEA_LGPL_OR_PROPRIETARY
@@ -1051,6 +1075,7 @@ src/plugins/pdg/pdg_parameters.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/pdg/pdg_state.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/pdg/pdg_state.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/pdg/register.ml: CEA_LGPL_OR_PROPRIETARY
+src/plugins/pdg/register.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/pdg/sets.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/pdg/sets.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/pdg_types/pdgIndex.ml: CEA_LGPL_OR_PROPRIETARY
@@ -1061,26 +1086,29 @@ src/plugins/pdg_types/pdgTypes.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/pdg_types/pdgTypes.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/postdominators/Postdominators.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/postdominators/compute.ml: CEA_LGPL_OR_PROPRIETARY
+src/plugins/postdominators/compute.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/postdominators/postdominators_parameters.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/postdominators/postdominators_parameters.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/postdominators/print.ml: CEA_LGPL_OR_PROPRIETARY
+src/plugins/postdominators/print.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/print_api/.gitignore: .ignore
src/plugins/print_api/Makefile: CEA_LGPL
src/plugins/print_api/Print_api.mli: CEA_LGPL
src/plugins/print_api/grammar.mly: CEA_LGPL
src/plugins/print_api/lexer.mll: CEA_LGPL
+src/plugins/print_api/lexer.mli: CEA_LGPL
src/plugins/print_api/print_interface.ml: CEA_LGPL
+src/plugins/print_api/print_interface.mli: CEA_LGPL
src/plugins/qed/.gitignore: .ignore
src/plugins/qed/.ocp-indent: .ignore
src/plugins/qed/Makefile: CEA_WP
-src/plugins/qed/QedGui.ml: CEA_WP
src/plugins/qed/bvars.ml: CEA_WP
src/plugins/qed/bvars.mli: CEA_WP
src/plugins/qed/cache.ml: CEA_WP
src/plugins/qed/cache.mli: CEA_WP
src/plugins/qed/collection.ml: CEA_WP
src/plugins/qed/collection.mli: CEA_WP
-src/plugins/qed/engine.ml: CEA_WP
+src/plugins/qed/engine.mli: CEA_WP
src/plugins/qed/export.ml: CEA_WP
src/plugins/qed/export.mli: CEA_WP
src/plugins/qed/export_altergo.ml: CEA_WP
@@ -1107,7 +1135,7 @@ src/plugins/qed/listmap.ml: CEA_WP
src/plugins/qed/listmap.mli: CEA_WP
src/plugins/qed/listset.ml: CEA_WP
src/plugins/qed/listset.mli: CEA_WP
-src/plugins/qed/logic.ml: CEA_WP
+src/plugins/qed/logic.mli: CEA_WP
src/plugins/qed/mergemap.ml: CEA_WP
src/plugins/qed/mergemap.mli: CEA_WP
src/plugins/qed/mergeset.ml: CEA_WP
@@ -1132,6 +1160,7 @@ src/plugins/reduc/misc.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/reduc/reduc_options.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/reduc/reduc_options.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/reduc/register.ml: CEA_LGPL_OR_PROPRIETARY
+src/plugins/reduc/register.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/reduc/value2acsl.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/reduc/value2acsl.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/report/.gitignore: .ignore
@@ -1158,6 +1187,7 @@ src/plugins/rte/generator.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/rte/options.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/rte/options.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/rte/register.ml: CEA_LGPL_OR_PROPRIETARY
+src/plugins/rte/register.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/rte/rte.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/rte/rte.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/rte/visit.ml: CEA_LGPL_OR_PROPRIETARY
@@ -1189,7 +1219,9 @@ src/plugins/server/server_doc.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/server/server_parameters.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/server/server_parameters.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/server/server_batch.ml: CEA_LGPL_OR_PROPRIETARY
+src/plugins/server/server_batch.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/server/server_zmq.ml: CEA_LGPL_OR_PROPRIETARY
+src/plugins/server/server_zmq.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/server/states.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/server/states.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/scope/Scope.mli: CEA_LGPL_OR_PROPRIETARY
@@ -1198,6 +1230,7 @@ src/plugins/scope/datascope.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/scope/defs.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/scope/defs.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/scope/dpds_gui.ml: CEA_LGPL_OR_PROPRIETARY
+src/plugins/scope/dpds_gui.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/scope/zones.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/scope/zones.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/security_slicing/.gitignore: .ignore
@@ -1212,12 +1245,14 @@ src/plugins/security_slicing/security_slicing_parameters.ml: CEA_LGPL_OR_PROPRIE
src/plugins/security_slicing/security_slicing_parameters.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/slicing/Slicing.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/slicing/api.ml: CEA_LGPL_OR_PROPRIETARY
+src/plugins/slicing/api.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/slicing/bts336.c: .ignore
src/plugins/slicing/fct_slice.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/slicing/fct_slice.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/slicing/printSlice.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/slicing/printSlice.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/slicing/register.ml: CEA_LGPL_OR_PROPRIETARY
+src/plugins/slicing/register.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/slicing/register_gui.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/slicing/register_gui.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/slicing/slicingActions.ml: CEA_LGPL_OR_PROPRIETARY
@@ -1225,6 +1260,7 @@ src/plugins/slicing/slicingActions.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/slicing/slicingCmds.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/slicing/slicingCmds.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/slicing/slicingInternals.ml: CEA_LGPL_OR_PROPRIETARY
+src/plugins/slicing/slicingInternals.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/slicing/slicingMacros.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/slicing/slicingMacros.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/slicing/slicingMarks.ml: CEA_LGPL_OR_PROPRIETARY
@@ -1234,19 +1270,24 @@ src/plugins/slicing/slicingParameters.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/slicing/slicingProject.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/slicing/slicingProject.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/slicing/slicingSelect.ml: CEA_LGPL_OR_PROPRIETARY
+src/plugins/slicing/slicingSelect.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/slicing/slicingState.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/slicing/slicingState.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/slicing/slicingTransform.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/slicing/slicingTransform.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/slicing/slicingTypes.ml: CEA_LGPL_OR_PROPRIETARY
+src/plugins/slicing/slicingTypes.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/sparecode/Sparecode.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/sparecode/globs.ml: CEA_LGPL_OR_PROPRIETARY
+src/plugins/sparecode/globs.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/sparecode/register.ml: CEA_LGPL_OR_PROPRIETARY
+src/plugins/sparecode/register.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/sparecode/spare_marks.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/sparecode/spare_marks.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/sparecode/sparecode_params.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/sparecode/sparecode_params.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/sparecode/transform.ml: CEA_LGPL_OR_PROPRIETARY
+src/plugins/sparecode/transform.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/studia/Makefile.in: CEA_LGPL_OR_PROPRIETARY
src/plugins/studia/configure.ac: CEA_LGPL_OR_PROPRIETARY
src/plugins/studia/options.ml: CEA_LGPL_OR_PROPRIETARY
@@ -1262,6 +1303,7 @@ src/plugins/studia/writes.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/studia/writes.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/users/Users.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/users/users_register.ml: CEA_LGPL_OR_PROPRIETARY
+src/plugins/users/users_register.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/value/Changelog_non_free: .ignore
src/plugins/value/Eva.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/value/alarmset.ml: CEA_LGPL_OR_PROPRIETARY
@@ -1495,7 +1537,9 @@ src/plugins/variadic/Makefile.in: CEA_LGPL_OR_PROPRIETARY
src/plugins/variadic/configure.ac: CEA_LGPL_OR_PROPRIETARY
src/plugins/variadic/Variadic.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/variadic/classify.ml: CEA_LGPL_OR_PROPRIETARY
+src/plugins/variadic/classify.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/variadic/environment.ml: CEA_LGPL_OR_PROPRIETARY
+src/plugins/variadic/environment.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/variadic/extends.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/variadic/extends.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/variadic/format_parser.ml: CEA_LGPL_OR_PROPRIETARY
@@ -1503,17 +1547,22 @@ src/plugins/variadic/format_parser.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/variadic/format_pprint.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/variadic/format_pprint.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/variadic/format_string.ml: CEA_LGPL_OR_PROPRIETARY
+src/plugins/variadic/format_string.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/variadic/format_typer.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/variadic/format_typer.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/variadic/format_types.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/variadic/generic.ml: CEA_LGPL_OR_PROPRIETARY
+src/plugins/variadic/generic.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/variadic/options.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/variadic/options.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/variadic/register.ml: CEA_LGPL_OR_PROPRIETARY
+src/plugins/variadic/register.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/variadic/replacements.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/variadic/replacements.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/variadic/standard.ml: CEA_LGPL_OR_PROPRIETARY
+src/plugins/variadic/standard.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/variadic/translate.ml: CEA_LGPL_OR_PROPRIETARY
+src/plugins/variadic/translate.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/variadic/va_types.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/wp/.gitignore: .ignore
src/plugins/wp/.ocp-indent: .ignore
@@ -1613,7 +1662,7 @@ src/plugins/wp/MemVar.ml: CEA_WP
src/plugins/wp/MemVar.mli: CEA_WP
src/plugins/wp/MemZeroAlias.ml: CEA_WP
src/plugins/wp/MemZeroAlias.mli: CEA_WP
-src/plugins/wp/Sigs.ml: CEA_WP
+src/plugins/wp/Sigs.mli: CEA_WP
src/plugins/wp/Mstate.ml: CEA_WP
src/plugins/wp/Mstate.mli: CEA_WP
src/plugins/wp/Passive.ml: CEA_WP
@@ -1788,7 +1837,7 @@ src/plugins/wp/driver.mll: CEA_WP
src/plugins/wp/dyncall.ml: CEA_WP
src/plugins/wp/dyncall.mli: CEA_WP
src/plugins/wp/intro_wp.txt: CEA_WP
-src/plugins/wp/mcfg.ml: CEA_WP
+src/plugins/wp/mcfg.mli: CEA_WP
src/plugins/wp/normAtLabels.ml: CEA_WP
src/plugins/wp/normAtLabels.mli: CEA_WP
src/plugins/wp/proof.ml: CEA_WP
@@ -1796,6 +1845,7 @@ src/plugins/wp/proof.mli: CEA_WP
src/plugins/wp/prover.ml: CEA_WP
src/plugins/wp/prover.mli: CEA_WP
src/plugins/wp/register.ml: CEA_WP
+src/plugins/wp/register.mli: CEA_WP
src/plugins/wp/rformat.mli: CEA_WP
src/plugins/wp/rformat.mll: CEA_WP
src/plugins/wp/script.mli: CEA_WP
diff --git a/nix/default.nix b/nix/default.nix
index fb7bbc39f54dd5971f8d681234840499737b1c55..056c432610ae8f2b12e9b605b208f72106ebc248 100644
--- a/nix/default.nix
+++ b/nix/default.nix
@@ -2,16 +2,17 @@
{ pkgs, stdenv, src ? ../., opam2nix, ocaml ? pkgs.ocaml-ng.ocamlPackages_4_08.ocaml, plugins ? { } }:
let mydir = builtins.getEnv("PWD");
- mk-opam-selection = { name, opamSrc?null, ... }: {
+ mk-opam-selection = { name, opamSrc?{}, ... }: {
inherit ocaml;
src = opamSrc;
selection = "${mydir}/${name}-${ocaml.version}-opam-selection.nix";
};
- opamPackages =
+ opamPackages =
[ "ocamlfind" "zarith" "ocamlgraph" "yojson" "zmq"
"ppx_deriving" "ppx_deriving_yojson"
- "coq=8.12.0" "alt-ergo=2.2.0" "why3=1.4.0" "why3-coq=1.4.0" ];
-
+ "coq=8.13.0" "alt-ergo=2.2.0"
+ "why3=1.4.0" "why3-coq=1.4.0"
+ ];
# only pure nix packages. See mk_deriv below for adding opam2nix packages
mk_buildInputs = { nixPackages ? [] } :
[ pkgs.gnugrep pkgs.gnused pkgs.autoconf pkgs.gnumake pkgs.gcc pkgs.ncurses pkgs.time pkgs.python3 pkgs.perl pkgs.file pkgs.which pkgs.dos2unix] ++ nixPackages;
@@ -362,7 +363,13 @@ pkgs.lib.makeExtensible
sed -i src/plugins/pathcrawler/extern/eclipseCLP/RUNME -e "s/chmod 2755/chmod 755/g"
rm src/plugins/pathcrawler/extern/eclipseCLP/lib/x86_64_linux/dbi_mysql.so
rm src/plugins/pathcrawler/extern/eclipseCLP/lib/x86_64_linux/ic.so
- autoPatchelf src/plugins/pathcrawler
+ rm src/plugins/pathcrawler/extern/eclipseCLP/lib/x86_64_linux/bitmap.so
+ rm -fr src/plugins/pathcrawler/extern/eclipseCLP/lib/i386_linux
+ rm src/plugins/pathcrawler/src/generator/COLIBRI/float_util_sparc_sunos5.so
+ rm src/plugins/pathcrawler/src/generator/COLIBRI/float_util_i386_linux.so.*
+ rm src/plugins/pathcrawler/share/bin/float_util_sparc_sunos5.so
+ find src/plugins/pathcrawler -name '*_i386_*.so' -delete
+ autoPatchelf src/plugins/pathcrawler/
make -j 4
ln -sr src/plugins/pathcrawler/share share/pc
# Setup Why3
diff --git a/nix/frama-ci.nix b/nix/frama-ci.nix
index ba8b10a47d5df6e03700e0cb3fcbaa6516329692..5e6a9b2212dd73d85b3bd49f040b52fc5371992e 100644
--- a/nix/frama-ci.nix
+++ b/nix/frama-ci.nix
@@ -5,8 +5,8 @@ let
src = builtins.fetchGit {
"url" = "https://bobot:${password}@git.frama-c.com/frama-c/Frama-CI.git";
"name" = "Frama-CI";
- "rev" = "4150f5b75b121450aef5687f779ec374ed7f1b92";
- "ref" = "master";
+ "rev" = "bb2c9632abbb651363f2070d1cd89bc25cff5249";
+ "ref" = "fix/interface-files";
};
pkgs = import "${src}/pkgs.nix" {};
in
diff --git a/nix/frama-ci.sh b/nix/frama-ci.sh
index dbbe1bb07e4976298cd85cb0a96675ab78d5ac56..b4deee0abc1543e01c82d3c6c92d9b0045b26d77 100755
--- a/nix/frama-ci.sh
+++ b/nix/frama-ci.sh
@@ -3,10 +3,10 @@
DIR=$(dirname $0)
export FRAMA_CI_NIX=$DIR/frama-ci.nix
-
export FRAMA_CI=$(nix-instantiate --eval -E "((import <nixos-20.03> {}).callPackage $FRAMA_CI_NIX { password = \"$TOKEN_FOR_API\";}).src.outPath")
FRAMA_CI=${FRAMA_CI#\"}
FRAMA_CI=${FRAMA_CI%\"}
+export NIX_PATH="nixpkgs=$(eval echo $(nix-instantiate --eval -E "with import $FRAMA_CI/pkgs-ref.nix; url"))"
$FRAMA_CI/compile.sh $@
diff --git a/share/Makefile.plugin.template b/share/Makefile.plugin.template
index 9e6c6d6848b8318eaaed8535d448e83b4639e89f..ca77423063136672f4335cfd2192a467e2580977 100644
--- a/share/Makefile.plugin.template
+++ b/share/Makefile.plugin.template
@@ -444,7 +444,7 @@ $(NAME_OFLAGS):=$(OFLAGS) $(INCLUDE_FLAGS) $(PLUGIN_OFLAGS)
# DO NOT include the plugin's own directory as search path for compiling
# ml test scripts: they will be loaded in a separate phase, and will only see
# the plugin through its static API
-$(NAME_TEST_BFLAGS):= $(BFLAGS) $(INCLUDE_EXT_FLAGS) $(PLUGIN_BFLAGS)
+$(NAME_TEST_BFLAGS):= $(BFLAGS) -w -70 $(INCLUDE_EXT_FLAGS) $(PLUGIN_BFLAGS)
$(NAME_TEST_OFLAGS):= $(OFLAGS) $(INCLUDE_EXT_FLAGS) $(PLUGIN_OFLAGS)
$(TARGET_BFLAGS):= $(PLUGIN_LINK_BFLAGS)
diff --git a/src/kernel_internals/runtime/boot.mli b/src/kernel_internals/runtime/boot.mli
new file mode 100644
index 0000000000000000000000000000000000000000..98ffe7ef308729877bd4ce7bf50dd0584b275cde
--- /dev/null
+++ b/src/kernel_internals/runtime/boot.mli
@@ -0,0 +1,23 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2021 *)
+(* 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). *)
+(* *)
+(**************************************************************************)
+
+(** Nothing is exported. *)
diff --git a/src/kernel_services/ast_transformations/contract_special_float.mli b/src/kernel_services/ast_transformations/contract_special_float.mli
index cce51dc83ef23f10bb7ed95d5a93dfc632b91896..3dd81628ff8b6e38ce4a1ed45466c725bc8149c7 100644
--- a/src/kernel_services/ast_transformations/contract_special_float.mli
+++ b/src/kernel_services/ast_transformations/contract_special_float.mli
@@ -19,3 +19,5 @@
(* for more details (enclosed in the file licenses/LGPLv2.1). *)
(* *)
(**************************************************************************)
+
+(* No function exported *)
diff --git a/src/kernel_services/plugin_entry_points/dynamic.ml b/src/kernel_services/plugin_entry_points/dynamic.ml
index 4781f03369da26a445965716513b24c46feaf225..6867443c7790a77c9a04964c89b2d25de4663c9f 100644
--- a/src/kernel_services/plugin_entry_points/dynamic.ml
+++ b/src/kernel_services/plugin_entry_points/dynamic.ml
@@ -246,7 +246,7 @@ let load_script base =
else
Format.fprintf fmt "%s -c" Fc_config.ocamlc ;
Format.fprintf fmt
- " -g %s -warn-error a -I %s" Fc_config.ocaml_wflags (Fc_config.libdir :> string) ;
+ " -g %s -w -70 -warn-error a -I %s" Fc_config.ocaml_wflags (Fc_config.libdir :> string) ;
if !Fc_config.is_gui && Fc_config.lablgtk <> "" then
Format.fprintf fmt " -package %s" Fc_config.lablgtk;
List.iter (fun p -> Format.fprintf fmt " -I %s" p) !load_path ;
diff --git a/src/plugins/aorai/aorai_register.ml b/src/plugins/aorai/aorai_register.ml
index 90965ec6c8d0c7b65f453ead13e1aaa07f536169..68f3278e1eaa886e550f67ebc514509576b3d612 100644
--- a/src/plugins/aorai/aorai_register.ml
+++ b/src/plugins/aorai/aorai_register.ml
@@ -29,7 +29,6 @@ open Promelaast
(* [VP] Need to get rid of those global references at some point. *)
let promela_file = ref Filepath.Normalized.empty
let c_file = ref Filepath.Normalized.empty
-let output_c_file = ref Filepath.Normalized.empty
let ltl_tmp_file = ref Filepath.Normalized.empty
let ltl_file = ref Filepath.Normalized.empty
let dot_file = ref Filepath.Normalized.empty
@@ -69,16 +68,6 @@ let convert_ltl_exprs t =
(* Promela file *)
-let syntax_error loc msg =
- Aorai_option.abort
- "File %S, line %d, characters %d-%d:@\nSyntax error: %s"
- (Filepath.Normalized.to_pretty_string
- (Datatype.Filepath.of_string (fst loc).Lexing.pos_fname))
- (fst loc).Lexing.pos_lnum
- ((fst loc).Lexing.pos_cnum - (fst loc).Lexing.pos_bol)
- ((snd loc).Lexing.pos_cnum - (fst loc).Lexing.pos_bol)
- msg
-
(* Performs some checks before calling [open_in f], reporting ["errmsg: <f>"]
in case of error. *)
let check_and_open_in (f : Filepath.Normalized.t) errmsg =
@@ -87,30 +76,11 @@ let check_and_open_in (f : Filepath.Normalized.t) errmsg =
open_in (f :> string)
let ltl_to_ltlLight f_ltl (f_out : Filepath.Normalized.t) =
- try
- let c = check_and_open_in f_ltl "invalid LTL file" in
- let (ltl_form,exprs) = Ltllexer.parse c in
- close_in c;
- Ltl_output.output ltl_form (f_out :> string);
- set_ltl_correspondence exprs
- with
- | Ltllexer.Error (loc,msg) -> syntax_error loc msg
-
-let parse_error' lexbuf msg =
- let open Lexing in
- let start_p = Cil_datatype.Position.of_lexing_pos (lexeme_start_p lexbuf)
- and end_p = Cil_datatype.Position.of_lexing_pos (lexeme_end_p lexbuf)
- and lexeme = Lexing.lexeme lexbuf in
- let start_line = start_p.Filepath.pos_lnum in
- let abort str =
- Aorai_option.feedback ~source:start_p "%s@.%a, before or at token: %s\n%a@."
- str
- Errorloc.pp_location (start_p, end_p)
- lexeme
- (Errorloc.pp_context_from_file ~start_line ~ctx:2) start_p;
- raise (Log.AbortError "aorai")
- in
- Pretty_utils.ksfprintf abort msg
+ let c = check_and_open_in f_ltl "invalid LTL file" in
+ let (ltl_form,exprs) = Ltllexer.parse c in
+ close_in c;
+ Ltl_output.output ltl_form (f_out :> string);
+ set_ltl_correspondence exprs
let load_ya_file filename =
let channel = check_and_open_in filename "invalid Ya file" in
@@ -122,30 +92,21 @@ let load_ya_file filename =
close_in channel;
Data_for_aorai.setAutomata automata
with
- | Parsing.Parse_error | Invalid_argument _ ->
- parse_error' lexbuf "syntax error"
- | Yalexer.Lexing_error msg ->
- parse_error' lexbuf "%s" msg
-
+ | Parsing.Parse_error ->
+ Utils_parser.abort_current lexbuf "syntax error"
let load_promela_file f =
- try
- let c = check_and_open_in f "invalid Promela file" in
- let auto = Promelalexer.parse c in
- let trans = convert_ltl_exprs auto.trans in
- close_in c;
- Data_for_aorai.setAutomata { auto with trans };
- with
- | Promelalexer.Error(loc,msg) -> syntax_error loc msg
+ let c = check_and_open_in f "invalid Promela file" in
+ let auto = Promelalexer.parse c in
+ let trans = convert_ltl_exprs auto.trans in
+ close_in c;
+ Data_for_aorai.setAutomata { auto with trans }
let load_promela_file_withexps f =
- try
- let c = check_and_open_in f "invalid Promela file" in
- let automata = Promelalexer_withexps.parse c in
- close_in c;
- Data_for_aorai.setAutomata automata;
- with
- | Promelalexer_withexps.Error(loc,msg) -> syntax_error loc msg
+ let c = check_and_open_in f "invalid Promela file" in
+ let automata = Promelalexer_withexps.parse c in
+ close_in c;
+ Data_for_aorai.setAutomata automata
let display_status () =
if Aorai_option.verbose_atleast 2 then begin
@@ -266,9 +227,6 @@ let work () =
else
load_promela_file !promela_file;
printverb "Loading promela : done\n";
- (* Computing the list of ignored functions *)
- (* Aorai_visitors.compute_ignored_functions file; *)
-
(* Promelaoutput.print_raw_automata (Data_for_aorai.getAutomata()); *)
(* Data_for_aorai.debug_ltl_expressions (); *)
diff --git a/src/plugins/aorai/aorai_register.mli b/src/plugins/aorai/aorai_register.mli
new file mode 100644
index 0000000000000000000000000000000000000000..ff43ae4b1cfab696df46d3ae7e3f8e19f4710a45
--- /dev/null
+++ b/src/plugins/aorai/aorai_register.mli
@@ -0,0 +1,26 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Aorai plug-in of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2021 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* INRIA (Institut National de Recherche en Informatique et en *)
+(* Automatique) *)
+(* INSA (Institut National des Sciences Appliquees) *)
+(* *)
+(* 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). *)
+(* *)
+(**************************************************************************)
+
+(** Register the plugin in the Frama-C kernel. Nothing is exported. *)
diff --git a/src/plugins/aorai/aorai_visitors.ml b/src/plugins/aorai/aorai_visitors.ml
index 93889b764fe0adc88286eb2ee0cb9cc4757fe69f..22172b8226905770639e4a061c806538c283c7cd 100644
--- a/src/plugins/aorai/aorai_visitors.ml
+++ b/src/plugins/aorai/aorai_visitors.ml
@@ -41,14 +41,6 @@ let get_acceptance_pred () =
| Bool3.False | Bool3.Undefined -> acc)
Logic_const.pfalse st
-let get_call_name exp = match exp.enode with
- | Const(CStr(s)) -> s
- | Lval(Var(vi),NoOffset) -> vi.vname
- | _ ->
- Aorai_option.not_yet_implemented
- ~source:(fst exp.eloc)
- "At this time, only explicit calls are allowed by the Aorai plugin."
-
(****************************************************************************)
(* The instrumentation is done in two passes:
diff --git a/src/plugins/aorai/aorai_visitors.mli b/src/plugins/aorai/aorai_visitors.mli
new file mode 100644
index 0000000000000000000000000000000000000000..93ec57c67d4e2c5a5b47205c2add3bdea562c2e2
--- /dev/null
+++ b/src/plugins/aorai/aorai_visitors.mli
@@ -0,0 +1,58 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Aorai plug-in of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2021 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* INRIA (Institut National de Recherche en Informatique et en *)
+(* Automatique) *)
+(* INSA (Institut National des Sciences Appliquees) *)
+(* *)
+(* 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). *)
+(* *)
+(**************************************************************************)
+
+(** visitors performing the instrumentation *)
+
+module Aux_funcs: sig
+ (** the various kinds of auxiliary functions. *)
+ type kind =
+ | Not_aux_func (** original C function. *)
+ | Aux of Cil_types.kernel_function
+ (** Checks whether we are in the corresponding behavior
+ of the function. *)
+ | Pre of Cil_types.kernel_function
+ (** [Pre_func f] denotes a function updating the automaton
+ when [f] is called. *)
+ | Post of Cil_types.kernel_function
+ (** [Post_func f] denotes a function updating the automaton
+ when returning from [f]. *)
+
+ val iter: (Cil_types.varinfo -> kind -> unit) -> unit
+ (** [iter f] calls [f] on all functions registered so far by
+ {!add_sync_with_buch}
+ *)
+
+end
+
+(** generate prototypes for auxiliary functions. *)
+val add_sync_with_buch: Cil_types.file -> unit
+
+(**
+ [add_pre_post_from_buch ast treatloop]
+ provide contracts and/or bodies for auxiliary function
+ (once they have been generated). If [treatloop] is [true],
+ loop invariants are also generated.
+*)
+val add_pre_post_from_buch: Cil_types.file -> bool -> unit
diff --git a/src/plugins/aorai/ltllexer.mli b/src/plugins/aorai/ltllexer.mli
new file mode 100644
index 0000000000000000000000000000000000000000..ac6e7712ddae9d5ac1c6d4a17fcd00f8690fc712
--- /dev/null
+++ b/src/plugins/aorai/ltllexer.mli
@@ -0,0 +1,31 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Aorai plug-in of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2021 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* INRIA (Institut National de Recherche en Informatique et en *)
+(* Automatique) *)
+(* INSA (Institut National des Sciences Appliquees) *)
+(* *)
+(* 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). *)
+(* *)
+(**************************************************************************)
+
+val parse:
+ in_channel ->
+ Ltlast.formula *
+ (string,
+ (Logic_ptree.relation * Promelaast.expression * Promelaast.expression))
+ Hashtbl.t
diff --git a/src/plugins/aorai/ltllexer.mll b/src/plugins/aorai/ltllexer.mll
index a217fb37e852c6fdb6ba58b234f5894b0929a7fc..9e9e3b0300519269d8aaff4c55f23faa5c013b1a 100644
--- a/src/plugins/aorai/ltllexer.mll
+++ b/src/plugins/aorai/ltllexer.mll
@@ -28,47 +28,10 @@
(* from http://www.ltl2dstar.de/down/ltl2dstar-0.4.2.zip *)
{
-
- open Ltlparser
- open Lexing
-
- let loc lexbuf = (lexeme_start_p lexbuf, lexeme_end_p lexbuf)
-
- (*let lex_error lexbuf s = ()*)
- (* Creport.raise_located (loc lexbuf) (AnyMessage ("lexical error: " ^ s))
- *)
-
- let buf = Buffer.create 1024
-
- let newline lexbuf =
- let pos = lexbuf.lex_curr_p in
- lexbuf.lex_curr_p <-
- { pos with pos_lnum = pos.pos_lnum + 1; pos_bol = pos.pos_cnum }
-
- (* Update the current location with file name and line number. *)
-
-(* let update_loc lexbuf file line absolute chars =
- let pos = lexbuf.lex_curr_p in
- let new_file = match file with
- | None -> pos.pos_fname
- | Some s -> s
- in
- lexbuf.lex_curr_p <-
- { pos with
- pos_fname = new_file;
- pos_lnum = if absolute then line else pos.pos_lnum + line;
- pos_bol = pos.pos_cnum - chars;
- }
-*)
- exception Error of (Lexing.position * Lexing.position) * string
-
- let raise_located loc e = raise (Error (loc, e))
-
+open Ltlparser
+open Lexing
}
-
-
-
let rD = ['0'-'9']
let rL = ['a'-'z' 'A'-'Z' '_']
@@ -119,11 +82,11 @@ rule token = parse
(* Comments *)
| "/*" { comment lexbuf; token lexbuf }
- | "//" [^ '\n']* '\n' { newline lexbuf; token lexbuf }
+ | "//" [^ '\n']* '\n' { Utils_parser.newline lexbuf; token lexbuf }
(* Spaces *)
| [' ' '\t' '\012' '\r']+ { token lexbuf }
- | '\n' { newline lexbuf; token lexbuf }
+ | '\n' { Utils_parser.newline lexbuf; token lexbuf }
(* Variables and constants *)
| rD+ | '-' rD+ { LTL_INT (lexeme lexbuf) }
@@ -131,15 +94,12 @@ rule token = parse
(* Others *)
| eof { EOF }
- | _ {
- raise_located (loc lexbuf)
- (Format.sprintf "Illegal_character %s\n" (lexeme lexbuf))
- }
+ | _ { Utils_parser.unknown_token lexbuf }
and comment = parse
| "*/" { () }
- | eof { raise_located (loc lexbuf) "Unterminated_comment\n" }
- | '\n' { newline lexbuf; comment lexbuf }
+ | eof { Utils_parser.abort_current lexbuf "Unterminated_comment" }
+ | '\n' { Utils_parser.newline lexbuf; comment lexbuf }
| _ { comment lexbuf }
@@ -149,6 +109,5 @@ and comment = parse
try
Ltlparser.ltl token lb
with
- Parsing.Parse_error
- | Invalid_argument _ -> raise_located (loc lb) "Syntax error"
+ Parsing.Parse_error -> Utils_parser.abort_current lb "Syntax error"
}
diff --git a/src/plugins/aorai/path_analysis.ml b/src/plugins/aorai/path_analysis.ml
index 0ce2ab315a4b9f0f878e5528343fa7f60edfc266..36c9ef735b4e94195ba1049f8a2785c69dc633b2 100644
--- a/src/plugins/aorai/path_analysis.ml
+++ b/src/plugins/aorai/path_analysis.ml
@@ -24,56 +24,6 @@
(**************************************************************************)
open Promelaast
-(*open Graph.Pack.Digraph
-
- let st_array = ref (Array.make 1 (V.create 0)) ;;
-
- let auto2digraph (stl,trl) =
- Aorai_option.feedback "auto2digraph:" ;
- let digraph = create () in
- st_array:= Array.make (List.length stl) (V.create 0);
- Aorai_option.feedback " array : ok\n" ;
-
- let _ = List.iter
- (fun st ->
- (!st_array).(st.nums)<-(V.create st.nums);
- add_vertex digraph (!st_array).(st.nums)
- )
- stl
- in
- Aorai_option.feedback " array remplissage : ok\n" ;
- List.iter
- (fun tr -> add_edge digraph (V.create tr.start.nums) (V.create tr.stop.nums))
- trl;
- digraph
- ;;
-
-
- let existing_path auto st1 st2 =
- Aorai_option.feedback "existing path ..\n" ;
- let digraph = auto2digraph auto in
- let start = (!st_array).(st1.nums) in
- let stop = (!st_array).(st2.nums) in
- Aorai_option.feedback "%s" ("test : Etats choisis ("^(string_of_int (V.label start))^","^(string_of_int (V.label stop))^")\n") ;
-
- display_with_gv digraph;
- Aorai_option.feedback " affichage : ok\n" ;
- Aorai_option.feedback "shortest path : " ;
-
- let path=shortest_path digraph start stop in
- Aorai_option.feedback "done.\n" ;
- path
- ;;
-
- let test (stl,trl) =
- let st2 = List.hd stl in
- let st1 = List.hd (List.tl stl) in
-
- let _ = existing_path (stl,trl) st1 st2 in
- Aorai_option.feedback "Fini.\n" ;
- ()
- ;;
-*)
let voisins (_,trans_l) st =
List.fold_left
@@ -123,27 +73,6 @@ let dijkstra (adj: 'a -> ('a * int) list) (v1:'a) (v2:'a) =
in
loop (add (0,(v1,[])) (empty()))
-
-
-
-let existing_path (stl,_ as auto) stn1 stn2 =
- let st1 = ref (List.hd stl) in
- let st2 = ref (List.hd stl) in
- List.iter
- (fun st ->
- if st.nums=stn1 then st1:=st;
- if st.nums=stn2 then st2:=st;
- )
- stl;
-
- try
- let _ = dijkstra (voisins auto) !st1 !st2 in
- true
- with
- | Not_found -> false
-;;
-
-
(** since Nitrogen-20111001 *)
let get_transitions_of_state st (_,tr) =
List.fold_left
@@ -151,12 +80,6 @@ let get_transitions_of_state st (_,tr) =
if tr.start.nums = st.nums then tr::acc else acc)
[] tr
-let get_transitions_to_state st (_,tr) =
- List.fold_left
- (fun acc tr ->
- if tr.stop.nums = st.nums then tr::acc else acc)
- [] tr
-
let get_edges st1 st2 (_,tr) =
List.find_all
(fun tr -> tr.start.nums = st1.nums && tr.stop.nums = st2.nums)
@@ -181,16 +104,6 @@ let at_most_one_path (states,transitions as auto) st1 st2 =
false
with Not_found -> true
-let test (stl,_ as auto) =
- let st2 = List.hd stl in
- let st1 = List.hd (List.tl stl) in
- Aorai_option.feedback "test : Etats choisis (%d,%d)" st1.nums st2.nums;
- let (res,_) = dijkstra (voisins auto) st1 st2 in
- Aorai_option.feedback "Fini.@\n%a"
- (Pretty_utils.pp_list ~pre:"@[[" ~sep:",@ " ~suf:"@]]"
- (fun fmt st -> Format.fprintf fmt "%d" st.nums))
- res
-
(*
Local Variables:
compile-command: "make -C ../../.."
diff --git a/src/plugins/aorai/path_analysis.mli b/src/plugins/aorai/path_analysis.mli
new file mode 100644
index 0000000000000000000000000000000000000000..b30f709bfc26c4f3be78a1089e99fd734a0f25cb
--- /dev/null
+++ b/src/plugins/aorai/path_analysis.mli
@@ -0,0 +1,40 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Aorai plug-in of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2021 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* INRIA (Institut National de Recherche en Informatique et en *)
+(* Automatique) *)
+(* INSA (Institut National des Sciences Appliquees) *)
+(* *)
+(* 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). *)
+(* *)
+(**************************************************************************)
+
+(** [get_edges s1 s2 g] retrieves all edges in [g] between [s1] and [s2]. *)
+val get_edges:
+ Promelaast.state -> Promelaast.state -> ('c,'a) Promelaast.graph
+ -> ('c, 'a) Promelaast.trans list
+
+(** retrieve all edges starting at the given node. *)
+val get_transitions_of_state:
+ Promelaast.state -> ('c,'a) Promelaast.graph -> ('c,'a) Promelaast.trans list
+
+(** return the initial states of the graph. *)
+val get_init_states: ('c, 'a) Promelaast.graph -> Promelaast.state list
+
+(** [true] iff there's at most one path between the two states in the graph. *)
+val at_most_one_path:
+ ('c, 'a) Promelaast.graph -> Promelaast.state -> Promelaast.state -> bool
diff --git a/src/plugins/aorai/promelaast.mli b/src/plugins/aorai/promelaast.mli
index c2f539897fc53abb025862cffc9d21f94a266fb5..133d1426600fc61efc83115616b40d9af9e49f91 100644
--- a/src/plugins/aorai/promelaast.mli
+++ b/src/plugins/aorai/promelaast.mli
@@ -132,6 +132,8 @@ type ('c,'a) trans = {
mutable numt : int (** Numerical ID of the transition *)
}
+type ('c,'a) graph = state list * ('c, 'a) trans list
+
type parsed_trans = (guard, action) trans
type typed_trans = (typed_condition, typed_action) trans
@@ -140,7 +142,7 @@ type typed_trans = (typed_condition, typed_action) trans
of transitions.*)
type ('c,'a) automaton = {
states: state list;
- trans: (('c,'a) trans) list;
+ trans: ('c,'a) trans list;
metavariables: Cil_types.varinfo Datatype.String.Map.t;
observables: Datatype.String.Set.t option;
}
diff --git a/src/plugins/aorai/promelalexer.mli b/src/plugins/aorai/promelalexer.mli
new file mode 100644
index 0000000000000000000000000000000000000000..c782e5202006897b65bb3576fa13d3bbf8646c54
--- /dev/null
+++ b/src/plugins/aorai/promelalexer.mli
@@ -0,0 +1,26 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Aorai plug-in of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2021 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* INRIA (Institut National de Recherche en Informatique et en *)
+(* Automatique) *)
+(* INSA (Institut National des Sciences Appliquees) *)
+(* *)
+(* 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). *)
+(* *)
+(**************************************************************************)
+
+val parse: in_channel -> Promelaast.parsed_automaton
diff --git a/src/plugins/aorai/promelalexer.mll b/src/plugins/aorai/promelalexer.mll
index 633d018dd49e2df4493dca2f1d0538433a2e1343..58b8d173faa6c8361c060ff631735597a408bcc9 100644
--- a/src/plugins/aorai/promelalexer.mll
+++ b/src/plugins/aorai/promelalexer.mll
@@ -30,19 +30,6 @@
{
open Promelaparser
open Lexing
-
- exception Error of (Lexing.position * Lexing.position) * string
-
- let loc lexbuf = (lexeme_start_p lexbuf, lexeme_end_p lexbuf)
-
- let raise_located loc e = raise (Error (loc, e))
-
- let buf = Buffer.create 1024
-
- let newline lexbuf =
- let pos = lexbuf.lex_curr_p in
- lexbuf.lex_curr_p <-
- { pos with pos_lnum = pos.pos_lnum + 1; pos_bol = pos.pos_cnum }
}
let rD = ['0'-'9']
@@ -69,9 +56,9 @@ rule token = parse
| "&&" { PROMELA_AND }
| '!' { PROMELA_NOT }
| [' ' '\t' '\012' '\r']+ { token lexbuf }
- | '\n' { newline lexbuf; token lexbuf }
+ | '\n' { Utils_parser.newline lexbuf; token lexbuf }
| "/*" { comment lexbuf; token lexbuf }
- | "//" [^ '\n']* '\n' { newline lexbuf; token lexbuf }
+ | "//" [^ '\n']* '\n' { Utils_parser.newline lexbuf; token lexbuf }
| "callof_" rL* (rL | rD)*
{ let s=(lexeme lexbuf) in
@@ -86,53 +73,30 @@ rule token = parse
let s=String.sub s 15 ((String.length s)-15) in
PROMELA_CALLORRETURNOF s }
+ | "callof_" { Utils_parser.abort_current lexbuf
+ "Illegal function name in Promela file." }
+ | "returnof_" { Utils_parser.abort_current lexbuf
+ "Illegal function name in Promela file." }
+ | "callorreturnof_" { Utils_parser.abort_current lexbuf
+ "Illegal function name in Promela file." }
- | "callof_" { raise_located (loc lexbuf) "Illegal function name in Promela file." }
- | "returnof_" { raise_located (loc lexbuf) "Illegal function name in Promela file." }
- | "callorreturnof_" { raise_located (loc lexbuf) "Illegal function name in Promela file." }
-
-
-
- | rL (rL | rD)* { let s = lexeme lexbuf in
- PROMELA_LABEL s }
+ | rL (rL | rD)* { let s = lexeme lexbuf in PROMELA_LABEL s }
| eof { EOF }
| "1" { PROMELA_TRUE }
- | _ { Aorai_option.error "Illegal_character : '%s'\n" (lexeme lexbuf);
- raise Parsing.Parse_error}
-
-
-
+ | _ { Utils_parser.unknown_token lexbuf }
and comment = parse
| "*/" { () }
- | eof { Aorai_option.error "Unterminated_comment\n" (*lex_error lexbuf "Unterminated_comment"*) }
- | '\n' { newline lexbuf; comment lexbuf }
+ | eof { Aorai_option.abort "Unterminated_comment\n" }
+ | '\n' { Utils_parser.newline lexbuf; comment lexbuf }
| _ { comment lexbuf }
-
{
let parse c =
let lb = from_channel c in
try
Promelaparser.promela token lb
with
- Parsing.Parse_error
- | Invalid_argument _ ->
- let (a,b)=(loc lb) in
- Aorai_option.error "Syntax error (l%d c%d -> l%dc%d)" a.pos_lnum (a.pos_cnum-a.pos_bol) b.pos_lnum (b.pos_cnum-b.pos_bol);
-(* Format.print_string "Syntax error (" ; *)
-(* Format.print_string "l" ; *)
-(* Format.print_int a.pos_lnum ; *)
-(* Format.print_string "c" ; *)
-(* Format.print_int (a.pos_cnum-a.pos_bol) ;*)
-(* Format.print_string " -> l" ; *)
-(* Format.print_int b.pos_lnum ; *)
-(* Format.print_string "c" ; *)
-(* Format.print_int (b.pos_cnum-b.pos_bol) ;*)
-(* Format.print_string ")\n" ; *)
- raise_located (loc lb) "Syntax error"
-
-
-
+ | Parsing.Parse_error -> Utils_parser.abort_current lb "Syntax error"
}
diff --git a/src/plugins/aorai/promelalexer_withexps.mli b/src/plugins/aorai/promelalexer_withexps.mli
new file mode 100644
index 0000000000000000000000000000000000000000..c782e5202006897b65bb3576fa13d3bbf8646c54
--- /dev/null
+++ b/src/plugins/aorai/promelalexer_withexps.mli
@@ -0,0 +1,26 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Aorai plug-in of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2021 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* INRIA (Institut National de Recherche en Informatique et en *)
+(* Automatique) *)
+(* INSA (Institut National des Sciences Appliquees) *)
+(* *)
+(* 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). *)
+(* *)
+(**************************************************************************)
+
+val parse: in_channel -> Promelaast.parsed_automaton
diff --git a/src/plugins/aorai/promelalexer_withexps.mll b/src/plugins/aorai/promelalexer_withexps.mll
index 60a6eccee52b014b09a146a7fcc597f2620d66d3..178a70ef49108a10aa22858b6682a47d4a1ab019 100644
--- a/src/plugins/aorai/promelalexer_withexps.mll
+++ b/src/plugins/aorai/promelalexer_withexps.mll
@@ -31,19 +31,6 @@
open Promelaparser_withexps
open Lexing
- exception Error of (Lexing.position * Lexing.position) * string
-
- let loc lexbuf = (lexeme_start_p lexbuf, lexeme_end_p lexbuf)
-
- let raise_located loc e = raise (Error (loc, e))
-
- let buf = Buffer.create 1024
-
- let newline lexbuf =
- let pos = lexbuf.lex_curr_p in
- lexbuf.lex_curr_p <-
- { pos with pos_lnum = pos.pos_lnum + 1; pos_bol = pos.pos_cnum }
-
}
@@ -74,9 +61,9 @@ rule token = parse
| "&&" { PROMELA_AND }
| '!' { PROMELA_NOT }
| [' ' '\t' '\012' '\r']+ { token lexbuf }
- | '\n' { newline lexbuf; token lexbuf }
+ | '\n' { Utils_parser.newline lexbuf; token lexbuf }
| "/*" { comment lexbuf; token lexbuf }
- | "//" [^ '\n']* '\n' { newline lexbuf; token lexbuf }
+ | "//" [^ '\n']* '\n' { Utils_parser.newline lexbuf; token lexbuf }
| "callof_" rL* (rL | rD)*
{ let s=(lexeme lexbuf) in
@@ -92,9 +79,12 @@ rule token = parse
PROMELA_CALLORRETURNOF s }
- | "callof_" { raise_located (loc lexbuf) "Illegal function name in Promela file." }
- | "returnof_" { raise_located (loc lexbuf) "Illegal function name in Promela file." }
- | "callorreturnof_" { raise_located (loc lexbuf) "Illegal function name in Promela file." }
+ | "callof_" { Utils_parser.abort_current lexbuf
+ "Illegal function name in Promela file." }
+ | "returnof_" { Utils_parser.abort_current lexbuf
+ "Illegal function name in Promela file." }
+ | "callorreturnof_" { Utils_parser.abort_current lexbuf
+ "Illegal function name in Promela file." }
| rD+ | '-' rD+ { PROMELA_INT (lexeme lexbuf) }
@@ -130,16 +120,12 @@ rule token = parse
| eof { EOF }
| "1" { PROMELA_TRUE }
- | _ { Aorai_option.error "Illegal_character : '%s'\n" (lexeme lexbuf);
- raise Parsing.Parse_error}
-
-
-
+ | _ { Utils_parser.unknown_token lexbuf }
and comment = parse
| "*/" { () }
- | eof { Aorai_option.warning "Unterminated_comment\n" (*lex_error lexbuf "Unterminated_comment"*) }
- | '\n' { newline lexbuf; comment lexbuf }
+ | eof { Aorai_option.abort "Unterminated_comment\n" }
+ | '\n' { Utils_parser.newline lexbuf; comment lexbuf }
| _ { comment lexbuf }
@@ -149,22 +135,5 @@ and comment = parse
try
Promelaparser_withexps.promela token lb
with
- Parsing.Parse_error
- | Invalid_argument _ ->
- let (a,b)=(loc lb) in
- Aorai_option.error "Syntax error (l%d c%d -> l%dc%d)" a.pos_lnum (a.pos_cnum-a.pos_bol) b.pos_lnum (b.pos_cnum-b.pos_bol);
-(* Format.print_string "Syntax error (" ; *)
-(* Format.print_string "l" ; *)
-(* Format.print_int a.pos_lnum ; *)
-(* Format.print_string "c" ; *)
-(* Format.print_int (a.pos_cnum-a.pos_bol) ;*)
-(* Format.print_string " -> l" ; *)
-(* Format.print_int b.pos_lnum ; *)
-(* Format.print_string "c" ; *)
-(* Format.print_int (b.pos_cnum-b.pos_bol) ;*)
-(* Format.print_string ")\n" ; *)
- raise_located (loc lb) "Syntax error"
-
-
-
+ Parsing.Parse_error -> Utils_parser.abort_current lb "Syntax error"
}
diff --git a/src/plugins/aorai/tests/Aorai_test.mli b/src/plugins/aorai/tests/Aorai_test.mli
new file mode 100644
index 0000000000000000000000000000000000000000..93dd0917c8512b2e33b4b288d70faf3435badb4a
--- /dev/null
+++ b/src/plugins/aorai/tests/Aorai_test.mli
@@ -0,0 +1 @@
+(* Nothing is exported. *)
diff --git a/src/plugins/aorai/tests/ya/name_projects.mli b/src/plugins/aorai/tests/ya/name_projects.mli
new file mode 100644
index 0000000000000000000000000000000000000000..257f4adfc7668a67011f2f6a5043a211ae5b882a
--- /dev/null
+++ b/src/plugins/aorai/tests/ya/name_projects.mli
@@ -0,0 +1 @@
+(* nothing is exported. *)
diff --git a/src/plugins/aorai/utils_parser.ml b/src/plugins/aorai/utils_parser.ml
index 819ae335d6fa9032c9d849097025b71066c5025f..87b196e921f3af940d818b60c191f789d62e6e51 100644
--- a/src/plugins/aorai/utils_parser.ml
+++ b/src/plugins/aorai/utils_parser.ml
@@ -23,60 +23,23 @@
(* *)
(**************************************************************************)
-let rec get_last_field my_field my_offset =
- match my_offset with
- | Cil_types.NoOffset -> my_field
- | Cil_types.Field(fieldinfo,the_offset) -> get_last_field fieldinfo the_offset
- | _ -> Aorai_option.fatal "NOT YET IMPLEMENTED : struct with array access."
-
-
-let rec add_offset father_offset new_offset =
- match father_offset with
- | Cil_types.NoOffset -> new_offset
- | Cil_types.Field(_,the_offset) -> (Cil.addOffset father_offset (add_offset the_offset new_offset))
- | _ -> Aorai_option.fatal "NOT YET IMPLEMENTED : struct with array access."
-
-
-
-let rec get_field_info_from_name my_list name =
- if(List.length my_list <> 0) then begin
- let my_field = List.hd my_list in
- if(my_field.Cil_types.fname = name) then my_field
- else get_field_info_from_name (List.tl my_list) name
- end
- else Aorai_option.fatal "no field found with name :%s" name
-
-
-
-let get_new_offset my_host my_offset name=
- match my_host with
- | Cil_types.Var(var) ->
- let var_info = var in
- (* if my_offset is null no need to search the last field *)
- (* else we need to have the last *)
-
- let my_comp =
- if (my_offset = Cil_types.NoOffset) then
- match var_info.Cil_types.vtype with
- | Cil_types.TComp(mc,_,_) -> mc
- | _ -> assert false
- (*Cil_types.TComp(my_comp,_,_) = var_info.Cil_types.vtype in*)
-
- else begin
- let get_field_from_offset my_offset = begin
- match my_offset with
- | Cil_types.Field(fieldinfo,_) -> fieldinfo
- | _ -> Aorai_option.fatal "support only struct no array with struct"
- end in
- let field_info = get_field_from_offset my_offset in
- let last_field_offset = get_last_field field_info my_offset in
- (* last field in offset but not the field we want, for that we search in*)
- let mc = last_field_offset.Cil_types.fcomp in
- mc
- end
- in
- let cfields = Option.value ~default:[] my_comp.Cil_types.cfields in
- let field_info = get_field_info_from_name cfields name in
- Cil_types.Field(field_info,Cil_types.NoOffset)
-
- | _ -> Aorai_option.fatal "NOT YET IMPLEMENTED : mem is not supported"
+open Lexing
+
+let current_loc lex = Cil_datatype.Position.of_lexing_pos (lexeme_start_p lex)
+
+let abort_current lex fmt =
+ let source = current_loc lex in
+ let start_line = source.Filepath.pos_lnum in
+ let fmt = "before or at token %s@\n%a@\n" ^^ fmt in
+ Aorai_option.abort ~source fmt
+ (Lexing.lexeme lex)
+ (Errorloc.pp_context_from_file ~start_line ~ctx:2) source
+
+let unknown_token lex =
+ abort_current lex
+ "Unexpected character: '%c'" (lexeme_char lex (lexeme_start lex))
+
+let newline lexbuf =
+ let pos = lexbuf.lex_curr_p in
+ lexbuf.lex_curr_p <-
+ { pos with pos_lnum = pos.pos_lnum + 1; pos_bol = pos.pos_cnum }
diff --git a/src/plugins/aorai/utils_parser.mli b/src/plugins/aorai/utils_parser.mli
new file mode 100644
index 0000000000000000000000000000000000000000..e62bd1736e4bbb97ea3952358a872fa43bfb460c
--- /dev/null
+++ b/src/plugins/aorai/utils_parser.mli
@@ -0,0 +1,41 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Aorai plug-in of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2021 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* INRIA (Institut National de Recherche en Informatique et en *)
+(* Automatique) *)
+(* INSA (Institut National des Sciences Appliquees) *)
+(* *)
+(* 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). *)
+(* *)
+(**************************************************************************)
+
+(** utilities for parsing automata and LTL formulas *)
+
+(** returns the position corresponding to the
+ current character in the lexbuf. *)
+val current_loc: Lexing.lexbuf -> Cil_datatype.Position.t
+
+(** aborts the execution using current lexbuf position as source. *)
+val abort_current:
+ Lexing.lexbuf -> ('a, Format.formatter, unit, 'b) format4 -> 'a
+
+(** aborts in case the current character
+ is not the beginning of a valid token. *)
+val unknown_token: Lexing.lexbuf -> 'a
+
+(** initiate a new line in the lexbuf *)
+val newline: Lexing.lexbuf -> unit
diff --git a/src/plugins/aorai/yalexer.mli b/src/plugins/aorai/yalexer.mli
new file mode 100644
index 0000000000000000000000000000000000000000..f587f3928a3ee577fb15f500d5f5478bf6f9a6c6
--- /dev/null
+++ b/src/plugins/aorai/yalexer.mli
@@ -0,0 +1,26 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Aorai plug-in of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2021 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* INRIA (Institut National de Recherche en Informatique et en *)
+(* Automatique) *)
+(* INSA (Institut National des Sciences Appliquees) *)
+(* *)
+(* 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). *)
+(* *)
+(**************************************************************************)
+
+val token: Lexing.lexbuf -> Yaparser.token
diff --git a/src/plugins/aorai/yalexer.mll b/src/plugins/aorai/yalexer.mll
index b99f7b4a8320ec9c9c52bd1c2f3120c496a7c429..4ba7d63d681cc9de3a31ffb9fd92f213870ad444 100644
--- a/src/plugins/aorai/yalexer.mll
+++ b/src/plugins/aorai/yalexer.mll
@@ -26,14 +26,6 @@
(* File yalexer.mll *)
{
open Yaparser
- open Lexing
- exception Lexing_error of string
-
- let new_line lexbuf =
- let lcp = lexbuf.lex_curr_p in
- lexbuf.lex_curr_p <- { lcp with pos_lnum = lcp.pos_lnum + 1;
- pos_bol = lcp.pos_cnum; }
- ;;
}
let num = ['0'-'9']
@@ -44,7 +36,7 @@ let string = ([^ '"' '\\']|'\\'_)*
rule token = parse
[' ' '\t' ] { token lexbuf } (* skip blanks *)
- | '\n' { new_line lexbuf; token lexbuf }
+ | '\n' { Utils_parser.newline lexbuf; token lexbuf }
| ['0'-'9']+ as lxm { INT(lxm) }
| "CALL" { CALL_OF }
| "RETURN" { RETURN_OF }
@@ -89,6 +81,4 @@ rule token = parse
| '?' { QUESTION }
| eof { EOF }
| ":=" { AFF }
- | _ {
- raise (Lexing_error ("unexpected character '" ^ Lexing.lexeme lexbuf ^ "'"))
- }
+ | _ { Utils_parser.unknown_token lexbuf }
diff --git a/src/plugins/callgraph/register.mli b/src/plugins/callgraph/register.mli
new file mode 100644
index 0000000000000000000000000000000000000000..bf4d38e09ce8cf89921a5f88d286a79b1a6854d7
--- /dev/null
+++ b/src/plugins/callgraph/register.mli
@@ -0,0 +1,23 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2021 *)
+(* 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). *)
+(* *)
+(**************************************************************************)
+
+(** Register the plugin in the Frama-C kernel. Nothing is exported. *)
diff --git a/src/plugins/dive/main.mli b/src/plugins/dive/main.mli
new file mode 100644
index 0000000000000000000000000000000000000000..bf4d38e09ce8cf89921a5f88d286a79b1a6854d7
--- /dev/null
+++ b/src/plugins/dive/main.mli
@@ -0,0 +1,23 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2021 *)
+(* 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). *)
+(* *)
+(**************************************************************************)
+
+(** Register the plugin in the Frama-C kernel. Nothing is exported. *)
diff --git a/src/plugins/e-acsl/headers/header_spec.txt b/src/plugins/e-acsl/headers/header_spec.txt
index 3512bc95bbe2867dfea4d72efe1a676078410865..9f014a0a1abe4040f1804d2d5e5caf67ca31ce72 100644
--- a/src/plugins/e-acsl/headers/header_spec.txt
+++ b/src/plugins/e-acsl/headers/header_spec.txt
@@ -151,6 +151,7 @@ src/libraries/varname.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
src/libraries/varname.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL
src/local_config.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL
src/main.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
+src/main.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL
src/options.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
src/options.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL
src/project_initializer/rtl.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
diff --git a/src/plugins/e-acsl/src/main.mli b/src/plugins/e-acsl/src/main.mli
new file mode 100644
index 0000000000000000000000000000000000000000..f3b673478f0ddb74158fdefdf6d2c10a1fedda87
--- /dev/null
+++ b/src/plugins/e-acsl/src/main.mli
@@ -0,0 +1,23 @@
+(**************************************************************************)
+(* *)
+(* This file is part of the Frama-C's E-ACSL plug-in. *)
+(* *)
+(* Copyright (C) 2012-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). *)
+(* *)
+(**************************************************************************)
+
+(** Register the plugin in the Frama-C kernel. Nothing is exported. *)
diff --git a/src/plugins/e-acsl/tests/print.mli b/src/plugins/e-acsl/tests/print.mli
new file mode 100644
index 0000000000000000000000000000000000000000..9e846eed54c8875c271b1dd7eb248405cf485798
--- /dev/null
+++ b/src/plugins/e-acsl/tests/print.mli
@@ -0,0 +1,21 @@
+(**************************************************************************)
+(* *)
+(* This file is part of the Frama-C's E-ACSL plug-in. *)
+(* *)
+(* Copyright (C) 2012-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). *)
+(* *)
+(**************************************************************************)
diff --git a/src/plugins/impact/reason_graph.ml b/src/plugins/impact/reason_graph.ml
index d39473451727bc94dc441974a145042055e1cd37..18f11b72630744f1d1e0a4fed02dc36ffa044c74 100644
--- a/src/plugins/impact/reason_graph.ml
+++ b/src/plugins/impact/reason_graph.ml
@@ -58,8 +58,6 @@ module Reason =
type reason_graph = Reason.Set.t
-(** Map from a node to the kernel_function it belongs to *)
-
type nodes_origin = Cil_types.kernel_function PdgTypes.Node.Map.t
type reason = {
@@ -217,7 +215,7 @@ let print_dot_graph reason =
(Printexc.to_string exn)
(* Very basic textual debugging function *)
-let print_reason reason =
+let _print_reason reason =
let pp_node = !Db.Pdg.pretty_node false in
let pp fmt (nsrc, ndst, reason) =
Format.fprintf fmt "@[<v 2>%a -> %a (%s)@]"
diff --git a/src/plugins/impact/reason_graph.mli b/src/plugins/impact/reason_graph.mli
new file mode 100644
index 0000000000000000000000000000000000000000..a67394404e020c6071b05fb1bd0f4e78262778ff
--- /dev/null
+++ b/src/plugins/impact/reason_graph.mli
@@ -0,0 +1,58 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2021 *)
+(* 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). *)
+(* *)
+(**************************************************************************)
+
+(** Why is a node impacted. The reasons will be given as [n is impacted
+ by the effect of [n'], and the impact is of type reason]. *)
+type reason_type =
+ | Intraprocedural of PdgTypes.Dpd.t
+ (** The effect of [n'] in [f] impact [n], which is also in [f]. *)
+
+ | InterproceduralDownward (** the effect of [n'] in [f] has an effect on a
+ callee [f'] of [f], in which [n] is located. *)
+
+ | InterproceduralUpward (** the effect of [n'] in [f] has an effect on a
+ caller [f'] of [f] (once the call to [f] has ended), [n] being in [f']. *)
+
+module ReasonType: Datatype.S with type t = reason_type
+
+module Reason: Datatype.S_with_collections
+ with type t = PdgTypes.Node.t * PdgTypes.Node.t * reason_type
+
+type reason_graph = Reason.Set.t
+
+(** Map from a node to the kernel_function it belongs to *)
+type nodes_origin = Cil_types.kernel_function PdgTypes.Node.Map.t
+
+type reason = {
+ reason_graph: reason_graph;
+ nodes_origin: nodes_origin;
+ initial_nodes: Pdg_aux.NS.t;
+}
+
+module DatatypeReason: Datatype.S with type t = reason
+
+val empty: reason
+
+val to_dot_formatter:
+ ?in_kf:Cil_types.kernel_function -> reason -> Format.formatter -> unit
+
+val print_dot_graph: reason -> unit
diff --git a/src/plugins/impact/register.mli b/src/plugins/impact/register.mli
new file mode 100644
index 0000000000000000000000000000000000000000..39ee2f2c607d65864cfaaccadb7e8d74f7f6d1c1
--- /dev/null
+++ b/src/plugins/impact/register.mli
@@ -0,0 +1,41 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2021 *)
+(* 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). *)
+(* *)
+(**************************************************************************)
+
+open Cil_types
+
+val compute_pragmas: (unit -> stmt list)
+(** Compute the impact analysis from the impact pragma in the program.
+ Print and slice the results according to the parameters -impact-print
+ and -impact-slice.
+ @return the impacted statements *)
+
+val from_stmt: (stmt -> stmt list)
+(** Compute the impact analysis of the given statement.
+ @return the impacted statements *)
+
+val from_nodes:
+ (kernel_function -> PdgTypes.Node.t list -> PdgTypes.NodeSet.t)
+(** Compute the impact analysis of the given set of PDG nodes,
+ that come from the given function.
+ @return the impacted nodes *)
+
+val slice: stmt list -> Project.t
diff --git a/src/plugins/inout/operational_inputs.ml b/src/plugins/inout/operational_inputs.ml
index 0fae49bb5f3cc278c6e53409e25b12bcce26407a..43736a78c9436ab1209a6d1bd9af3bed5476bfe3 100644
--- a/src/plugins/inout/operational_inputs.ml
+++ b/src/plugins/inout/operational_inputs.ml
@@ -561,6 +561,7 @@ let extract_inout_from_froms froms =
(Zone.join in_return in_), out_
+[@@@ warning "-60"]
module Callwise = struct
let merge_call_in_local_table call local_table v =
@@ -842,7 +843,6 @@ module Externals_With_Formals =
end)
let get_external_with_formals =
Externals_With_Formals.memo (raw_externals ~with_formals:true)
-let compute_external_with_formals kf = ignore (get_external_with_formals kf)
let pretty_operational_inputs_internal fmt kf =
diff --git a/src/plugins/inout/operational_inputs.mli b/src/plugins/inout/operational_inputs.mli
new file mode 100644
index 0000000000000000000000000000000000000000..01c0be4bd4b3557b904d4f29766479fdcba70640
--- /dev/null
+++ b/src/plugins/inout/operational_inputs.mli
@@ -0,0 +1,33 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2021 *)
+(* 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). *)
+(* *)
+(**************************************************************************)
+
+open Cil_types
+
+val get_external: kernel_function -> Inout_type.t
+val get_external_aux: ?stmt:stmt -> kernel_function -> Inout_type.t
+
+val pretty_operational_inputs_internal:
+ Format.formatter -> kernel_function -> unit
+val pretty_operational_inputs_external:
+ Format.formatter -> kernel_function -> unit
+val pretty_operational_inputs_external_with_formals:
+ Format.formatter -> kernel_function -> unit
diff --git a/src/plugins/inout/register.mli b/src/plugins/inout/register.mli
new file mode 100644
index 0000000000000000000000000000000000000000..bf4d38e09ce8cf89921a5f88d286a79b1a6854d7
--- /dev/null
+++ b/src/plugins/inout/register.mli
@@ -0,0 +1,23 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2021 *)
+(* 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). *)
+(* *)
+(**************************************************************************)
+
+(** Register the plugin in the Frama-C kernel. Nothing is exported. *)
diff --git a/src/plugins/instantiate/register.mli b/src/plugins/instantiate/register.mli
new file mode 100644
index 0000000000000000000000000000000000000000..bf4d38e09ce8cf89921a5f88d286a79b1a6854d7
--- /dev/null
+++ b/src/plugins/instantiate/register.mli
@@ -0,0 +1,23 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2021 *)
+(* 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). *)
+(* *)
+(**************************************************************************)
+
+(** Register the plugin in the Frama-C kernel. Nothing is exported. *)
diff --git a/src/plugins/loop_analysis/Makefile.in b/src/plugins/loop_analysis/Makefile.in
index 74a6af00dbb2f68843f0feba4e28737dba0145cc..4cb7ceebdc781357e9221147bad002aae4d4c284 100644
--- a/src/plugins/loop_analysis/Makefile.in
+++ b/src/plugins/loop_analysis/Makefile.in
@@ -31,7 +31,8 @@ PLUGIN_ENABLE:=@ENABLE_LOOP_ANALYSIS@
PLUGIN_DISTRIBUTED:=$(PLUGIN_ENABLE)
PLUGIN_NAME:= LoopAnalysis
-PLUGIN_CMO:= options region_analysis_sig region_analysis region_analysis_stmt loop_analysis register
+PLUGIN_CMO:= options region_analysis region_analysis_stmt loop_analysis register
+PLUGIN_CMI:= region_analysis_sig
PLUGIN_DISTRIB_EXTERNAL:= Makefile.in configure.ac configure test.c test.oracle README.org
PLUGIN_TESTS_DIRS:=loop_analysis
diff --git a/src/plugins/loop_analysis/loop_analysis.ml b/src/plugins/loop_analysis/loop_analysis.ml
index b97bd62b23f89ccc3695b52442ae65d1584996bb..43a3fd5b4913cfa2ccb8e7653694cbabe38e1ed2 100644
--- a/src/plugins/loop_analysis/loop_analysis.ml
+++ b/src/plugins/loop_analysis/loop_analysis.ml
@@ -324,21 +324,21 @@ module Store(* (B:sig *)
let value = (mem,conds) in
let open Cil_types in
let map_on_all_succs (mem,conds) =
- List.map (fun x -> (Region_analysis.Edge(stmt,x),(mem,conds,x))) stmt.succs in
+ List.map (fun x -> (Region_analysis_sig.Edge(stmt,x),(mem,conds,x))) stmt.succs in
match stmt.skind with
| Instr(i) -> map_on_all_succs (do_instr i (mem,conds))
| Return _ ->
- [Region_analysis.Exit stmt, (mem,conds,Cil.dummyStmt)]
+ [Region_analysis_sig.Exit stmt, (mem,conds,Cil.dummyStmt)]
| Loop _ | Goto _ | Break _ | Continue _ | Block _ | UnspecifiedSequence _ ->
map_on_all_succs value
| If _ ->
let result = Dataflows.transfer_if_from_guard do_guard stmt value in
List.map (fun (succ,(mem,cond)) ->
- (Region_analysis.Edge(stmt,succ),(mem,cond,succ))) result
+ (Region_analysis_sig.Edge(stmt,succ),(mem,cond,succ))) result
| Switch _ ->
let result = Dataflows.transfer_switch_from_guard do_guard stmt value in
List.map (fun (succ,(mem,cond)) ->
- (Region_analysis.Edge(stmt,succ),(mem,cond,succ))) result
+ (Region_analysis_sig.Edge(stmt,succ),(mem,cond,succ))) result
| Throw _ | TryCatch _ | TryExcept _ | TryFinally _ ->
Options.abort "unsupported exception-related statement: %a"
Printer.pp_stmt stmt
diff --git a/src/plugins/loop_analysis/region_analysis.ml b/src/plugins/loop_analysis/region_analysis.ml
index c04f9f6ec334804ad68163320611d5063f7fe9d4..2906d0e5fe3eb7d5101891ff8b94b3155d407df3 100644
--- a/src/plugins/loop_analysis/region_analysis.ml
+++ b/src/plugins/loop_analysis/region_analysis.ml
@@ -48,9 +48,7 @@
of Nodes". It is maybe also possible to use the wto ordering of
bourdoncle for this purpose. *)
-include Region_analysis_sig;;
-
-module Make(N:Node):sig
+module Make(N:Region_analysis_sig.Node):sig
(* Function computing from an entry abstract value the "after"
state, which is a map from each outgoing edge to its respective
value. *)
@@ -192,7 +190,7 @@ struct
(* Compute for previous node if result not yet available. *)
and get_edge pred n =
- let edge = Edge(pred, n) in
+ let edge = Region_analysis_sig.Edge(pred, n) in
try N.Edge_Dict.get edge_term edge
with Not_found -> do_node pred; N.Edge_Dict.get edge_term edge
in
@@ -215,7 +213,7 @@ struct
N.Graph.iter_preds header (fun pred ->
if (N.Set.mem pred tset) && (is_back_edge pred header)
then
- let edge = Edge(pred,header) in
+ let edge = Region_analysis_sig.Edge(pred,header) in
let input = N.Edge_Dict.get edge_term edge in
inputs := input::!inputs );
N.join !inputs
diff --git a/src/plugins/loop_analysis/region_analysis.mli b/src/plugins/loop_analysis/region_analysis.mli
index 6b4feeb6c8143b74197eb1da945f934e44d824e9..02a957af9f4d8cce3980f451301b6a7d1c4fdc32 100644
--- a/src/plugins/loop_analysis/region_analysis.mli
+++ b/src/plugins/loop_analysis/region_analysis.mli
@@ -31,9 +31,8 @@
reached.
TODO: The algorithm does not handle non-natural loops for now. *)
-include module type of Region_analysis_sig;;
-module Make(N:Node):sig
+module Make(N:Region_analysis_sig.Node):sig
(* Function computing from an entry abstract value the "after"
state, which is a map from each outgoing edge to its respective
value. *)
diff --git a/src/plugins/loop_analysis/region_analysis_sig.ml b/src/plugins/loop_analysis/region_analysis_sig.mli
similarity index 100%
rename from src/plugins/loop_analysis/region_analysis_sig.ml
rename to src/plugins/loop_analysis/region_analysis_sig.mli
diff --git a/src/plugins/loop_analysis/region_analysis_stmt.ml b/src/plugins/loop_analysis/region_analysis_stmt.ml
index b9db0a8032b4b90af9badd2ef66b37bdefa0131c..dad5e1806545d018aeef682a81724486d3c88b5e 100644
--- a/src/plugins/loop_analysis/region_analysis_stmt.ml
+++ b/src/plugins/loop_analysis/region_analysis_stmt.ml
@@ -20,7 +20,7 @@
(* *)
(**************************************************************************)
-open Region_analysis
+open Region_analysis_sig
module type M = sig
val kf: Kernel_function.t
diff --git a/src/plugins/loop_analysis/region_analysis_stmt.mli b/src/plugins/loop_analysis/region_analysis_stmt.mli
index a52050d3e067bab4e2d7c3e67f51a4dc966371c2..23b37e7dcb3fab00600ecebe707e02dca580c616 100644
--- a/src/plugins/loop_analysis/region_analysis_stmt.mli
+++ b/src/plugins/loop_analysis/region_analysis_stmt.mli
@@ -20,7 +20,7 @@
(* *)
(**************************************************************************)
-open Region_analysis
+open Region_analysis_sig
open Cil_types
module type M = sig
diff --git a/src/plugins/loop_analysis/register.mli b/src/plugins/loop_analysis/register.mli
new file mode 100644
index 0000000000000000000000000000000000000000..bf4d38e09ce8cf89921a5f88d286a79b1a6854d7
--- /dev/null
+++ b/src/plugins/loop_analysis/register.mli
@@ -0,0 +1,23 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2021 *)
+(* 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). *)
+(* *)
+(**************************************************************************)
+
+(** Register the plugin in the Frama-C kernel. Nothing is exported. *)
diff --git a/src/plugins/markdown-report/sarif.ml b/src/plugins/markdown-report/sarif.ml
index 0e9661b4067e3112984257fb2650bf251699171e..7356601de8f7aa70ba9392ed19dec2e94e510658 100644
--- a/src/plugins/markdown-report/sarif.ml
+++ b/src/plugins/markdown-report/sarif.ml
@@ -26,12 +26,19 @@
by default: we must thus silence spurious let rec warning (39). *)
[@@@ warning "-39"]
+type 'a dict = (string * 'a) list
+
module type Json_type = sig
type t
val of_yojson: Yojson.Safe.t -> t Ppx_deriving_yojson_runtime.error_or
val to_yojson: t -> Yojson.Safe.t
end
+module type Json_default = sig
+ include Json_type
+ val default: t
+end
+
module Json_string: Json_type with type t = string =
struct
type t = string
@@ -93,6 +100,8 @@ module ArtifactLocation = struct
uriBaseId: (string [@default ""])
}[@@deriving yojson]
+ type _t = t
+
let create ~uri ?(uriBaseId = "") () = { uri; uriBaseId }
let default = create ~uri:"" ()
@@ -119,6 +128,8 @@ module Properties = struct
additional_properties: Custom_properties.t
}
+ type _t = t
+
let default = { tags = []; additional_properties = [] }
let create additional_properties =
@@ -153,6 +164,8 @@ module Message = struct
properties: (Properties.t [@default Properties.default]);
}[@@deriving yojson]
+ type _t = t
+
let create
?(text="")
?(id="")
@@ -182,6 +195,8 @@ module MultiformatMessageString = struct
properties: (Properties.t [@default Properties.default])
}[@@deriving yojson]
+ type _t = t
+
let create ~text ?(markdown="") ?(properties=Properties.default) () =
{ text; markdown; properties }
@@ -201,6 +216,8 @@ module ArtifactContent = struct
}
[@@deriving yojson]
+ type _t = t
+
let create ?(text="") ?(binary="")
?(rendered=MultiformatMessageString.default)
?(properties=Properties.default) () =
diff --git a/src/plugins/markdown-report/sarif.mli b/src/plugins/markdown-report/sarif.mli
new file mode 100644
index 0000000000000000000000000000000000000000..a81d7188fa851e0daac0a93923e5188bcc9e220e
--- /dev/null
+++ b/src/plugins/markdown-report/sarif.mli
@@ -0,0 +1,1140 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2021 *)
+(* 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). *)
+(* *)
+(**************************************************************************)
+
+(** OCaml representation for the sarif 2.1 schema. *)
+
+module type Json_type = sig
+ type t
+ val of_yojson: Yojson.Safe.t -> t Ppx_deriving_yojson_runtime.error_or
+ val to_yojson: t -> Yojson.Safe.t
+end
+
+module type Json_default = sig
+ include Json_type
+ val default: t
+end
+
+module Json_string: Json_type with type t = string
+
+type 'a dict = (string * 'a) list
+
+module Json_dictionary(J: Json_type):
+ Json_type with type t = J.t dict
+
+module JsonStringDictionary: Json_type with type t = string dict
+
+module Uri: sig
+ include Json_type with type t = private string
+ val sarif_github:t
+end
+
+module Version: sig
+ include Json_type with type t = private string
+ val v2_1_0: t
+end
+
+module ArtifactLocation: sig
+ type t = {
+ uri: string;
+ uriBaseId: string
+ } [@@ deriving of_yojson]
+
+ val create: uri:string -> ?uriBaseId:string -> unit -> t
+
+ val of_loc: Cil_datatype.Location.t -> t
+
+ val default: t
+
+end
+
+module ArtifactLocationDictionary:
+ Json_type with type t = ArtifactLocation.t dict
+
+module Custom_properties: Json_type with type t = Yojson.Safe.t dict
+
+module Properties: sig
+ type tags = string list
+
+ type t = {
+ tags: tags;
+ additional_properties: Custom_properties.t
+ } [@@ deriving of_yojson]
+
+ val create: Custom_properties.t -> t
+
+ val default: t
+
+end
+
+module Message: sig
+ type t = {
+ text: string;
+ id: string;
+ markdown: string;
+ arguments: string list;
+ properties: Properties.t;
+ } [@@deriving of_yojson]
+
+ val create:
+ ?text:string ->
+ ?id: string ->
+ ?markdown: string ->
+ ?arguments: string list ->
+ ?properties: Properties.t ->
+ unit ->
+ t
+
+ val plain_text:
+ text:string -> ?id:string -> ?arguments:string list -> unit -> t
+
+ val markdown:
+ markdown:Markdown.elements ->
+ ?id:string -> ?arguments:string list -> unit -> t
+
+end
+
+module MultiformatMessageString: sig
+ type t = {
+ text: string;
+ markdown: string;
+ properties: Properties.t;
+ } [@@deriving of_yojson]
+
+ val create:
+ text:string -> ?markdown:string -> ?properties:Properties.t -> unit -> t
+
+ val default: t
+
+end
+
+module MultiformatMessageStringDictionary:
+ Json_type with type t = MultiformatMessageString.t dict
+
+module ArtifactContent: sig
+ type t =
+ { text: string;
+ binary: string;
+ rendered: MultiformatMessageString.t;
+ properties: Properties.t;
+ }
+ [@@deriving of_yojson]
+
+ val create:
+ ?text:string -> ?binary:string ->
+ ?rendered:MultiformatMessageString.t ->
+ ?properties:Properties.t -> unit -> t
+
+ val default: t
+end
+
+module Region: sig
+ type t = {
+ startLine: int;
+ startColumn: int;
+ endLine: int;
+ endColumn: int;
+ charOffset: int;
+ charLength: int;
+ byteOffset: int;
+ byteLength: int;
+ snippet: ArtifactContent.t;
+ message: Message.t;
+ }[@@deriving yojson]
+
+ val create:
+ ?startLine:int ->
+ ?startColumn:int ->
+ ?endLine:int ->
+ ?endColumn:int ->
+ ?charOffset:int ->
+ ?charLength:int ->
+ ?byteOffset:int ->
+ ?byteLength: int ->
+ ?snippet: ArtifactContent.t ->
+ ?message: Message.t ->
+ unit -> t
+
+ val default: t
+
+ val of_loc: Cil_datatype.Location.t -> t
+end
+
+module Rectangle: sig
+ type t = {
+ top: float;
+ left: float;
+ bottom: float;
+ right: float;
+ message: Message.t;
+ }
+ [@@deriving yojson]
+end
+
+module PhysicalLocation: sig
+ type t = {
+ id: string;
+ artifactLocation: ArtifactLocation.t;
+ region: Region.t;
+ contextRegion: Region.t;
+ }[@@deriving yojson]
+
+ val create:
+ ?id:string ->
+ artifactLocation: ArtifactLocation.t ->
+ ?region: Region.t ->
+ ?contextRegion: Region.t ->
+ unit -> t
+
+ val default: t
+
+ val of_loc: Cil_datatype.Location.t -> t
+
+end
+
+module Location: sig
+ type t = {
+ physicalLocation: PhysicalLocation.t;
+ fullyQualifiedLogicalName: string;
+ message: Message.t;
+ annotations: Region.t list;
+ properties: Properties.t;
+ }[@@deriving yojson]
+
+ val create:
+ physicalLocation: PhysicalLocation.t ->
+ ?fullyQualifiedLogicalName: string ->
+ ?message: Message.t ->
+ ?annotations: Region.t list ->
+ ?properties: Properties.t ->
+ unit -> t
+
+ val default: t
+
+ val of_loc: Cil_datatype.Location.t -> t
+
+end
+
+module StackFrame: sig
+ type t = {
+ location: Location.t;
+ stack_module: string;
+ threadId: int;
+ address: int;
+ offset: int;
+ parameters: string list;
+ properties: Properties.t;
+ }[@@deriving yojson]
+end
+
+module Stack: sig
+ type t = {
+ message: Message.t;
+ frames: StackFrame.t list;
+ properties: Properties.t;
+ }[@@deriving yojson]
+
+ val default: t
+end
+
+module Additional_properties: Json_default with type t = string dict
+
+module Stl_importance: sig
+ include Json_type with type t = private string
+ val important: t
+ val essential: t
+ val unimportant: t
+end
+
+module ThreadFlowLocation: sig
+ type t = {
+ step: int;
+ location: Location.t;
+ stack: Stack.t;
+ kind: string;
+ tfl_module: string;
+ state: Additional_properties.t;
+ nestingLevel: int;
+ executionOrder: int;
+ timestamp: string;
+ importance: Stl_importance.t;
+ properties: Properties.t;
+ }[@@deriving yojson]
+end
+
+module ThreadFlow: sig
+ type t = {
+ id: string;
+ message: Message.t;
+ locations: ThreadFlowLocation.t list;
+ properties: Properties.t;
+ }[@@deriving yojson]
+end
+
+module Attachment: sig
+ type t = {
+ description: Message.t;
+ artifactLocation: ArtifactLocation.t;
+ regions: Region.t list;
+ rectangles: Rectangle.t list;
+ } [@@deriving yojson]
+end
+
+module CodeFlow: sig
+ type t = {
+ description: Message.t;
+ threadFlows: ThreadFlow.t list;
+ properties: Properties.t;
+ } [@@deriving yojson]
+end
+
+module Sarif_exception: sig
+ type t = {
+ kind: string;
+ message: string;
+ stack: Stack.t;
+ innerExceptions: t list;
+ }[@@deriving yojson]
+
+ val default: t
+
+end
+
+module Notification_kind: sig
+ include Json_type with type t = private string
+ val note: t
+ val warning: t
+ val error: t
+end
+
+module Notification: sig
+ type t = {
+ id: string;
+ ruleId: string;
+ physicalLocation: PhysicalLocation.t;
+ message: Message.t;
+ level: Notification_kind.t;
+ threadId: int;
+ time: string;
+ exn: Sarif_exception.t;
+ properties: Properties.t;
+ }[@@deriving yojson]
+end
+
+module Driver: sig
+ type t = {
+ name: string;
+ fullName: string;
+ version: string;
+ semanticVersion: string;
+ fileVersion: string;
+ downloadUri: string;
+ informationUri: string;
+ sarifLoggerVersion: string;
+ language: string;
+ properties: Properties.t;
+ }[@@deriving yojson]
+
+ val create:
+ name: string ->
+ ?fullName: string ->
+ ?version: string ->
+ ?semanticVersion: string ->
+ ?fileVersion: string ->
+ ?downloadUri: string ->
+ ?informationUri: string ->
+ ?sarifLoggerVersion: string ->
+ ?language: string ->
+ ?properties: Properties.t ->
+ unit -> t
+
+ val default: t
+end
+
+module Tool: sig
+ type t = {
+ driver: Driver.t
+ }[@@deriving yojson]
+
+ val create: Driver.t -> t
+
+ val default: t
+end
+
+module Invocation: sig
+
+ type t = {
+ commandLine: string;
+ arguments: string list;
+ responseFiles: ArtifactLocation.t list;
+ attachments: Attachment.t list;
+ startTime: string;
+ endTime: string;
+ exitCode: int;
+ toolNotifications: Notification.t list;
+ configurationNotifications: Notification.t list;
+ exitCodeDescription: string;
+ exitSignalName: string;
+ exitSignalNumber: int;
+ processStartFailureMessage: string;
+ executionSuccessful: bool;
+ machine: string;
+ account: string;
+ processId: int;
+ executableLocation: ArtifactLocation.t;
+ workingDirectory: ArtifactLocation.t;
+ environmentVariables: Additional_properties.t;
+ stdin: ArtifactLocation.t;
+ stdout: ArtifactLocation.t;
+ stderr: ArtifactLocation.t;
+ stdoutStderr: ArtifactLocation.t;
+ properties: Properties.t;
+ }[@@deriving yojson]
+
+ val create:
+ commandLine: string ->
+ ?arguments: string list ->
+ ?responseFiles: ArtifactLocation.t list ->
+ ?attachments: Attachment.t list ->
+ ?startTime: string ->
+ ?endTime: string ->
+ ?exitCode: int ->
+ ?toolNotifications: Notification.t list ->
+ ?configurationNotifications: Notification.t list ->
+ ?exitCodeDescription: string ->
+ ?exitSignalName: string ->
+ ?exitSignalNumber: int ->
+ ?processStartFailureMessage: string ->
+ ?executionSuccessful: bool ->
+ ?machine: string ->
+ ?account: string ->
+ ?processId: int ->
+ ?executableLocation: ArtifactLocation.t ->
+ ?workingDirectory: ArtifactLocation.t ->
+ ?environmentVariables: Additional_properties.t ->
+ ?stdin: ArtifactLocation.t ->
+ ?stdout: ArtifactLocation.t ->
+ ?stderr: ArtifactLocation.t ->
+ ?stdoutStderr: ArtifactLocation.t ->
+ ?properties: Properties.t ->
+ unit -> t
+
+ val default: t
+
+end
+
+module Conversion: sig
+ type t = {
+ tool: Tool.t;
+ invocation: Invocation.t;
+ analysisToolLogFiles: ArtifactLocation.t;
+ } [@@deriving yojson]
+
+ val default: t
+
+end
+
+module Edge: sig
+ type t = {
+ id: string;
+ label: Message.t;
+ sourceNodeId: string;
+ targetNodeId: string;
+ properties: Properties.t;
+ } [@@deriving yojson]
+end
+
+module Node: sig
+ type t = {
+ id: string;
+ label: string;
+ location: Location.t;
+ children: t list;
+ properties: Properties.t;
+ }[@@deriving yojson]
+end
+
+module Edge_traversal: sig
+ type t = {
+ edgeId: string;
+ message: Message.t;
+ finalState: Additional_properties.t;
+ stepOverEdgeCount: int;
+ properties: Properties.t;
+ }[@@deriving yojson]
+end
+
+module Role: sig
+ include Json_type with type t = private string
+ val analysisTarget: t
+ val attachment: t
+ val responseFile: t
+ val resultFile: t
+ val standardStream: t
+ val traceFile: t
+ val unmodifiedFile: t
+ val modifiedFile: t
+ val addedFile: t
+ val deletedFile:t
+ val renamedFile:t
+ val uncontrolledFile: t
+end
+
+module Hash: sig
+ type t = {
+ value: string;
+ algorithm: string
+ } [@@deriving yojson]
+end
+
+module Graph: sig
+ type t = {
+ id : string;
+ description: Message.t;
+ nodes: Node.t list;
+ edges: Edge.t list;
+ properties: Properties.t;
+ }[@@deriving yojson]
+end
+
+module Graph_dictionary: Json_type with type t = Graph.t dict
+
+module GraphTraversal: sig
+ type t = {
+ graphId: string;
+ description: Message.t;
+ initialState: Additional_properties.t;
+ edgeTraversals: Edge_traversal.t list;
+ properties: Properties.t;
+ }[@@deriving yojson]
+end
+
+module Replacement: sig
+ type t = {
+ deletedRegion: Region.t;
+ insertedContent: ArtifactContent.t;
+ }[@@deriving yojson]
+end
+
+module Artifact: sig
+ type t = {
+ description: Message.t;
+ location: ArtifactLocation.t;
+ parentIndex: int;
+ offset: int;
+ length: int;
+ roles: Role.t list;
+ mimeType: string;
+ contents: ArtifactContent.t;
+ encoding: string;
+ sourceLanguage: string;
+ hashes: JsonStringDictionary.t;
+ lastModifiedTimeUtc: string;
+ properties: Properties.t;
+ }[@@deriving yojson]
+
+ val create:
+ ?description: Message.t ->
+ ?location: ArtifactLocation.t ->
+ ?parentIndex: int ->
+ ?offset: int ->
+ ?length: int ->
+ ?roles: Role.t list ->
+ ?mimeType: string ->
+ ?contents: ArtifactContent.t ->
+ ?encoding: string ->
+ ?sourceLanguage: string ->
+ ?hashes: JsonStringDictionary.t ->
+ ?lastModifiedTimeUtc: string ->
+ ?properties: Properties.t ->
+ unit -> t
+
+end
+
+module FileChange: sig
+ type t = {
+ artifactLocation: ArtifactLocation.t;
+ replacements: Replacement.t list
+ }[@@deriving yojson]
+end
+
+module Fix: sig
+ type t = {
+ description: (Message.t [@defaut Message.default]);
+ fileChanges: FileChange.t list;
+ }[@@deriving yojson]
+end
+
+module ExternalFiles: sig
+ type t = {
+ conversion: ArtifactLocation.t;
+ files: ArtifactLocation.t;
+ graphs: ArtifactLocation.t;
+ invocations: ArtifactLocation.t list;
+ logicalLocations: ArtifactLocation.t;
+ resources: ArtifactLocation.t;
+ results: ArtifactLocation.t;
+ }[@@deriving yojson]
+end
+
+module LogicalLocation: sig
+ type t = {
+ name: string;
+ fullyQualifiedName: string;
+ decoratedName: string;
+ parentKey: string;
+ kind: string;
+ }[@@deriving yojson]
+end
+
+module RuleConfigLevel:
+sig
+ include Json_type with type t = private string
+ val cl_none: t
+ val cl_note: t
+ val cl_warning: t
+ val cl_error: t
+end
+
+module ReportingConfiguration: sig
+ type t = {
+ enabled: bool;
+ defaultLevel: RuleConfigLevel.t;
+ rank: int;
+ parameters: Properties.t;
+ properties: Properties.t;
+ }[@@deriving yojson]
+
+ val default: t
+
+end
+
+module ToolComponentReference: sig
+ type t = {
+ name: string;
+ index: int;
+ guid: string;
+ properties: Properties.t;
+ }[@@deriving yojson]
+
+ val create:
+ ?name:string -> ?index:int -> ?guid:string -> ?properties:Properties.t ->
+ unit -> t
+
+ val default: t
+
+end
+
+module ReportingDescriptorReference: sig
+ type t = {
+ id: string;
+ index: int;
+ guid: string;
+ toolComponent: ToolComponentReference.t;
+ properties: Properties.t;
+ }[@@deriving yojson]
+
+ val create:
+ ?id: string -> ?index:int -> ?guid:string ->
+ ?toolComponent:ToolComponentReference.t ->
+ ?properties: Properties.t -> unit -> t
+
+ val default: t
+end
+
+module ReportingDescriptorRelationship: sig
+ type t = {
+ target: ReportingDescriptorReference.t;
+ kinds: string list;
+ description: Message.t;
+ properties: Properties.t;
+ }[@@deriving yojson]
+
+ val create:
+ target: ReportingDescriptorReference.t ->
+ ?kinds: string list ->
+ ?description:Message.t ->
+ ?properties:Properties.t -> unit -> t
+
+ val default: t
+
+end
+
+module ReportingDescriptor: sig
+ type t = {
+ id: string;
+ deprecatedIds: string list;
+ guid: string;
+ deprecatedGuids: string list;
+ name: string;
+ deprecatedNames: string list;
+ shortDescription: MultiformatMessageString.t;
+ fullDescription: MultiformatMessageString.t;
+ messageStrings: MultiformatMessageStringDictionary.t;
+ defaultConfiguration: ReportingConfiguration.t;
+ helpUri: string;
+ help: MultiformatMessageString.t;
+ relationships: ReportingDescriptorRelationship.t list;
+ properties: Properties.t;
+ }[@@deriving yojson]
+
+ val create:
+ id: string ->
+ ?deprecatedIds: string list ->
+ ?guid: string ->
+ ?deprecatedGuids: string list ->
+ ?name: string ->
+ ?deprecatedNames: string list ->
+ ?shortDescription: MultiformatMessageString.t ->
+ ?fullDescription: MultiformatMessageString.t ->
+ ?messageStrings: MultiformatMessageStringDictionary.t ->
+ ?defaultConfiguration: ReportingConfiguration.t ->
+ ?helpUri: string ->
+ ?help: MultiformatMessageString.t ->
+ ?relationships: ReportingDescriptorRelationship.t list ->
+ ?properties: Properties.t -> unit -> t
+
+ val default: t
+
+end
+
+module Result_kind:
+sig
+ type t = private string
+ val notApplicable: t
+ val pass: t
+ val fail: t
+ val review: t
+ val open_: t
+ val informational: t
+
+ val to_yojson: t -> Yojson.Safe.t
+ val of_yojson: Yojson.Safe.t -> (t,string) result
+end
+
+module Result_level:
+sig
+ type t = private string
+ val none: t
+ val note: t
+ val warning: t
+ val error: t
+
+ val to_yojson: t -> Yojson.Safe.t
+ val of_yojson: Yojson.Safe.t -> (t,string) result
+end
+
+module Result_suppressionState: sig
+ include Json_type with type t = private string
+ val suppressedInSource: t
+ val suppressedExternally: t
+end
+
+module Result_baselineState: sig
+ include Json_type with type t = private string
+ val bs_new: t
+ val bs_existing: t
+ val bs_absent: t
+end
+
+(* we can't use Result here, as this would conflict with
+ Ppx_deriving_yojson_runtime.Result that is opened by the
+ code generated by Ppx_deriving_yojson. *)
+module Sarif_result: sig
+ type t = {
+ ruleId: string;
+ kind: Result_kind.t;
+ level: Result_level.t;
+ message: Message.t;
+ analysisTarget: ArtifactLocation.t;
+ locations: Location.t list;
+ instanceGuid: string;
+ correlationGuid: string;
+ occurrenceCount: int;
+ partialFingerprints: Additional_properties.t;
+ fingerprints: Additional_properties.t;
+ stacks: Stack.t list;
+ codeFlows: CodeFlow.t list;
+ graphs: Graph_dictionary.t;
+ graphTraversals: GraphTraversal.t list;
+ relatedLocations: Location.t list;
+ suppressionStates: Result_suppressionState.t list;
+ baselineState: Result_baselineState.t;
+ attachments: Attachment.t list;
+ workItemsUris: string list;
+ conversionProvenance: PhysicalLocation.t list;
+ fixes: Fix.t list;
+ properties: Properties.t;
+ }[@@deriving yojson]
+
+ val create:
+ ruleId: string ->
+ ?kind: Result_kind.t ->
+ ?level: Result_level.t ->
+ ?message: Message.t ->
+ ?analysisTarget: ArtifactLocation.t ->
+ ?locations: Location.t list ->
+ ?instanceGuid: string ->
+ ?correlationGuid: string ->
+ ?occurrenceCount: int ->
+ ?partialFingerprints: Additional_properties.t ->
+ ?fingerprints: Additional_properties.t ->
+ ?stacks: Stack.t list ->
+ ?codeFlows: CodeFlow.t list ->
+ ?graphs: Graph_dictionary.t ->
+ ?graphTraversals: GraphTraversal.t list ->
+ ?relatedLocations: Location.t list ->
+ ?suppressionStates: Result_suppressionState.t list ->
+ ?baselineState: Result_baselineState.t ->
+ ?attachments: Attachment.t list ->
+ ?workItemsUris: string list ->
+ ?conversionProvenance: PhysicalLocation.t list ->
+ ?fixes: Fix.t list ->
+ ?properties: Properties.t ->
+ unit -> t
+
+end
+
+module VersionControlDetails: sig
+ type t = {
+ uri: string;
+ revisionId: string;
+ branch: string;
+ tag: string;
+ timestamp: string;
+ properties: Properties.t;
+ }[@@deriving yojson]
+end
+
+module ColumnKind: sig
+ include Json_type with type t = private string
+ val utf16CodeUnits: t
+ val unicodeCodePoints: t
+end
+
+module RunAutomationDetails: sig
+ type t = {
+ description: Message.t;
+ id: string;
+ guid: string;
+ correlationGuid: string;
+ properties: Properties.t;
+ } [@@deriving yojson]
+
+ val create:
+ ?description: Message.t -> ?id: string -> ?guid: string ->
+ ?correlationGuid: string -> ?properties: Properties.t ->
+ unit -> t
+
+ val default: t
+end
+
+module ExternalPropertyFileReferences: sig
+ type t = {
+ location: ArtifactLocation.t;
+ guid: string;
+ itemCount: int;
+ properties: Properties.t;
+ } [@@deriving yojson]
+
+ val create:
+ ?location: ArtifactLocation.t ->
+ ?guid: string ->
+ ?itemCount: int ->
+ ?properties: Properties.t ->
+ unit -> t
+
+ val default: t
+end
+
+module TranslationMetadata: sig
+ type t = {
+ name: string;
+ fullName: string;
+ shortDescription: MultiformatMessageString.t;
+ fullDescription: MultiformatMessageString.t;
+ downloadUri: string;
+ informationUri: string;
+ properties: Properties.t;
+ } [@@deriving yojson]
+
+ val create:
+ name: string ->
+ ?fullName: string ->
+ ?shortDescription: MultiformatMessageString.t ->
+ ?fullDescription: MultiformatMessageString.t ->
+ ?downloadUri: string ->
+ ?informationUri: string ->
+ ?properties: Properties.t ->
+ unit -> t
+
+ val default: t
+end
+
+module ToolComponent: sig
+ module Contents: sig
+ include Json_type with type t = private string
+ val localizedData: t
+ val nonLocalizedData: t
+ end
+ type t = {
+ guid: string;
+ name: string;
+ organization: string;
+ product: string;
+ productSuite: string;
+ shortDescription: MultiformatMessageString.t;
+ fullDescription: MultiformatMessageString.t;
+ fullName: string;
+ version: string;
+ semanticVersion: string;
+ dottedQuadFileVersion: string;
+ releaseDateUtc: string;
+ downloadUri: string;
+ informationUri: string;
+ globalMessageStrings: MultiformatMessageStringDictionary.t;
+ notifications: ReportingDescriptor.t list;
+ rules: ReportingDescriptor.t list;
+ taxa: ReportingDescriptor.t list;
+ locations: ArtifactLocation.t list;
+ language: string;
+ contents: Contents.t list;
+ isComprehensive: bool;
+ localizedDataSemanticVersion: string;
+ minimumRequiredLocalizedDataSemanticVersion: string;
+ associateComponent: ToolComponentReference.t;
+ translationMetadata: TranslationMetadata.t;
+ supportedTaxonomies: ToolComponentReference.t list;
+ properties: Properties.t;
+ }[@@deriving yojson]
+
+ val create:
+ ?guid: string ->
+ name: string ->
+ ?organization: string ->
+ ?product: string ->
+ ?productSuite: string ->
+ ?shortDescription: MultiformatMessageString.t ->
+ ?fullDescription: MultiformatMessageString.t ->
+ ?fullName: string ->
+ ?version: string ->
+ ?semanticVersion: string ->
+ ?dottedQuadFileVersion: string ->
+ ?releaseDateUtc: string ->
+ ?downloadUri: string ->
+ ?informationUri: string ->
+ ?globalMessageStrings: MultiformatMessageStringDictionary.t ->
+ ?notifications: ReportingDescriptor.t list ->
+ ?rules: ReportingDescriptor.t list ->
+ ?taxa: ReportingDescriptor.t list ->
+ ?locations: ArtifactLocation.t list ->
+ ?language: string ->
+ ?contents: Contents.t list ->
+ ?isComprehensive: bool ->
+ ?localizedDataSemanticVersion: string ->
+ ?minimumRequiredLocalizedDataSemanticVersion: string ->
+ ?associateComponent: ToolComponentReference.t ->
+ ?translationMetadata: TranslationMetadata.t ->
+ ?supportedTaxonomies: ToolComponentReference.t list ->
+ ?properties: Properties.t ->
+ unit -> t
+
+ val default: t
+end
+
+module Address: sig
+ type t = {
+ absoluteAddress: int;
+ relativeAddress: int;
+ length: int;
+ kind: string;
+ name: string;
+ fullyQualifiedName: string;
+ offsetFromParent: int;
+ index: int;
+ parentIndex: int;
+ properties: Properties.t;
+ } [@@deriving yojson]
+
+ val create:
+ ?absoluteAddress: int ->
+ ?relativeAddress: int ->
+ ?length: int ->
+ ?kind: string ->
+ ?name: string ->
+ ?fullyQualifiedName: string ->
+ ?offsetFromParent: int ->
+ ?index: int ->
+ ?parentIndex: int ->
+ ?properties: Properties.t ->
+ unit -> t
+
+ val default: t
+end
+
+module WebRequest: sig
+ type t = {
+ index: int;
+ protocol: string;
+ version: string;
+ target: string;
+ method_: string;
+ headers: JsonStringDictionary.t;
+ parameters: JsonStringDictionary.t;
+ body: ArtifactContent.t;
+ properties: Properties.t;
+ } [@@deriving yojson]
+
+ val create:
+ ?index: int ->
+ ?protocol: string ->
+ ?version: string ->
+ ?target: string ->
+ ?method_: string ->
+ ?headers: JsonStringDictionary.t ->
+ ?parameters: JsonStringDictionary.t ->
+ ?body: ArtifactContent.t ->
+ ?properties: Properties.t ->
+ unit -> t
+
+ val default: t
+
+end
+
+module WebResponse: sig
+ type t = {
+ index: int;
+ protocol: string;
+ version: string;
+ statusCode: int;
+ reasonPhrase: string;
+ headers: JsonStringDictionary.t;
+ body: ArtifactContent.t;
+ noResponseReceived: bool;
+ properties: Properties.t;
+ } [@@deriving yojson]
+
+ val create:
+ ?index: int ->
+ ?protocol: string ->
+ ?version: string ->
+ ?statusCode: int ->
+ ?reasonPhrase: string ->
+ ?headers: JsonStringDictionary.t ->
+ ?body: ArtifactContent.t ->
+ ?noResponseReceived: bool ->
+ ?properties: Properties.t ->
+ unit -> t
+
+ val default: t
+
+end
+
+module SpecialLocations: sig
+ type t = {
+ displayBase: ArtifactLocation.t;
+ properties: Properties.t;
+ } [@@deriving yojson]
+
+ val create:
+ ?displayBase: ArtifactLocation.t ->
+ ?properties: Properties.t ->
+ unit -> t
+
+ val default: t
+end
+
+module Run: sig
+ type t = {
+ tool: Tool.t;
+ invocations: Invocation.t list;
+ conversion: Conversion.t;
+ language: string;
+ versionControlProvenance: VersionControlDetails.t list;
+ originalUriBaseIds: ArtifactLocationDictionary.t;
+ artifacts: Artifact.t list;
+ logicalLocations: LogicalLocation.t list;
+ graphs: Graph.t list;
+ results: Sarif_result.t list;
+ automationDetails: RunAutomationDetails.t;
+ runAggregates: RunAutomationDetails.t list;
+ baselineGuid: string;
+ redactionToken: string list;
+ defaultEncoding: string;
+ defaultSourceLanguage: string;
+ newlineSequences: string list;
+ columnKind: ColumnKind.t;
+ externalPropertyFileReferences: ExternalPropertyFileReferences.t;
+ threadFlowLocations: ThreadFlowLocation.t list;
+ taxonomies: ToolComponent.t list;
+ addresses: Address.t list;
+ translations: ToolComponent.t list;
+ policies: ToolComponent.t list;
+ webRequests: WebRequest.t list;
+ webResponses: WebResponse.t list;
+ specialLocations: SpecialLocations.t;
+ properties: Properties.t;
+ }
+ [@@deriving yojson]
+
+ val create:
+ tool: Tool.t ->
+ ?invocations: Invocation.t list ->
+ ?conversion: Conversion.t ->
+ ?language: string ->
+ ?versionControlProvenance: VersionControlDetails.t list ->
+ ?originalUriBaseIds: ArtifactLocationDictionary.t ->
+ ?artifacts: Artifact.t list ->
+ ?logicalLocations: LogicalLocation.t list ->
+ ?graphs: Graph.t list ->
+ ?results: Sarif_result.t list ->
+ ?automationDetails:RunAutomationDetails.t ->
+ ?runAggregates: RunAutomationDetails.t list ->
+ ?baselineGuid: string ->
+ ?redactionToken: string list ->
+ ?defaultEncoding: string ->
+ ?defaultSourceLanguage: string ->
+ ?newlineSequences: string list ->
+ ?columnKind: ColumnKind.t ->
+ ?externalPropertyFileReferences: ExternalPropertyFileReferences.t ->
+ ?threadFlowLocations: ThreadFlowLocation.t list ->
+ ?taxonomies: ToolComponent.t list ->
+ ?addresses: Address.t list ->
+ ?translations: ToolComponent.t list ->
+ ?policies: ToolComponent.t list ->
+ ?webRequests: WebRequest.t list ->
+ ?webResponses: WebResponse.t list ->
+ ?specialLocations: SpecialLocations.t ->
+ ?properties: Properties.t ->
+ unit -> t
+end
+
+module Schema: sig
+ type t = {
+ schema: Uri.t;
+ version: Version.t;
+ runs: Run.t list
+ } [@@deriving yojson]
+
+ val create: ?schema: Uri.t -> ?version:Version.t -> runs: Run.t list ->
+ unit -> t
+
+end
diff --git a/src/plugins/metrics/css_html.mli b/src/plugins/metrics/css_html.mli
new file mode 100644
index 0000000000000000000000000000000000000000..8a0801e621bd49198c4ca801c425a7d77e0394b5
--- /dev/null
+++ b/src/plugins/metrics/css_html.mli
@@ -0,0 +1,23 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2021 *)
+(* 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). *)
+(* *)
+(**************************************************************************)
+
+val css: string
diff --git a/src/plugins/metrics/register.mli b/src/plugins/metrics/register.mli
new file mode 100644
index 0000000000000000000000000000000000000000..bf4d38e09ce8cf89921a5f88d286a79b1a6854d7
--- /dev/null
+++ b/src/plugins/metrics/register.mli
@@ -0,0 +1,23 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2021 *)
+(* 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). *)
+(* *)
+(**************************************************************************)
+
+(** Register the plugin in the Frama-C kernel. Nothing is exported. *)
diff --git a/src/plugins/metrics/register_gui.ml b/src/plugins/metrics/register_gui.ml
index 6cd3d4ad6b556d8b711ce147987db6ed4d644cc5..ace660eb586bb41b196a5e55fe44b4344204e7a9 100644
--- a/src/plugins/metrics/register_gui.ml
+++ b/src/plugins/metrics/register_gui.ml
@@ -22,25 +22,8 @@
(** This module defines abstraction for Metrics use *)
-
-let mk_bi_label (parent:GPack.box) l1 =
- let container = GPack.hbox ~packing:parent#pack () in
- let t = GMisc.label ~text:l1 ~xalign:0.0
- ~packing:(container#pack ~expand:false ~fill:true)
- ()
- in
- Gtk_helper.old_gtk_compat t#set_width_chars 7;
- let label = GMisc.label ~selectable:true ~xalign:0.0 ~text:""
- ~packing:(container#pack ~expand:true)
- ()
- in label
-
-
-
-
module HalsteadMetricsGUI = struct
- let compute = Metrics_cabs.compute_on_cabs
let name = "Halstead"
let display_result (main_ui:Design.main_window_extension_points) (parent_win:GPack.box) =
@@ -192,8 +175,6 @@ module CyclomaticMetricsGUI = struct
main_ui#register_source_selector self#cyclo_selector
end
- let compute ~libc () = Metrics_cilast.compute_on_cilast ~libc
-
let display_result ~libc (parent_win:GPack.box) =
let padder = GBin.alignment
~padding:(5, 5, 15, 15) ~packing:parent_win#pack () in
diff --git a/src/plugins/metrics/register_gui.mli b/src/plugins/metrics/register_gui.mli
new file mode 100644
index 0000000000000000000000000000000000000000..74f71e807575328df490c96638838ea7007ad21c
--- /dev/null
+++ b/src/plugins/metrics/register_gui.mli
@@ -0,0 +1,23 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2021 *)
+(* 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). *)
+(* *)
+(**************************************************************************)
+
+(** Extension of the Frama-C GUI for the plugin. Nothing is exported. *)
diff --git a/src/plugins/nonterm/nonterm_run.mli b/src/plugins/nonterm/nonterm_run.mli
new file mode 100644
index 0000000000000000000000000000000000000000..bf4d38e09ce8cf89921a5f88d286a79b1a6854d7
--- /dev/null
+++ b/src/plugins/nonterm/nonterm_run.mli
@@ -0,0 +1,23 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2021 *)
+(* 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). *)
+(* *)
+(**************************************************************************)
+
+(** Register the plugin in the Frama-C kernel. Nothing is exported. *)
diff --git a/src/plugins/obfuscator/obfuscator_register.mli b/src/plugins/obfuscator/obfuscator_register.mli
new file mode 100644
index 0000000000000000000000000000000000000000..bf4d38e09ce8cf89921a5f88d286a79b1a6854d7
--- /dev/null
+++ b/src/plugins/obfuscator/obfuscator_register.mli
@@ -0,0 +1,23 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2021 *)
+(* 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). *)
+(* *)
+(**************************************************************************)
+
+(** Register the plugin in the Frama-C kernel. Nothing is exported. *)
diff --git a/src/plugins/occurrence/register.ml b/src/plugins/occurrence/register.ml
index 9d4f0680471f3286ffbf940813c0ed386ef42b15..8d9d94741ec37ce7bf37449cc19674c8fc73cc66 100644
--- a/src/plugins/occurrence/register.ml
+++ b/src/plugins/occurrence/register.ml
@@ -38,8 +38,6 @@ module Occurrences: sig
(Cil_types.lhost * Cil_types.offset))
list * Cil_types.varinfo)
option
- val iter:
- (varinfo -> (kernel_function option * kinstr * lval) list -> unit) -> unit
val iter_sorted:
(varinfo -> (kernel_function option * kinstr * lval) list -> unit) -> unit
end = struct
@@ -96,7 +94,6 @@ end = struct
let map = IState.fold Varinfo.Map.add Varinfo.Map.empty in
Varinfo.Map.fold f map init
- let iter = iter_aux IState.fold
let iter_sorted = iter_aux fold_sorted
let self = IState.self
diff --git a/src/plugins/occurrence/register.mli b/src/plugins/occurrence/register.mli
new file mode 100644
index 0000000000000000000000000000000000000000..a8018a977b7372cb12a9828a71eadda0145c6b91
--- /dev/null
+++ b/src/plugins/occurrence/register.mli
@@ -0,0 +1,42 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2021 *)
+(* 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). *)
+(* *)
+(**************************************************************************)
+
+(** Register the plugin in the Frama-C kernel. *)
+
+open Cil_types
+
+val self: State.t
+
+val get_last_result:
+ unit -> ((kernel_function option * kinstr * lval) list * varinfo) option
+
+val get: (varinfo -> (kernel_function option * kinstr * lval) list)
+(** Return the occurrences of the given varinfo.
+ An occurrence [ki, lv] is a left-value [lv] which uses the location of
+ [vi] at the position [ki]. *)
+
+val print_all: (unit -> unit)
+(** Print all the occurrence of each variable declarations. *)
+
+type access_type = Read | Write | Both
+
+val classify_accesses: kernel_function option * kinstr *lval -> access_type
diff --git a/src/plugins/pdg/register.mli b/src/plugins/pdg/register.mli
new file mode 100644
index 0000000000000000000000000000000000000000..f54d0a9a8b07072f659aacc25fca02324311cdc1
--- /dev/null
+++ b/src/plugins/pdg/register.mli
@@ -0,0 +1,23 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2021 *)
+(* 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). *)
+(* *)
+(**************************************************************************)
+
+include module type of Marks
diff --git a/src/plugins/postdominators/compute.ml b/src/plugins/postdominators/compute.ml
index 7f520a7255a731bc2537eaeb4cafaa1ad4eced79..d0b257ac9a65ef5759a2b9b9e935fca9701bde32 100644
--- a/src/plugins/postdominators/compute.ml
+++ b/src/plugins/postdominators/compute.ml
@@ -23,7 +23,7 @@
open Cil_types
open Cil_datatype
-module DomKernel =
+include
Plugin.Register
(struct
let name = "dominators"
@@ -252,16 +252,15 @@ let output, _ = State_builder.apply_once "Postdominators.Compute.output"
let () = Db.Main.extend output
-module PostDomVal =
- PostDomDb(
- struct
- let is_accessible = Db.Value.is_reachable_stmt
- let dependencies = [ Db.Value.self ]
- let name = "value"
- let eval_cond stmt _e =
- Db.Value.condition_truth_value stmt
-
- end)
+include
+ PostDomDb
+ (struct
+ let is_accessible = Db.Value.is_reachable_stmt
+ let dependencies = [ Db.Value.self ]
+ let name = "value"
+ let eval_cond stmt _e =
+ Db.Value.condition_truth_value stmt
+ end)
(Db.PostdominatorsValue)
(*
diff --git a/src/plugins/postdominators/compute.mli b/src/plugins/postdominators/compute.mli
new file mode 100644
index 0000000000000000000000000000000000000000..bf4d38e09ce8cf89921a5f88d286a79b1a6854d7
--- /dev/null
+++ b/src/plugins/postdominators/compute.mli
@@ -0,0 +1,23 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2021 *)
+(* 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). *)
+(* *)
+(**************************************************************************)
+
+(** Register the plugin in the Frama-C kernel. Nothing is exported. *)
diff --git a/src/plugins/postdominators/print.mli b/src/plugins/postdominators/print.mli
new file mode 100644
index 0000000000000000000000000000000000000000..5303ff110311e63a8b95f0bfbfaad0c3a3ccc03a
--- /dev/null
+++ b/src/plugins/postdominators/print.mli
@@ -0,0 +1,23 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2021 *)
+(* 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). *)
+(* *)
+(**************************************************************************)
+
+val build_dot: string -> Kernel_function.t -> unit
diff --git a/src/plugins/print_api/lexer.mli b/src/plugins/print_api/lexer.mli
new file mode 100644
index 0000000000000000000000000000000000000000..50e5a8b1493f64247e4147e63048b049d10bb502
--- /dev/null
+++ b/src/plugins/print_api/lexer.mli
@@ -0,0 +1,23 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2021 *)
+(* 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). *)
+(* *)
+(**************************************************************************)
+
+val token: Lexing.lexbuf -> Grammar.token
diff --git a/src/plugins/print_api/print_interface.mli b/src/plugins/print_api/print_interface.mli
new file mode 100644
index 0000000000000000000000000000000000000000..bf4d38e09ce8cf89921a5f88d286a79b1a6854d7
--- /dev/null
+++ b/src/plugins/print_api/print_interface.mli
@@ -0,0 +1,23 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2021 *)
+(* 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). *)
+(* *)
+(**************************************************************************)
+
+(** Register the plugin in the Frama-C kernel. Nothing is exported. *)
diff --git a/src/plugins/qed/Makefile b/src/plugins/qed/Makefile
index 21d114d352f63d8252a7f9481e0e40c0e1d57f19..fb2350efe6e9561f0bcbe3c3803c7b266b8bda09 100644
--- a/src/plugins/qed/Makefile
+++ b/src/plugins/qed/Makefile
@@ -50,15 +50,15 @@ PLUGIN_CMO:= \
idxmap idxset \
mergemap mergeset collection \
partition cache \
- bvars logic \
+ bvars \
pool kind term \
- plib pretty engine export \
+ plib pretty export \
export_whycore \
export_altergo \
export_why3 \
export_coq \
-PLUGIN_GUI_CMO:= QedGui
+PLUGIN_CMI:= logic engine
PLUGIN_DEPENDENCIES:=
PLUGIN_TESTS_DIRS:=
@@ -83,9 +83,9 @@ QED_API= \
mergemap.mli mergeset.mli collection.mli \
partition.mli cache.mli \
bvars.mli \
- logic.ml \
+ logic.mli \
pool.mli kind.mli term.mli \
- plib.mli pretty.mli engine.ml export.mli \
+ plib.mli pretty.mli engine.mli export.mli \
export_whycore.mli \
export_altergo.mli \
export_why3.mli \
diff --git a/src/plugins/qed/engine.ml b/src/plugins/qed/engine.mli
similarity index 100%
rename from src/plugins/qed/engine.ml
rename to src/plugins/qed/engine.mli
diff --git a/src/plugins/qed/logic.ml b/src/plugins/qed/logic.mli
similarity index 100%
rename from src/plugins/qed/logic.ml
rename to src/plugins/qed/logic.mli
diff --git a/src/plugins/reduc/Reduc.mli b/src/plugins/reduc/Reduc.mli
index cce51dc83ef23f10bb7ed95d5a93dfc632b91896..49010ca1bf725583e882f7160ef2de77907aade5 100644
--- a/src/plugins/reduc/Reduc.mli
+++ b/src/plugins/reduc/Reduc.mli
@@ -19,3 +19,5 @@
(* for more details (enclosed in the file licenses/LGPLv2.1). *)
(* *)
(**************************************************************************)
+
+(* This plugin does not export anything *)
diff --git a/src/plugins/reduc/register.mli b/src/plugins/reduc/register.mli
new file mode 100644
index 0000000000000000000000000000000000000000..bf4d38e09ce8cf89921a5f88d286a79b1a6854d7
--- /dev/null
+++ b/src/plugins/reduc/register.mli
@@ -0,0 +1,23 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2021 *)
+(* 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). *)
+(* *)
+(**************************************************************************)
+
+(** Register the plugin in the Frama-C kernel. Nothing is exported. *)
diff --git a/src/plugins/rte/register.mli b/src/plugins/rte/register.mli
new file mode 100644
index 0000000000000000000000000000000000000000..bf4d38e09ce8cf89921a5f88d286a79b1a6854d7
--- /dev/null
+++ b/src/plugins/rte/register.mli
@@ -0,0 +1,23 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2021 *)
+(* 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). *)
+(* *)
+(**************************************************************************)
+
+(** Register the plugin in the Frama-C kernel. Nothing is exported. *)
diff --git a/src/plugins/scope/dpds_gui.ml b/src/plugins/scope/dpds_gui.ml
index 99e71b97d3a4444afea3e9682169463bc5bd216e..d9d87225b1b4a4361133aa4d48040a91fff153fc 100644
--- a/src/plugins/scope/dpds_gui.ml
+++ b/src/plugins/scope/dpds_gui.ml
@@ -162,7 +162,7 @@ end
module type DpdCmdSig = sig
type t_in
val help : string
- val get_info : (Kernel_function.t * Cil_types.stmt) option -> string
+ val _get_info : (Kernel_function.t * Cil_types.stmt) option -> string
val compute : Kernel_function.t -> Cil_types.stmt -> t_in -> string
val tag_stmt : Cil_types.stmt -> (string * GText.tag_property list)
val clear: unit -> unit
@@ -191,7 +191,7 @@ module DataScope : (DpdCmdSig with type t_in = lval) = struct
^"than at its value at L.\n\t"
^"For more information, please look at the Scope plugin documentation.")
- let get_info _kf_stmt_opt =
+ let _get_info _kf_stmt_opt =
if Stmt.Hptset.is_empty (Fscope.get ())
&& Stmt.Hptset.is_empty (FBscope.get ())
&& Stmt.Hptset.is_empty (Bscope.get ())
@@ -213,8 +213,6 @@ end
module Pscope (* : (DpdCmdSig with type t_in = code_annotation) *) = struct
- type t_in = code_annotation
-
module Pscope =
Make_StmtSetState
(struct let name = "Dpds_gui.Highlighter.Pscope" end)
@@ -233,7 +231,7 @@ module Pscope (* : (DpdCmdSig with type t_in = code_annotation) *) = struct
^"highlight the statements where the value of the assertion is also ok\n\t"
^"For more information, please look at the Scope plugin documentation.")
- let get_info _kf_stmt_opt =
+ let _get_info _kf_stmt_opt =
if Stmt.Hptset.is_empty (Pscope.get ())
then ""
else "[prop_scope] selected"
@@ -271,7 +269,7 @@ module ShowDef : (DpdCmdSig with type t_in = lval) = struct
^"not defined on some path from the beginning of the function.")
- let get_info _kf_stmt_opt =
+ let _get_info _kf_stmt_opt =
if Stmt.Map.is_empty (ShowDefState.get()) then ""
else "[show_def] selected"
@@ -345,7 +343,7 @@ module Zones : (DpdCmdSig with type t_in = lval) = struct
^"\tAfter this computation, the result Di will be printed in the "
^" information window each time a statement Li is selected.")
- let get_info kf_stmt_opt =
+ let _get_info kf_stmt_opt =
try
let zones, _ = ZonesState.get () in
match kf_stmt_opt with
diff --git a/src/plugins/scope/dpds_gui.mli b/src/plugins/scope/dpds_gui.mli
new file mode 100644
index 0000000000000000000000000000000000000000..74f71e807575328df490c96638838ea7007ad21c
--- /dev/null
+++ b/src/plugins/scope/dpds_gui.mli
@@ -0,0 +1,23 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2021 *)
+(* 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). *)
+(* *)
+(**************************************************************************)
+
+(** Extension of the Frama-C GUI for the plugin. Nothing is exported. *)
diff --git a/src/plugins/server/server_batch.mli b/src/plugins/server/server_batch.mli
new file mode 100644
index 0000000000000000000000000000000000000000..e472344b807649188e8567bf9720f5a7f7ca1d51
--- /dev/null
+++ b/src/plugins/server/server_batch.mli
@@ -0,0 +1,23 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2021 *)
+(* 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). *)
+(* *)
+(**************************************************************************)
+
+(* No interface, registered via side-effects *)
diff --git a/src/plugins/server/server_zmq.mli b/src/plugins/server/server_zmq.mli
new file mode 100644
index 0000000000000000000000000000000000000000..e472344b807649188e8567bf9720f5a7f7ca1d51
--- /dev/null
+++ b/src/plugins/server/server_zmq.mli
@@ -0,0 +1,23 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2021 *)
+(* 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). *)
+(* *)
+(**************************************************************************)
+
+(* No interface, registered via side-effects *)
diff --git a/src/plugins/slicing/api.ml b/src/plugins/slicing/api.ml
index d7271052fe2c434ac969950bb34ef490e72d6879..3ece47ef72315659e3f2c4756382c7912a072c2a 100644
--- a/src/plugins/slicing/api.ml
+++ b/src/plugins/slicing/api.ml
@@ -164,8 +164,8 @@ module Select = struct
let dyn_t = SlicingTypes.Sl_select.ty
type set = SlicingCmds.set
module S = Cil_datatype.Varinfo.Map.Make(SlicingTypes.Fct_user_crit)
+ type selections = S.t
let dyn_set = S.ty
-
(** {2 Journalized selectors } *)
let empty_selects = Journal.register
diff --git a/src/plugins/slicing/api.mli b/src/plugins/slicing/api.mli
new file mode 100644
index 0000000000000000000000000000000000000000..56527fb169143cffce49230016c2b4e0070a0265
--- /dev/null
+++ b/src/plugins/slicing/api.mli
@@ -0,0 +1,466 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2021 *)
+(* 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). *)
+(* *)
+(**************************************************************************)
+
+(* ---------------------------------------------------------------------- *)
+(** Global data management *)
+
+val split_slice :
+ SlicingInternals.fct_slice -> SlicingInternals.fct_slice list
+
+val merge_slices :
+ SlicingInternals.fct_slice ->
+ SlicingInternals.fct_slice -> replace:bool -> SlicingInternals.fct_slice
+
+val copy_slice : SlicingInternals.fct_slice -> SlicingInternals.fct_slice
+
+(* ---------------------------------------------------------------------- *)
+(** {1 Global setting } *)
+
+val self : State.t
+
+(* ---------------------------------------------------------------------- *)
+
+(** {2 Functions with journalized side effects } *)
+
+val set_modes :
+ ?calls:SlicingParameters.Mode.Calls.t ->
+ ?callers:SlicingParameters.Mode.Callers.t ->
+ ?sliceUndef:SlicingParameters.Mode.SliceUndef.t ->
+ ?keepAnnotations:SlicingParameters.Mode.KeepAnnotations.t -> unit -> unit
+
+
+(* ---------------------------------------------------------------------- *)
+
+(** {1 Slicing project } *)
+module Project : sig
+
+ (** {2 Values } *)
+
+ val default_slice_names :
+ Cil_types.kernel_function -> bool -> int -> string
+
+ (** {2 Functions with journalized side effects } *)
+
+ val reset_slicing : unit -> unit
+
+ val extract :
+ ?f_slice_names:(Kernel_function.t -> bool -> int -> string) ->
+ string -> Project.t
+
+ val print_dot : filename:string -> title:string -> unit
+
+ val change_slicing_level : Kernel_function.t -> int -> unit
+
+ (** {2 No needs of Journalization} *)
+
+ val is_directly_called_internal : Kernel_function.t -> bool
+
+ val is_called : Cil_types.kernel_function -> bool
+
+ val has_persistent_selection : Kernel_function.t -> bool
+
+ (** {2 Debug} *)
+
+ val pretty : Format.formatter -> unit
+
+end
+
+(* ---------------------------------------------------------------------- *)
+
+(** {1 Mark} *)
+module Mark : sig
+
+ type t = SlicingTypes.sl_mark
+ val dyn_t : SlicingTypes.Sl_mark.t Type.t
+
+ (** {2 No needs of Journalization} *)
+
+ val compare : SlicingTypes.sl_mark -> SlicingTypes.sl_mark -> int
+
+ val pretty : Format.formatter -> SlicingTypes.sl_mark -> unit
+
+ val make : data:bool -> addr:bool -> ctrl:bool -> SlicingTypes.sl_mark
+
+ val is_bottom : SlicingTypes.sl_mark -> bool
+
+ val is_spare : SlicingTypes.sl_mark -> bool
+
+ val is_ctrl : SlicingTypes.sl_mark -> bool
+
+ val is_data : SlicingTypes.sl_mark -> bool
+
+ val is_addr : SlicingTypes.sl_mark -> bool
+
+ val get_from_src_func : Kernel_function.t -> SlicingInternals.pdg_mark
+
+end
+
+(* ---------------------------------------------------------------------- *)
+
+(** {1 Selection} *)
+module Select : sig
+
+ type t = SlicingTypes.sl_select
+ val dyn_t : SlicingTypes.Sl_select.t Type.t
+
+ type set = SlicingCmds.set
+
+ type selections = SlicingTypes.Fct_user_crit.t Cil_datatype.Varinfo.Map.t
+
+ val dyn_set : selections Type.t
+
+ (** {2 Journalized selectors } *)
+
+ val empty_selects : selections
+
+ val select_stmt :
+ selections -> spare:bool -> Cil_datatype.Stmt.t -> Kernel_function.t -> selections
+
+ val select_stmt_ctrl :
+ selections -> spare:bool -> Cil_datatype.Stmt.t -> Kernel_function.t -> selections
+
+ val select_stmt_lval_rw :
+ selections ->
+ SlicingTypes.Sl_mark.t ->
+ rd:Datatype.String.Set.t ->
+ wr:Datatype.String.Set.t ->
+ Cil_datatype.Stmt.t ->
+ eval:Cil_datatype.Stmt.t -> Kernel_function.t -> selections
+
+ val select_stmt_lval :
+ selections ->
+ SlicingTypes.Sl_mark.t ->
+ Datatype.String.Set.t ->
+ before:bool ->
+ Cil_datatype.Stmt.t ->
+ eval:Cil_datatype.Stmt.t -> Kernel_function.t -> selections
+
+ val select_stmt_annots :
+ selections ->
+ SlicingTypes.Sl_mark.t ->
+ spare:bool ->
+ threat:bool ->
+ user_assert:bool ->
+ slicing_pragma:bool ->
+ loop_inv:bool ->
+ loop_var:bool -> Cil_datatype.Stmt.t -> Kernel_function.t -> selections
+
+ val select_func_lval :
+ selections ->
+ SlicingTypes.Sl_mark.t ->
+ Datatype.String.Set.t -> Kernel_function.t -> selections
+
+ val select_func_lval_rw :
+ selections ->
+ SlicingTypes.Sl_mark.t ->
+ rd:Datatype.String.Set.t ->
+ wr:Datatype.String.Set.t ->
+ eval:Cil_datatype.Stmt.t -> Kernel_function.t -> selections
+
+ val select_func_return : selections -> spare:bool -> Kernel_function.t -> selections
+
+ val select_func_calls_to :
+ selections -> spare:bool -> Kernel_function.t -> selections
+
+ val select_func_calls_into :
+ selections -> spare:bool -> Kernel_function.t -> selections
+
+ val select_func_annots :
+ selections ->
+ SlicingTypes.Sl_mark.t ->
+ spare:bool ->
+ threat:bool ->
+ user_assert:bool ->
+ slicing_pragma:bool ->
+ loop_inv:bool -> loop_var:bool -> Kernel_function.t -> selections
+
+ val select_func_zone :
+ SlicingCmds.set ->
+ SlicingTypes.sl_mark ->
+ Locations.Zone.t -> Cil_types.kernel_function -> SlicingCmds.set
+
+ val select_stmt_term :
+ SlicingCmds.set ->
+ SlicingTypes.sl_mark ->
+ Cil_types.term ->
+ Cil_types.stmt -> Cil_types.kernel_function -> SlicingCmds.set
+
+ val select_stmt_pred :
+ SlicingCmds.set ->
+ SlicingTypes.sl_mark ->
+ Cil_types.predicate ->
+ Cil_types.stmt -> Cil_types.kernel_function -> SlicingCmds.set
+
+ val select_stmt_annot :
+ SlicingCmds.set ->
+ SlicingTypes.sl_mark ->
+ spare:bool ->
+ Cil_types.code_annotation ->
+ Cil_types.stmt -> Cil_types.kernel_function -> SlicingCmds.set
+
+ val select_stmt_zone :
+ SlicingCmds.set ->
+ SlicingTypes.sl_mark ->
+ Locations.Zone.t ->
+ before:bool ->
+ Cil_types.stmt -> Cil_types.kernel_function -> SlicingCmds.set
+
+ val select_pdg_nodes :
+ SlicingCmds.set ->
+ SlicingTypes.sl_mark ->
+ PdgTypes.Node.t list -> Cil_types.kernel_function -> SlicingCmds.set
+
+ val get_function : SlicingTypes.sl_select -> Cil_types.kernel_function
+
+ val merge_internal :
+ Cil_datatype.Varinfo.t * SlicingInternals.fct_user_crit ->
+ Cil_datatype.Varinfo.t * SlicingInternals.fct_user_crit ->
+ Cil_datatype.Varinfo.t * SlicingInternals.fct_user_crit
+
+ val add_to_selects_internal :
+ Cil_datatype.Varinfo.Map.key * SlicingInternals.fct_user_crit ->
+ SlicingInternals.fct_user_crit Cil_datatype.Varinfo.Map.t ->
+ SlicingInternals.fct_user_crit Cil_datatype.Varinfo.Map.t
+
+ val iter_selects_internal :
+ (Cil_datatype.Varinfo.Map.key * 'a -> unit) ->
+ 'a Cil_datatype.Varinfo.Map.t -> unit
+
+ val fold_selects_internal :
+ ('a -> Cil_datatype.Varinfo.Map.key * 'b -> 'a) ->
+ 'a -> 'b Cil_datatype.Varinfo.Map.t -> 'a
+
+ val select_stmt_internal :
+ Kernel_function.t ->
+ ?select:Cil_datatype.Varinfo.t * SlicingInternals.fct_user_crit ->
+ Cil_types.stmt ->
+ SlicingTypes.sl_mark ->
+ Cil_datatype.Varinfo.t * SlicingInternals.fct_user_crit
+
+ val select_label_internal :
+ Kernel_function.t ->
+ ?select:Cil_datatype.Varinfo.t * SlicingInternals.fct_user_crit ->
+ Cil_types.logic_label ->
+ SlicingTypes.sl_mark ->
+ Cil_datatype.Varinfo.t * SlicingInternals.fct_user_crit
+
+ val select_min_call_internal :
+ Kernel_function.t ->
+ ?select:Cil_datatype.Varinfo.t * SlicingInternals.fct_user_crit ->
+ Cil_types.stmt ->
+ SlicingTypes.sl_mark ->
+ Cil_datatype.Varinfo.t * SlicingInternals.fct_user_crit
+
+ val select_stmt_zone_internal :
+ Kernel_function.t ->
+ ?select:Cil_datatype.Varinfo.t * SlicingInternals.fct_user_crit ->
+ Cil_types.stmt ->
+ before:bool ->
+ Locations.Zone.t ->
+ SlicingTypes.sl_mark ->
+ Cil_datatype.Varinfo.t * SlicingInternals.fct_user_crit
+
+ val select_zone_at_entry_point_internal :
+ Kernel_function.t ->
+ ?select:Cil_datatype.Varinfo.t * SlicingInternals.fct_user_crit ->
+ Locations.Zone.t ->
+ SlicingTypes.sl_mark ->
+ Cil_datatype.Varinfo.t * SlicingInternals.fct_user_crit
+
+ val select_zone_at_end_internal :
+ Kernel_function.t ->
+ ?select:Cil_datatype.Varinfo.t * SlicingInternals.fct_user_crit ->
+ Locations.Zone.t ->
+ SlicingTypes.sl_mark ->
+ Cil_datatype.Varinfo.t * SlicingInternals.fct_user_crit
+
+ val select_modified_output_zone_internal :
+ Kernel_function.t ->
+ ?select:Cil_datatype.Varinfo.t * SlicingInternals.fct_user_crit ->
+ Locations.Zone.t ->
+ SlicingTypes.sl_mark ->
+ Cil_datatype.Varinfo.t * SlicingInternals.fct_user_crit
+
+ val select_stmt_ctrl_internal :
+ Kernel_function.t ->
+ ?select:Cil_datatype.Varinfo.t * SlicingInternals.fct_user_crit ->
+ Cil_types.stmt ->
+ Cil_datatype.Varinfo.t * SlicingInternals.fct_user_crit
+
+ val select_entry_point_internal :
+ Kernel_function.t ->
+ ?select:Cil_datatype.Varinfo.t * SlicingInternals.fct_user_crit ->
+ SlicingTypes.sl_mark ->
+ Cil_datatype.Varinfo.t * SlicingInternals.fct_user_crit
+
+ val select_return_internal :
+ Kernel_function.t ->
+ ?select:Cil_datatype.Varinfo.t * SlicingInternals.fct_user_crit ->
+ SlicingTypes.sl_mark ->
+ Cil_datatype.Varinfo.t * SlicingInternals.fct_user_crit
+
+ val select_decl_var_internal :
+ Kernel_function.t ->
+ ?select:Cil_datatype.Varinfo.t * SlicingInternals.fct_user_crit ->
+ Cil_types.varinfo ->
+ SlicingTypes.sl_mark ->
+ Cil_datatype.Varinfo.t * SlicingInternals.fct_user_crit
+
+ val select_pdg_nodes_internal :
+ Kernel_function.t ->
+ ?select:Cil_datatype.Varinfo.t * SlicingInternals.fct_user_crit ->
+ PdgTypes.Node.t list ->
+ SlicingTypes.sl_mark ->
+ Cil_datatype.Varinfo.t * SlicingInternals.fct_user_crit
+
+ (** {2 Debug} *)
+
+ val pretty :
+ Format.formatter ->
+ Cil_datatype.Varinfo.t * SlicingInternals.fct_user_crit -> unit
+
+end
+
+(* ---------------------------------------------------------------------- *)
+
+(** {1 Slice} *)
+module Slice : sig
+
+ type t = SlicingTypes.sl_fct_slice
+ val dyn_t : SlicingTypes.Sl_fct_slice.t Type.t
+
+ (** {2 Functions with journalized side effects } *)
+
+ val create : Kernel_function.t -> SlicingTypes.Sl_fct_slice.t
+
+ val remove : SlicingTypes.Sl_fct_slice.t -> unit
+
+ val remove_uncalled : unit -> unit
+
+ (** {2 No needs of Journalization} *)
+
+ val get_all : Kernel_function.t -> SlicingInternals.fct_slice list
+
+ val get_function :
+ SlicingInternals.fct_slice -> Cil_types.kernel_function
+
+ val get_callers :
+ SlicingInternals.fct_slice -> SlicingInternals.fct_slice list
+
+ val get_called_slice :
+ SlicingInternals.fct_slice ->
+ Cil_types.stmt -> SlicingInternals.fct_slice option
+
+ val get_called_funcs :
+ SlicingInternals.fct_slice ->
+ Cil_types.stmt -> Kernel_function.Hptset.elt list
+
+ val get_mark_from_stmt :
+ SlicingInternals.fct_slice ->
+ Cil_types.stmt -> SlicingInternals.pdg_mark
+
+ val get_mark_from_label :
+ SlicingInternals.fct_slice ->
+ Cil_types.stmt -> Cil_types.label -> SlicingInternals.pdg_mark
+
+ val get_mark_from_local_var :
+ SlicingInternals.fct_slice ->
+ Cil_types.varinfo -> SlicingInternals.pdg_mark
+
+ val get_mark_from_formal :
+ SlicingInternals.fct_slice ->
+ Cil_datatype.Varinfo.t -> SlicingInternals.pdg_mark
+
+ val get_user_mark_from_inputs :
+ SlicingInternals.fct_slice -> SlicingInternals.pdg_mark
+
+ val get_num_id : SlicingInternals.fct_slice -> int
+
+ val from_num_id :
+ Kernel_function.t -> int -> SlicingInternals.fct_slice
+
+ (** {2 Debug} *)
+
+ val pretty : Format.formatter -> SlicingInternals.fct_slice -> unit
+
+end
+
+(* ---------------------------------------------------------------------- *)
+
+(** {1 Slicing request} *)
+module Request : sig
+
+ (** {2 Functions with journalized side effects } *)
+
+ val apply_all : propagate_to_callers:bool -> unit
+
+ val apply_all_internal : unit -> unit
+
+ val apply_next_internal : unit -> unit
+
+ val propagate_user_marks : unit -> unit
+
+ val copy_slice :
+ SlicingTypes.Sl_fct_slice.t -> SlicingTypes.Sl_fct_slice.t
+
+ val split_slice :
+ SlicingTypes.Sl_fct_slice.t -> SlicingTypes.Sl_fct_slice.t list
+
+ val merge_slices :
+ SlicingTypes.Sl_fct_slice.t ->
+ SlicingTypes.Sl_fct_slice.t ->
+ replace:bool -> SlicingTypes.Sl_fct_slice.t
+
+ val add_call_slice :
+ caller:SlicingTypes.Sl_fct_slice.t ->
+ to_call:SlicingTypes.Sl_fct_slice.t -> unit
+
+ val add_call_fun :
+ caller:SlicingTypes.Sl_fct_slice.t ->
+ to_call:Kernel_function.t -> unit
+
+ val add_call_min_fun :
+ caller:SlicingTypes.Sl_fct_slice.t ->
+ to_call:Kernel_function.t -> unit
+
+ val add_selection : Select.selections -> unit
+
+ val add_persistent_selection : Select.selections -> unit
+
+ val add_persistent_cmdline : unit -> unit
+
+ (** {2 No needs of Journalization} *)
+
+ val is_request_empty_internal : unit -> bool
+
+ val add_slice_selection_internal :
+ SlicingInternals.fct_slice ->
+ Cil_datatype.Varinfo.t * SlicingInternals.fct_user_crit -> unit
+
+ val add_selection_internal :
+ Cil_datatype.Varinfo.t * SlicingInternals.fct_user_crit -> unit
+
+ (** {2 Debug} *)
+
+ val pretty : Format.formatter -> unit
+
+end
diff --git a/src/plugins/slicing/register.mli b/src/plugins/slicing/register.mli
new file mode 100644
index 0000000000000000000000000000000000000000..bf4d38e09ce8cf89921a5f88d286a79b1a6854d7
--- /dev/null
+++ b/src/plugins/slicing/register.mli
@@ -0,0 +1,23 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2021 *)
+(* 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). *)
+(* *)
+(**************************************************************************)
+
+(** Register the plugin in the Frama-C kernel. Nothing is exported. *)
diff --git a/src/plugins/slicing/slicingInternals.mli b/src/plugins/slicing/slicingInternals.mli
new file mode 100644
index 0000000000000000000000000000000000000000..0f1d865f08f2e33d215b4ecd6d56b53e687e5ec5
--- /dev/null
+++ b/src/plugins/slicing/slicingInternals.mli
@@ -0,0 +1,229 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2021 *)
+(* 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). *)
+(* *)
+(**************************************************************************)
+
+(** {2 Internals types}
+ Internals type definitions should be hidden to the outside world,
+ but it is not really possible to have abstract types since Slicing has to
+ use Db.Slicing functions... *)
+
+open Cil_datatype
+
+(** {3 About options} *)
+
+(** associate a level to each function in order to control how it will be
+ * specialized. This is only a hint used when the tool has to make a choice,
+ * but it doesn't forbid to the user to do whatever he wants
+ * (like building slices for a [DontSlice] function). *)
+type level_option =
+ | DontSlice (** don't build slice for the function :
+ ie. always call the source function. *)
+ | DontSliceButComputeMarks
+ (** don't slice the called functions,
+ * but compute the marks for them *)
+ | MinNbSlice (** try to use existing slices, create at most one *)
+ | MaxNbSlice (** most precise slices
+ (but merge slices with the same visibility,
+ even if they don't have the same marks) *)
+
+(** {3 About function slice} *)
+
+(** Kinds of elementary marks. *)
+type mark = Cav of PdgTypes.Dpd.t
+ | Spare
+
+val compare_mark : mark -> mark -> int
+
+(** Each PDG element has 2 marks to deal with interprocedural propagation *)
+type pdg_mark = {m1 : mark ; m2 : mark }
+
+val pdg_mark_packed_descr : Structural_descr.pack
+
+val compare_pdg_mark : pdg_mark -> pdg_mark -> int
+
+(** Type for all the informations related to any function,
+ * even if we don't have its definition. *)
+type fct_info = {
+ fi_kf : Cil_types.kernel_function;
+ fi_def : Cil_types.fundec option;
+ mutable fi_top : pdg_mark option;
+ (** indicates if the function is marked top (=> src visible) *)
+ mutable fi_level_option : level_option;
+ (** level of specialisation for this function *)
+ mutable fi_init_marks : ff_marks option;
+ (** the marks that must be in every slices of that function *)
+ mutable fi_slices : fct_slice list ;
+ (** the list of the slices already computed for this function. *)
+ mutable fi_next_ff_num : int;
+ (** the number to assign to the next slice. *)
+ mutable f_called_by : called_by;
+ (** calls in slices that call source fct *)
+}
+
+and
+ (** to represent where a function is called. *)
+ called_by = (fct_slice * Cil_types.stmt) list
+
+and
+ (** Function slice :
+ created as soon as there is a criterion to compute it,
+ even if the slice itself hasn't been computed yet.
+ *)
+ fct_slice = {
+ ff_fct : fct_info ;
+ ff_id : int ;
+ mutable ff_marks : ff_marks;
+ mutable ff_called_by : called_by
+}
+
+and
+ (** [fct_id] is used to identify either a source function or a sliced one.*)
+ fct_id =
+ | FctSrc of fct_info (** source function *)
+ | FctSliced of fct_slice (** sliced function *)
+
+and
+ called_fct =
+ | CallSrc of fct_info option
+ (** call the source function (might be unknown if the call uses pointer) *)
+ | CallSlice of fct_slice
+
+and
+ (** information about a call in a slice which gives the function to call *)
+ call_info = called_fct option
+
+and
+ (** main part of a slice = mapping between the function elements
+ * and information about them in the slice. *)
+ marks_index = (pdg_mark, call_info) PdgIndex.FctIndex.t
+
+and
+ ff_marks = PdgTypes.Pdg.t * marks_index
+
+and
+ project = { functions : fct_info Varinfo.Hashtbl.t;
+ mutable actions : criterion list;
+ }
+
+and
+ (** Slicing criterion at the application level.
+ When applied, they are translated into [fct_criterion]
+ *)
+ appli_criterion =
+ | CaGlobalData of Locations.Zone.t
+ (** select all that is necessary to compute the given location. *)
+ | CaCall of fct_info
+ (** select all that is necessary to call the given function.
+ * Its application generates requests to add persistent selection
+ * to all the function callers. *)
+ | CaOther
+
+and
+ (** Base criterion for the functions. These are the only one that can
+ really generate function slices. All the other criteria are
+ translated in more basic ones.
+ Note that to build such a base criterion, the PDG has to be already
+ computed.
+ *)
+ fct_base_criterion = pdg_mark PdgMarks.select
+
+and
+ (** Used to identify a location (zone) at a given program point.
+ * The boolean tell if the point is before (true) or after the statement *)
+ loc_point = Cil_types.stmt * Locations.Zone.t * bool
+
+(** List of pdg nodes to be selected (see {!fct_user_crit})*)
+(*type nodes = pdg_node list*)
+
+and
+ (** [node_or_dpds] tells how we want to select nodes,
+ * or some of their dependencies (see {!fct_user_crit}). *)
+ node_or_dpds = CwNode | CwAddrDpds | CwDataDpds | CwCtrlDpds
+
+and
+ (** Tells which marks we want to put in the slice of a function *)
+ fct_user_crit =
+ (* | CuNodes of (pdg_node list * (node_or_dpds * pdg_mark) list) list *)
+ | CuSelect of pdg_mark PdgMarks.select
+ | CuTop of pdg_mark (** the function has probably no PDG,
+ but we nonetheless give a mark to propagate *)
+and
+ (** kinds of actions that can be apply to a function *)
+ fct_crit =
+ | CcUserMark of fct_user_crit
+ (** add marks to a slice *)
+ | CcChooseCall of Cil_types.stmt
+ (** have to choose what function to call here. *)
+ | CcChangeCall of Cil_types.stmt * called_fct
+ (** call the [called_fct] for the given call [Cil_types.stmt] *)
+ | CcMissingOutputs of Cil_types.stmt * (pdg_mark PdgMarks.select) * bool
+ (** this call is affected to a function that doesn't compute enough
+ * outputs : we will have to choose between adding outputs to that slice,
+ * or call another one. The boolean tells if the modifications would
+ * change the visibility of some outputs. *)
+ | CcMissingInputs of Cil_types.stmt * (pdg_mark PdgMarks.select) * bool
+ (** the function calls a slice that has been modified :
+ * and doesn't compute not enough inputs.
+ * We will have to choose between adding marks to this function,
+ * and call another slice.
+ * The boolean tells if the modifications would
+ * change the visibility of some inputs. *)
+ | CcPropagate of (pdg_mark PdgMarks.select)
+ (** simply propagate the given marks *)
+ | CcExamineCalls of pdg_mark PdgMarks.info_called_outputs
+and
+ (** Slicing criterion for a function. *)
+ fct_criterion = {
+ cf_fct : fct_id ;
+ (** Identification of the {b RESULT} of this filter.
+ * When it a a slice, it might be an existing slice that will be modified,
+ * or a new one will be created during application.
+ * When it is the source function, it means what the criterion has to be
+ * applied on each existing slice, and stored into the initial marks of
+ * the function.
+ *)
+ cf_info : fct_crit
+}
+and
+ (** A slicing criterion is either an application level criterion,
+ * or a function level one. *)
+ criterion =
+ CrAppli of appli_criterion | CrFct of fct_criterion
+
+(** {2 Internals values} *)
+
+(** {3 For the journalization of these internals types} *)
+
+val dummy_pdg_mark : pdg_mark
+
+val dummy_fct_info : fct_info
+
+val dummy_marks_index : (pdg_mark, call_info) PdgIndex.FctIndex.t
+
+val dummy_ff_marks :
+ PdgTypes.Pdg.t * (pdg_mark, call_info) PdgIndex.FctIndex.t
+
+val dummy_fct_slice : fct_slice
+
+val dummy_fct_user_crit : fct_user_crit
+
+(** The whole project. *)
+val dummy_project : project
diff --git a/src/plugins/slicing/slicingSelect.mli b/src/plugins/slicing/slicingSelect.mli
new file mode 100644
index 0000000000000000000000000000000000000000..8cd5674a961a80f966c4b3c10731a70fa2e2fa65
--- /dev/null
+++ b/src/plugins/slicing/slicingSelect.mli
@@ -0,0 +1,226 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2021 *)
+(* 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). *)
+(* *)
+(**************************************************************************)
+
+val check_call : Cil_types.stmt -> bool -> Cil_types.stmt
+
+val print_select :
+ Format.formatter ->
+ Cil_datatype.Varinfo.t * SlicingInternals.fct_user_crit -> unit
+
+val get_select_kf : Cil_types.varinfo * 'a -> Cil_types.kernel_function
+
+val check_db_select :
+ Cil_datatype.Varinfo.t ->
+ Cil_datatype.Varinfo.t * SlicingInternals.fct_user_crit ->
+ Cil_datatype.Varinfo.t * SlicingInternals.fct_user_crit
+
+val empty_db_select :
+ Kernel_function.t -> Cil_types.varinfo * SlicingInternals.fct_user_crit
+
+val top_db_select :
+ Kernel_function.t ->
+ SlicingInternals.pdg_mark ->
+ Cil_types.varinfo * SlicingInternals.fct_user_crit
+
+val check_kf_db_select :
+ Kernel_function.t ->
+ Cil_datatype.Varinfo.t * SlicingInternals.fct_user_crit ->
+ Cil_datatype.Varinfo.t * SlicingInternals.fct_user_crit
+
+val check_ff_db_select :
+ SlicingInternals.fct_slice ->
+ Cil_datatype.Varinfo.t * SlicingInternals.fct_user_crit ->
+
+ Cil_datatype.Varinfo.t * SlicingInternals.fct_user_crit
+val bottom_msg : Kernel_function.t -> unit
+
+val basic_add_select :
+ Kernel_function.t ->
+ Cil_datatype.Varinfo.t * SlicingInternals.fct_user_crit ->
+ PdgTypes.Node.t list ->
+ ?undef:Locations.Zone.t option * SlicingTypes.sl_mark ->
+ SlicingActions.n_or_d_marks ->
+ Cil_datatype.Varinfo.t * SlicingInternals.fct_user_crit
+
+val select_pdg_nodes :
+ Kernel_function.t ->
+ ?select:Cil_datatype.Varinfo.t * SlicingInternals.fct_user_crit ->
+ PdgTypes.Node.t list ->
+ SlicingTypes.sl_mark ->
+ Cil_datatype.Varinfo.t * SlicingInternals.fct_user_crit
+
+val mk_select :
+ Db.Pdg.t ->
+ SlicingActions.select ->
+ (PdgTypes.Node.t * Locations.Zone.t option) list ->
+ Locations.Zone.t option ->
+ SlicingTypes.sl_mark -> SlicingInternals.fct_user_crit
+
+val select_stmt_zone :
+ Kernel_function.t ->
+ ?select:Cil_datatype.Varinfo.t * SlicingInternals.fct_user_crit ->
+ Cil_types.stmt ->
+ before:bool ->
+ Locations.Zone.t ->
+ SlicingTypes.sl_mark ->
+ Cil_datatype.Varinfo.t * SlicingInternals.fct_user_crit
+
+(** this one is similar to [select_stmt_zone] with the return statement
+ * when the function is defined, but it can also be used for undefined functions. *)
+val select_in_out_zone :
+ at_end:bool ->
+ use_undef:bool ->
+ Kernel_function.t ->
+ Cil_datatype.Varinfo.t * SlicingInternals.fct_user_crit ->
+ Locations.Zone.t ->
+ SlicingTypes.sl_mark ->
+ Cil_datatype.Varinfo.t * SlicingInternals.fct_user_crit
+
+val select_zone_at_end :
+ Kernel_function.t ->
+ ?select:Cil_datatype.Varinfo.t * SlicingInternals.fct_user_crit ->
+ Locations.Zone.t ->
+ SlicingTypes.sl_mark ->
+ Cil_datatype.Varinfo.t * SlicingInternals.fct_user_crit
+
+val select_modified_output_zone :
+ Kernel_function.t ->
+ ?select:Cil_datatype.Varinfo.t * SlicingInternals.fct_user_crit ->
+ Locations.Zone.t ->
+ SlicingTypes.sl_mark ->
+ Cil_datatype.Varinfo.t * SlicingInternals.fct_user_crit
+
+val select_zone_at_entry :
+ Kernel_function.t ->
+ ?select:Cil_datatype.Varinfo.t * SlicingInternals.fct_user_crit ->
+ Locations.Zone.t ->
+ SlicingTypes.sl_mark ->
+ Cil_datatype.Varinfo.t * SlicingInternals.fct_user_crit
+
+val stmt_nodes_to_select :
+ Db.Pdg.t -> Cil_types.stmt -> PdgTypes.Node.t list
+
+val select_stmt_computation :
+ Kernel_function.t ->
+ ?select:Cil_datatype.Varinfo.t * SlicingInternals.fct_user_crit ->
+ Cil_types.stmt ->
+ SlicingTypes.sl_mark ->
+ Cil_datatype.Varinfo.t * SlicingInternals.fct_user_crit
+
+val select_label :
+ Kernel_function.t ->
+ ?select:Cil_datatype.Varinfo.t * SlicingInternals.fct_user_crit ->
+ Cil_types.logic_label ->
+ SlicingTypes.sl_mark ->
+ Cil_datatype.Varinfo.t * SlicingInternals.fct_user_crit
+
+(** marking a call node means that a [choose_call] will have to decide that to
+ * call according to the slicing-level, but anyway, the call will be visible.
+*)
+val select_minimal_call :
+ Kernel_function.t ->
+ ?select:Cil_datatype.Varinfo.t * SlicingInternals.fct_user_crit ->
+ Cil_types.stmt ->
+ SlicingTypes.sl_mark ->
+ Cil_datatype.Varinfo.t * SlicingInternals.fct_user_crit
+
+val select_stmt_ctrl :
+ Kernel_function.t ->
+ ?select:Cil_datatype.Varinfo.t * SlicingInternals.fct_user_crit ->
+ Cil_types.stmt -> Cil_datatype.Varinfo.t * SlicingInternals.fct_user_crit
+
+val select_entry_point :
+ Kernel_function.t ->
+ ?select:Cil_datatype.Varinfo.t * SlicingInternals.fct_user_crit ->
+ SlicingTypes.sl_mark ->
+ Cil_datatype.Varinfo.t * SlicingInternals.fct_user_crit
+
+val select_return :
+ Kernel_function.t ->
+ ?select:Cil_datatype.Varinfo.t * SlicingInternals.fct_user_crit ->
+ SlicingTypes.sl_mark ->
+ Cil_datatype.Varinfo.t * SlicingInternals.fct_user_crit
+
+val select_decl_var :
+ Kernel_function.t ->
+ ?select:Cil_datatype.Varinfo.t * SlicingInternals.fct_user_crit ->
+ Cil_types.varinfo ->
+ SlicingTypes.sl_mark ->
+ Cil_datatype.Varinfo.t * SlicingInternals.fct_user_crit
+
+val merge_select :
+ SlicingInternals.fct_user_crit ->
+ SlicingInternals.fct_user_crit -> SlicingInternals.fct_user_crit
+
+val merge_db_select :
+ Cil_datatype.Varinfo.t * SlicingInternals.fct_user_crit ->
+ Cil_datatype.Varinfo.t * SlicingInternals.fct_user_crit ->
+ Cil_datatype.Varinfo.t * SlicingInternals.fct_user_crit
+
+module Selections : sig
+
+ val add_to_selects :
+ Cil_datatype.Varinfo.Map.key * SlicingInternals.fct_user_crit ->
+ SlicingInternals.fct_user_crit Cil_datatype.Varinfo.Map.t ->
+ SlicingInternals.fct_user_crit Cil_datatype.Varinfo.Map.t
+
+ val iter_selects_internal :
+ (Cil_datatype.Varinfo.Map.key * 'a -> unit) ->
+ 'a Cil_datatype.Varinfo.Map.t -> unit
+
+ val fold_selects_internal :
+ ('a -> Cil_datatype.Varinfo.Map.key * 'b -> 'a) ->
+ 'a -> 'b Cil_datatype.Varinfo.Map.t -> 'a
+end
+
+val add_crit_ff_change_call :
+ SlicingInternals.fct_slice ->
+ Cil_types.stmt -> SlicingInternals.called_fct -> unit
+
+(** change the call to call the given slice.
+ * This is a user request, so it might be the case that
+ * the new function doesn't compute enough outputs :
+ * in that case, add outputs first.
+*)
+val call_ff_in_caller :
+ caller:SlicingInternals.fct_slice ->
+ to_call:SlicingInternals.fct_slice -> unit
+
+val call_fsrc_in_caller :
+ caller:SlicingInternals.fct_slice -> to_call:Kernel_function.t -> unit
+
+val call_min_f_in_caller :
+ caller:SlicingInternals.fct_slice ->
+ to_call:Cil_types.kernel_function -> unit
+
+val is_already_selected :
+ SlicingInternals.fct_slice ->
+ Cil_datatype.Varinfo.t * SlicingInternals.fct_user_crit -> bool
+
+val add_ff_selection :
+ SlicingInternals.fct_slice ->
+ Cil_datatype.Varinfo.t * SlicingInternals.fct_user_crit -> unit
+
+(** add a persistent selection to the function.
+ * This might change its slicing level in order to call slices later on. *)
+val add_fi_selection :
+ Cil_datatype.Varinfo.t * SlicingInternals.fct_user_crit -> unit
diff --git a/src/plugins/slicing/slicingTypes.mli b/src/plugins/slicing/slicingTypes.mli
new file mode 100644
index 0000000000000000000000000000000000000000..34473da775d41dc839a8cb71b239c744878e1db8
--- /dev/null
+++ b/src/plugins/slicing/slicingTypes.mli
@@ -0,0 +1,89 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2021 *)
+(* 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). *)
+(* *)
+(**************************************************************************)
+
+(** Slicing module types. *)
+
+exception Slicing_Internal_Error of string
+exception ChangeCallErr of string
+exception PtrCallExpr
+exception CantRemoveCalledFf
+exception WrongSlicingLevel
+
+(** raised when someone tries to build more than one slice for the entry point.
+ * *)
+exception OnlyOneEntryPointSlice
+
+(** raised when one tries to select something in a function where we are not
+ * able to compute the Pdg. *)
+exception NoPdg
+
+(** {2 Public types}
+ * These types are the only one that should be used by the API functions.
+ * Public type definitions should be hidden to the outside world,
+ * but it is not really possible to have abstract types since Slicing has to
+ * use Db.Slicing functions... So, it is up to the user of this module to use
+ * only this public part.
+*)
+
+(** contains global things that has been computed so far
+ for the slicing project.
+ This includes :
+ - the slices of the functions,
+ - and the queue of actions to be applied.
+*)
+type sl_project = SlicingInternals.project
+
+(** Type of the selections
+ * (we store the varinfo because we cannot use the kernel_function in this file)
+ * *)
+type sl_select = Cil_types.varinfo * SlicingInternals.fct_user_crit
+
+module Fct_user_crit : Datatype.S with type t = SlicingInternals.fct_user_crit
+
+(** Function slice *)
+type sl_fct_slice = SlicingInternals.fct_slice
+
+(** Marks : used to put 'colors' in the result *)
+type sl_mark = SlicingInternals.pdg_mark
+
+(** {3 For the journalization of values of these types} *)
+
+val pp_sl_project : Type.precedence -> Format.formatter -> 'a -> unit
+
+module Sl_project : Datatype.S with type t = sl_project
+
+module Sl_select : Datatype.S with type t = sl_select
+
+val pp_sl_fct_slice :
+ Type.precedence -> Format.formatter -> SlicingInternals.fct_slice -> unit
+
+module Sl_fct_slice : Datatype.S with type t = SlicingInternals.fct_slice
+
+val dyn_sl_fct_slice : Sl_fct_slice.t Type.t
+
+val pp_sl_mark :
+ Type.precedence -> Format.formatter -> SlicingInternals.pdg_mark -> unit
+
+module Sl_mark : Datatype.S_with_collections with
+ type t = SlicingInternals.pdg_mark
+
+val dyn_sl_mark : Sl_mark.t Type.t
diff --git a/src/plugins/sparecode/globs.ml b/src/plugins/sparecode/globs.ml
index bdbc159416ca3a3968a8000726061e9c79f48cf4..2beb56b02391c49ee0a3bbd6b49f5ee3b87a567b 100644
--- a/src/plugins/sparecode/globs.ml
+++ b/src/plugins/sparecode/globs.ml
@@ -26,7 +26,6 @@ open Cil
let dkey = Sparecode_params.register_category "globs"
let debug format = Sparecode_params.debug ~dkey ~level:2 format
-let debug' format = Sparecode_params.debug ~dkey ~level:3 format
let used_variables = Hashtbl.create 257
let var_init = Hashtbl.create 257
diff --git a/src/plugins/sparecode/globs.mli b/src/plugins/sparecode/globs.mli
new file mode 100644
index 0000000000000000000000000000000000000000..b3bfdd81f7c7bf83f0bcbf0c98e9e53827e97d32
--- /dev/null
+++ b/src/plugins/sparecode/globs.mli
@@ -0,0 +1,23 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2021 *)
+(* 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). *)
+(* *)
+(**************************************************************************)
+
+val rm_unused_decl: string -> Project_skeleton.t
diff --git a/src/plugins/sparecode/register.mli b/src/plugins/sparecode/register.mli
new file mode 100644
index 0000000000000000000000000000000000000000..b55656795aa56aad775690406e707eab0459c803
--- /dev/null
+++ b/src/plugins/sparecode/register.mli
@@ -0,0 +1,34 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2021 *)
+(* 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). *)
+(* *)
+(**************************************************************************)
+
+val get: select_annot:bool -> select_slice_pragma:bool -> Project.t
+(** Remove in each function what isn't used to compute its outputs,
+ or its annotations when [select_annot] is true,
+ or its slicing pragmas when [select_slice_pragmas] is true.
+ @return a new project where the sparecode has been removed. *)
+
+val rm_unused_globals : ?new_proj_name:string -> ?project:Project.t -> unit -> Project.t
+(** Remove unused global types and variables from the given project
+ (the current one if no project given).
+ The source project is not modified.
+ The result is in the returned new project.
+ @modify Carbon-20110201 optional argument [new_proj_name] added. *)
diff --git a/src/plugins/sparecode/transform.mli b/src/plugins/sparecode/transform.mli
new file mode 100644
index 0000000000000000000000000000000000000000..a89bf49bcd416ad700ee477898fabcb760bf1176
--- /dev/null
+++ b/src/plugins/sparecode/transform.mli
@@ -0,0 +1,25 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2021 *)
+(* 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). *)
+(* *)
+(**************************************************************************)
+
+module Info: sig
+ val build_cil_file: ?last:bool -> string -> Spare_marks.proj -> Project.t
+end
diff --git a/src/plugins/studia/studia_gui.mli b/src/plugins/studia/studia_gui.mli
index cce51dc83ef23f10bb7ed95d5a93dfc632b91896..5f8a7338f77671ab186f3c88a3688c883d28b0df 100644
--- a/src/plugins/studia/studia_gui.mli
+++ b/src/plugins/studia/studia_gui.mli
@@ -19,3 +19,5 @@
(* for more details (enclosed in the file licenses/LGPLv2.1). *)
(* *)
(**************************************************************************)
+
+(* no function exported *)
diff --git a/src/plugins/users/users_register.mli b/src/plugins/users/users_register.mli
new file mode 100644
index 0000000000000000000000000000000000000000..adf4de554ad53d2afb6246a2c7cd0284998d518c
--- /dev/null
+++ b/src/plugins/users/users_register.mli
@@ -0,0 +1,23 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2021 *)
+(* 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). *)
+(* *)
+(**************************************************************************)
+
+val get: (Kernel_function.t -> Kernel_function.Hptset.t)
diff --git a/src/plugins/variadic/classify.mli b/src/plugins/variadic/classify.mli
new file mode 100644
index 0000000000000000000000000000000000000000..c63bca9665aa44f1c5de28b7e15e9a603709a9c2
--- /dev/null
+++ b/src/plugins/variadic/classify.mli
@@ -0,0 +1,35 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2021 *)
+(* 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). *)
+(* *)
+(**************************************************************************)
+
+(** Checks if the given name is the name of a Frama-C builtin *)
+val is_frama_c_builtin : string -> bool
+
+(** Checks if the given name is the name of one of the variadic va_* builtins *)
+val is_va_builtin : string -> bool
+
+(** Checks if a varinfo is a variadic function *)
+val is_variadic_function : Cil_types.varinfo -> bool
+
+(** Build a variadic function record for the given [varinfo] according to its
+ classification. Returns [None] if the function is not variadic. *)
+val classify : Environment.t -> Cil_types.varinfo ->
+ Va_types.variadic_function option
diff --git a/src/plugins/variadic/environment.ml b/src/plugins/variadic/environment.ml
index a7b9b7e3441cc622b2429f6df79e168cf63d13a0..0fb7737edb8a8731e725fe06ea1dfaef5bde0536 100644
--- a/src/plugins/variadic/environment.ml
+++ b/src/plugins/variadic/environment.ml
@@ -24,7 +24,7 @@ open Cil_types
module Table = Datatype.String.Hashtbl
-type env =
+type t =
{
globals: varinfo Table.t;
functions: varinfo Table.t;
@@ -34,7 +34,7 @@ type env =
enums: enuminfo Table.t;
}
-let empty () : env =
+let empty () : t =
{
globals = Table.create 17;
functions = Table.create 17;
@@ -44,41 +44,41 @@ let empty () : env =
enums = Table.create 17;
}
-let add_global (env : env) (vi : varinfo) : unit =
+let add_global (env : t) (vi : varinfo) : unit =
Table.add env.globals vi.vname vi
-let add_function (env : env) (vi : varinfo) : unit =
+let add_function (env : t) (vi : varinfo) : unit =
Table.add env.functions vi.vname vi
-let add_typeinfo (env : env) (typeinfo : typeinfo) : unit =
+let add_typeinfo (env : t) (typeinfo : typeinfo) : unit =
Table.add env.typedefs typeinfo.torig_name typeinfo
-let add_compinfo (env : env) (compinfo : compinfo) : unit =
+let add_compinfo (env : t) (compinfo : compinfo) : unit =
let table = if compinfo.cstruct then env.structs else env.unions in
Table.add table compinfo.corig_name compinfo
-let add_enuminfo (env : env) (enuminfo : enuminfo) : unit =
+let add_enuminfo (env : t) (enuminfo : enuminfo) : unit =
Table.add env.enums enuminfo.eorig_name enuminfo
-let find_global (env : env) (vname : string) : varinfo =
+let find_global (env : t) (vname : string) : varinfo =
Table.find env.globals vname
-let find_function (env : env) (vname : string) : varinfo =
+let find_function (env : t) (vname : string) : varinfo =
Table.find env.functions vname
-let find_typedef (env : env) (tname : string) : typeinfo=
+let find_typedef (env : t) (tname : string) : typeinfo=
Table.find env.typedefs tname
-let find_struct (env : env) (tname : string) : compinfo =
+let find_struct (env : t) (tname : string) : compinfo =
Table.find env.structs tname
-let find_union (env : env) (tname : string) : compinfo =
+let find_union (env : t) (tname : string) : compinfo =
Table.find env.unions tname
-let find_enum (env : env) (tname : string) : enuminfo =
+let find_enum (env : t) (tname : string) : enuminfo =
Table.find env.enums tname
-let find_type (env : env) (namespace : Logic_typing.type_namespace)
+let find_type (env : t) (namespace : Logic_typing.type_namespace)
(tname : string) : typ =
match namespace with
| Logic_typing.Typedef ->
@@ -90,7 +90,7 @@ let find_type (env : env) (namespace : Logic_typing.type_namespace)
| Logic_typing.Enum ->
TEnum (find_enum env tname, [])
-let from_file (file : file) : env =
+let from_file (file : file) : t =
let env = empty () in
let v = object inherit Cil.nopCilVisitor
method! vglob glob =
diff --git a/src/plugins/variadic/environment.mli b/src/plugins/variadic/environment.mli
new file mode 100644
index 0000000000000000000000000000000000000000..94ccd17423f6bb872774913bb720d30b68ee683c
--- /dev/null
+++ b/src/plugins/variadic/environment.mli
@@ -0,0 +1,36 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2021 *)
+(* 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). *)
+(* *)
+(**************************************************************************)
+
+(* Builds an environement to resolve names of globals and functions which
+ can then be used, even if Frama-C global tables are not filled yet. *)
+
+type t
+
+val from_file : Cil_types.file -> t
+
+val find_global : t -> string -> Cil_types.varinfo
+val find_function : t -> string -> Cil_types.varinfo
+val find_typedef : t -> string -> Cil_types.typeinfo
+val find_struct : t -> string -> Cil_types.compinfo
+val find_union : t -> string -> Cil_types.compinfo
+val find_enum : t -> string -> Cil_types.enuminfo
+val find_type : t -> Logic_typing.type_namespace -> string -> Cil_types.typ
diff --git a/src/plugins/variadic/format_string.mli b/src/plugins/variadic/format_string.mli
new file mode 100644
index 0000000000000000000000000000000000000000..5a5f71c56c8ff0cae17dcb193df9b0157443bc04
--- /dev/null
+++ b/src/plugins/variadic/format_string.mli
@@ -0,0 +1,32 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2021 *)
+(* 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). *)
+(* *)
+(**************************************************************************)
+
+type t =
+ | String of string
+ | WString of int64 list
+
+exception OutOfBounds
+exception NotAscii of int64
+
+val get_char : t -> int -> char
+val get_wchar : t -> int -> int64
+val sub_string : t -> int -> int -> string
diff --git a/src/plugins/variadic/generic.mli b/src/plugins/variadic/generic.mli
new file mode 100644
index 0000000000000000000000000000000000000000..998ec9cdc661524a5beeae7f803d34dbb0dd8fc5
--- /dev/null
+++ b/src/plugins/variadic/generic.mli
@@ -0,0 +1,41 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2021 *)
+(* 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). *)
+(* *)
+(**************************************************************************)
+
+(* The vpar formal parameter *)
+val vpar : string * Cil_types.typ * Cil_types.attributes
+
+(* Shallow translation of variadic types *)
+val translate_type : Cil_types.typ -> Cil_types.typ
+
+(* Adds the vpar parameter to variadic functions *)
+val add_vpar : Cil_types.varinfo -> unit
+
+(* Translation of va_* builtins *)
+val translate_va_builtin : Cil_types.fundec -> Cil_types.instr ->
+ Cil_types.instr list
+
+(* Generic translation of calls *)
+val translate_call : fundec:Cil_types.fundec -> ghost:bool ->
+ Cil_types.block -> Cil_types.location ->
+ (Cil_types.exp -> Cil_types.exp list -> Cil_types.instr) ->
+ Cil_types.exp -> Cil_types.exp list ->
+ Cil_types.instr list
diff --git a/src/plugins/variadic/register.mli b/src/plugins/variadic/register.mli
new file mode 100644
index 0000000000000000000000000000000000000000..bf4d38e09ce8cf89921a5f88d286a79b1a6854d7
--- /dev/null
+++ b/src/plugins/variadic/register.mli
@@ -0,0 +1,23 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2021 *)
+(* 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). *)
+(* *)
+(**************************************************************************)
+
+(** Register the plugin in the Frama-C kernel. Nothing is exported. *)
diff --git a/src/plugins/variadic/standard.ml b/src/plugins/variadic/standard.ml
index 4cd812ec3d82c2e17440adb142995f8d54b9c13e..7b7deeeaf33514d0aa63683d05db7801e0063fe5 100644
--- a/src/plugins/variadic/standard.ml
+++ b/src/plugins/variadic/standard.ml
@@ -26,6 +26,8 @@ open Options
module List = Extends.List
module Typ = Extends.Typ
+type call_builder = Cil_types.exp -> Cil_types.exp list -> Cil_types.instr
+
let pp_prototype name fmt tparams =
Format.fprintf fmt "%s(%a)"
name
diff --git a/src/plugins/variadic/standard.mli b/src/plugins/variadic/standard.mli
new file mode 100644
index 0000000000000000000000000000000000000000..e87c717eb52aedb141230f6f114d42f4ad51ce91
--- /dev/null
+++ b/src/plugins/variadic/standard.mli
@@ -0,0 +1,47 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2021 *)
+(* 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). *)
+(* *)
+(**************************************************************************)
+
+(* Ugly ref *)
+val new_globals : (Cil_types.global list) ref
+
+type call_builder = Cil_types.exp -> Cil_types.exp list -> Cil_types.instr
+
+exception Translate_call_exn of Cil_types.varinfo
+
+val fallback_fun_call : callee:Cil_types.varinfo -> Cil_types.location ->
+ call_builder -> Va_types.variadic_function -> Cil_types.exp list ->
+ Cil_types.instr list
+
+val aggregator_call : fundec:Cil_types.fundec -> ghost:bool ->
+ Va_types.aggregator -> Cil_types.block -> Cil_types.location ->
+ call_builder -> Va_types.variadic_function -> Cil_types.exp list ->
+ Cil_types.instr list
+
+val overloaded_call : fundec:Cil_types.fundec -> Va_types.overload ->
+ Cil_types.block -> Cil_types.location -> call_builder ->
+ Va_types.variadic_function -> Cil_types.exp list ->
+ Cil_types.instr list
+
+val format_fun_call : fundec:Cil_types.fundec -> Environment.t ->
+ Va_types.format_fun -> Cil_types.block -> Cil_types.location ->
+ call_builder -> Va_types.variadic_function -> Cil_types.exp list ->
+ Cil_types.instr list
diff --git a/src/plugins/variadic/translate.mli b/src/plugins/variadic/translate.mli
new file mode 100644
index 0000000000000000000000000000000000000000..9b5ac5aee458366d99cb6355a4c10bc8df454e5a
--- /dev/null
+++ b/src/plugins/variadic/translate.mli
@@ -0,0 +1,23 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2021 *)
+(* 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). *)
+(* *)
+(**************************************************************************)
+
+val translate_variadics : Cil_types.file -> unit
diff --git a/src/plugins/wp/Makefile.in b/src/plugins/wp/Makefile.in
index a4b18ac20739034825c65368744722c99554305f..c45d0439131d37ea213d85f8ace3f15580456644 100644
--- a/src/plugins/wp/Makefile.in
+++ b/src/plugins/wp/Makefile.in
@@ -68,12 +68,12 @@ PLUGIN_CMO:= \
LogicUsage RefUsage \
Layout Region \
RegionAnnot RegionAccess RegionDump RegionAnalysis \
- cil2cfg normAtLabels wpPropId wpStrategy mcfg \
+ cil2cfg normAtLabels wpPropId wpStrategy \
Lang Repr Matrix Passive Splitter \
LogicBuiltins Definitions \
Cmath Cint Cfloat Vset Vlist Cstring Cvalues \
Letify Cleaning \
- Sigs Mstate Conditions \
+ Mstate Conditions \
Filtering \
Plang Pcfg Pcond \
CodeSemantics \
@@ -103,7 +103,8 @@ PLUGIN_CMO:= \
wpGenerator cfgGenerator \
Generator register VC
-PLUGIN_CMI:=
+PLUGIN_CMI:= \
+ Sigs mcfg
PLUGIN_GENERATED:= \
$(PLUGIN_DIR)/script.ml \
@@ -237,12 +238,12 @@ WP_API_BASE= \
MemoryContext.mli \
LogicUsage.mli RefUsage.mli \
normAtLabels.mli \
- wpPropId.mli mcfg.ml \
+ wpPropId.mli mcfg.mli \
Context.mli Warning.mli AssignsCompleteness.mli wpContext.mli \
Lang.mli Repr.mli Passive.mli Splitter.mli \
LogicBuiltins.mli Definitions.mli \
Cint.mli Cfloat.mli Vset.mli Cstring.mli \
- Sigs.ml Mstate.mli Conditions.mli Filtering.mli \
+ Sigs.mli Mstate.mli Conditions.mli Filtering.mli \
Plang.mli Pcfg.mli Pcond.mli \
CodeSemantics.mli \
LogicCompiler.mli LogicSemantics.mli \
@@ -323,7 +324,7 @@ clean::
rm -f $(Wp_DIR)/share/install.cm*
$(Wp_DIR)/share/instwp: $(Wp_DIR)/share/install.ml
- $(OCAMLC) $(WARNINGS) -o $@ unix.cma $^
+ $(OCAMLC) $(WARNINGS) -w -70 -o $@ unix.cma $^
# --------------------------------------------------------------------------
# --- Pre-Compiled Coq Libraries ---
diff --git a/src/plugins/wp/Sigs.ml b/src/plugins/wp/Sigs.mli
similarity index 100%
rename from src/plugins/wp/Sigs.ml
rename to src/plugins/wp/Sigs.mli
diff --git a/src/plugins/wp/mcfg.ml b/src/plugins/wp/mcfg.mli
similarity index 100%
rename from src/plugins/wp/mcfg.ml
rename to src/plugins/wp/mcfg.mli
diff --git a/src/plugins/wp/register.ml b/src/plugins/wp/register.ml
index de651b862f8562d244218dabee2dba8dd3cb4a57..cd673ad5553ef608a18959dc17135fe8626d4443 100644
--- a/src/plugins/wp/register.ml
+++ b/src/plugins/wp/register.ml
@@ -22,30 +22,11 @@
let dkey_main = Wp_parameters.register_category "main"
let dkey_raised = Wp_parameters.register_category "raised"
-let wkey_smoke = Wp_parameters.register_warn_category "smoke"
(* ------------------------------------------------------------------------ *)
(* --- Memory Model Hypotheses --- *)
(* ------------------------------------------------------------------------ *)
-module Models = Set.Make(WpContext.MODEL)
-module Fmap = Kernel_function.Map
-
-let wp_iter_model ?ip ?index job =
- begin
- let pool : Models.t Fmap.t ref = ref Fmap.empty in
- Wpo.iter ?ip ?index ~on_goal:(fun wpo ->
- match Wpo.get_index wpo with
- | Wpo.Axiomatic _ -> ()
- | Wpo.Function(kf,_) ->
- let m = Wpo.get_model wpo in
- let ms = try Fmap.find kf !pool with Not_found -> Models.empty in
- if not (Models.mem m ms) then
- pool := Fmap.add kf (Models.add m ms) !pool ;
- ) () ;
- Fmap.iter (fun kf ms -> Models.iter (fun m -> job kf m) ms) !pool
- end
-
let wp_compute_memory_context model =
let hypotheses_computer = WpContext.compute_hypotheses model in
let name = WpContext.MODEL.id model in
@@ -136,12 +117,6 @@ let pp_warnings fmt wpo =
| false , _ -> Format.fprintf fmt " (Stronger, %d warnings)" n
end
-let launch task =
- let server = ProverTask.server () in
- (** Do on_server_stop save why3 session *)
- Task.spawn server (Task.thread task) ;
- Task.launch server
-
(* ------------------------------------------------------------------------ *)
(* --- Prover Stats --- *)
(* ------------------------------------------------------------------------ *)
@@ -755,21 +730,6 @@ let cmdline_run () =
end
end
-(* ------------------------------------------------------------------------ *)
-(* --- Register external functions --- *)
-(* ------------------------------------------------------------------------ *)
-
-let deprecated name =
- Wp_parameters.warning ~once:true ~current:false
- "Dynamic '%s' now is deprecated. Use `Wp.VC` api instead." name
-
-let register name ty code =
- let _ignore =
- Dynamic.register ~plugin:"Wp" name ty
- ~journalize:false (*LC: Because of Property is not journalizable. *)
- (fun x -> deprecated name ; code x)
- in ()
-
(* ------------------------------------------------------------------------ *)
(* --- Tracing WP Invocation --- *)
(* ------------------------------------------------------------------------ *)
diff --git a/src/plugins/qed/QedGui.ml b/src/plugins/wp/register.mli
similarity index 94%
rename from src/plugins/qed/QedGui.ml
rename to src/plugins/wp/register.mli
index 40db8a1c9750d4c5ba4d950adc1fbc5628140596..5ad2762fc1e77744ec9704c0ef2e23c0570206cc 100644
--- a/src/plugins/qed/QedGui.ml
+++ b/src/plugins/wp/register.mli
@@ -20,4 +20,5 @@
(* *)
(**************************************************************************)
-(* Fake Module for Frama-C / Gui *)
+val do_wp_proofs:
+ ?provers:Why3.Whyconf.prover list -> ?tip:bool -> Wpo.t Bag.t -> unit
diff --git a/src/plugins/wp/tests/inexistant-prover b/src/plugins/wp/tests/inexistant-prover
deleted file mode 100644
index e69de29bb2d1d6434b8b29ae775ad8c2e48c5391..0000000000000000000000000000000000000000
diff --git a/src/plugins/wp/tests/wp_bts/issue_143.i b/src/plugins/wp/tests/wp_bts/issue_143.i
deleted file mode 100644
index 555cbcb5b0889741e7ebe50de2d0713662fb9934..0000000000000000000000000000000000000000
--- a/src/plugins/wp/tests/wp_bts/issue_143.i
+++ /dev/null
@@ -1,22 +0,0 @@
-/* run.config
- DONTRUN:
-*/
-/* run.config_qualif
- EXECNOW: chmod a-x ./tests/inexistant-prover
- OPT: -wp
- OPT: -wp -wp-prover "alt-ergo,native:coq" -wp-alt-ergo ./tests/inexistant-prover -wp-coqc ./tests/inexistant-prover
- OPT: -wp -wp-prover "alt-ergo" -wp-alt-ergo ./tests/inexistant-prover
- OPT: -wp -wp-prover "native:coq" -wp-coqc ./tests/inexistant-prover
-*/
-
-/*@
- axiomatic A {
- lemma ok_because_inconsistent: \forall integer x; x > 0 ==> x < 0 ==> x == 0 ;
- }
-*/
-
-/*@
- axiomatic B {
- lemma ok_because_consistent: \forall integer x; x > 0 ==> x*x > 0 ;
- }
-*/
diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_143.0.res.oracle b/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_143.0.res.oracle
deleted file mode 100644
index 9d615ddd682dd47aa3bb673b79d3b40cb090cb74..0000000000000000000000000000000000000000
--- a/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_143.0.res.oracle
+++ /dev/null
@@ -1,14 +0,0 @@
-# frama-c -wp [...]
-[kernel] Parsing tests/wp_bts/issue_143.i (no preprocessing)
-[wp] Running WP plugin...
-[wp] 2 goals scheduled
-[wp] [Alt-Ergo] Goal typed_lemma_ok_because_consistent : Valid
-[wp] [Alt-Ergo] Goal typed_lemma_ok_because_inconsistent : Valid
-[wp] Proved goals: 2 / 2
- Qed: 0
- Alt-Ergo: 2
-------------------------------------------------------------
- Axiomatics WP Alt-Ergo Total Success
- Axiomatic A - 1 1 100%
- Axiomatic B - 1 1 100%
-------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_143.1.res.oracle b/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_143.1.res.oracle
deleted file mode 100644
index 08841f4f3a5743e7882829ae4b5b2530c704ef60..0000000000000000000000000000000000000000
--- a/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_143.1.res.oracle
+++ /dev/null
@@ -1,15 +0,0 @@
-# frama-c -wp [...]
-[kernel] Parsing tests/wp_bts/issue_143.i (no preprocessing)
-[wp] Running WP plugin...
-[wp] Warning: native support for coq is deprecated, use tip instead
-[wp] 2 goals scheduled
-[wp] [Alt-Ergo] Goal typed_lemma_ok_because_consistent : Valid
-[wp] [Alt-Ergo] Goal typed_lemma_ok_because_inconsistent : Valid
-[wp] Proved goals: 2 / 2
- Qed: 0
- Alt-Ergo: 2
-------------------------------------------------------------
- Axiomatics WP Alt-Ergo Total Success
- Axiomatic A - 1 1 100%
- Axiomatic B - 1 1 100%
-------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_143.2.res.oracle b/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_143.2.res.oracle
deleted file mode 100644
index 9d615ddd682dd47aa3bb673b79d3b40cb090cb74..0000000000000000000000000000000000000000
--- a/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_143.2.res.oracle
+++ /dev/null
@@ -1,14 +0,0 @@
-# frama-c -wp [...]
-[kernel] Parsing tests/wp_bts/issue_143.i (no preprocessing)
-[wp] Running WP plugin...
-[wp] 2 goals scheduled
-[wp] [Alt-Ergo] Goal typed_lemma_ok_because_consistent : Valid
-[wp] [Alt-Ergo] Goal typed_lemma_ok_because_inconsistent : Valid
-[wp] Proved goals: 2 / 2
- Qed: 0
- Alt-Ergo: 2
-------------------------------------------------------------
- Axiomatics WP Alt-Ergo Total Success
- Axiomatic A - 1 1 100%
- Axiomatic B - 1 1 100%
-------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_143.3.res.oracle b/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_143.3.res.oracle
deleted file mode 100644
index 376255d0dcbdd0874f047745de334d291a25548a..0000000000000000000000000000000000000000
--- a/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_143.3.res.oracle
+++ /dev/null
@@ -1,17 +0,0 @@
-# frama-c -wp [...]
-[kernel] Parsing tests/wp_bts/issue_143.i (no preprocessing)
-[wp] Running WP plugin...
-[wp] Warning: native support for coq is deprecated, use tip instead
-[wp] 2 goals scheduled
-[wp] [Coq (native)] Goal typed_lemma_ok_because_consistent : Failed
- Command './tests/inexistant-prover' not found
-[wp] [Coq] Goal typed_lemma_ok_because_inconsistent : Default tactic
-[wp] [Coq (native)] Goal typed_lemma_ok_because_inconsistent : Failed
- Command './tests/inexistant-prover' not found
-[wp] Proved goals: 0 / 2
- Coq (native): 0 (failed: 2)
-------------------------------------------------------------
- Axiomatics WP Alt-Ergo Total Success
- Axiomatic A - - 1 0.0%
- Axiomatic B - - 1 0.0%
-------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/config.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/config.res.oracle
index d1903f4234f1308657d5768f5132525318f1bb6d..8262db901edcbcaff5e750ec62f8b2abc6e3b159 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/config.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/config.res.oracle
@@ -3,5 +3,5 @@ WP Requirements for Qualif Tests (3)
----------------------------------------------------------
1. The Alt-Ergo theorem prover, version 2.2.0
2. The Why3 platform, version 1.4.0
-3. The Coq Proof Assistant, version 8.12.0
+3. The Coq Proof Assistant, version 8.13.0
----------------------------------------------------------