From 942139878b8fed98ec95fc00a49ef40a2f0bba07 Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Tue, 9 Aug 2022 16:14:59 +0200
Subject: [PATCH] [build] add landmarks
---
dune-workspace | 9 +++++++++
src/dune | 1 +
src/init/boot/dune | 1 +
src/init/dune | 1 +
src/init/impl_cmdline/dune | 1 +
src/plugins/aorai/dune | 1 +
src/plugins/callgraph/dune | 1 +
src/plugins/constant_propagation/dune | 1 +
src/plugins/dive/dune | 1 +
src/plugins/e-acsl/src/dune | 4 +++-
src/plugins/eva/dune | 12 ++++++++----
src/plugins/from/dune | 1 +
src/plugins/impact/dune | 1 +
src/plugins/inout/dune | 1 +
src/plugins/instantiate/dune | 1 +
src/plugins/loop_analysis/dune | 1 +
src/plugins/markdown-report/dune | 1 +
src/plugins/markdown-report/eva-info/dune | 1 +
src/plugins/metrics/dune | 1 +
src/plugins/nonterm/dune | 1 +
src/plugins/obfuscator/dune | 1 +
src/plugins/occurrence/dune | 1 +
src/plugins/pdg/dune | 1 +
src/plugins/postdominators/dune | 1 +
src/plugins/qed/dune | 3 ++-
src/plugins/reduc/dune | 1 +
src/plugins/report/dune | 1 +
src/plugins/rte/dune | 1 +
src/plugins/scope/dune | 1 +
src/plugins/security_slicing/dune | 1 +
src/plugins/server/dune | 1 +
src/plugins/slicing/dune | 1 +
src/plugins/sparecode/dune | 1 +
src/plugins/studia/dune | 1 +
src/plugins/users/dune | 1 +
src/plugins/variadic/dune | 1 +
src/plugins/wp/dune | 3 ++-
37 files changed, 56 insertions(+), 7 deletions(-)
create mode 100644 dune-workspace
diff --git a/dune-workspace b/dune-workspace
new file mode 100644
index 00000000000..6597fe31901
--- /dev/null
+++ b/dune-workspace
@@ -0,0 +1,9 @@
+(lang dune 2.8)
+(context default)
+(context
+ (default
+ (name bench)
+ (instrument_with landmarks)
+ (env
+ (_ (env-vars ("OCAML_LANDMARKS" "auto")))))
+)
diff --git a/src/dune b/src/dune
index 0b2e2272e22..5d6871a6b48 100644
--- a/src/dune
+++ b/src/dune
@@ -47,6 +47,7 @@
(foreign_stubs (language c) (names c_bindings))
(flags :standard -w -9)
(libraries frama-c.init str unix zarith ocamlgraph dynlink bytes yojson menhirLib dune-site dune-site.plugins)
+ (instrumentation (backend landmarks))
(preprocess (staged_pps ppx_import ppx_deriving.eq))
)
diff --git a/src/init/boot/dune b/src/init/boot/dune
index 7c0e0f2ba77..99571de6546 100644
--- a/src/init/boot/dune
+++ b/src/init/boot/dune
@@ -26,6 +26,7 @@
(modules boot)
(flags :standard -open Frama_c_kernel)
(libraries frama_c_kernel)
+ (instrumentation (backend landmarks))
)
diff --git a/src/init/dune b/src/init/dune
index 034e06a38dc..9187a431dcf 100644
--- a/src/init/dune
+++ b/src/init/dune
@@ -26,6 +26,7 @@
(modules frama_c_init gui_init)
(virtual_modules gui_init)
(libraries threads)
+ (instrumentation (backend landmarks))
)
(include_subdirs no)
diff --git a/src/init/impl_cmdline/dune b/src/init/impl_cmdline/dune
index b00afdb0599..7e8d680abd9 100644
--- a/src/init/impl_cmdline/dune
+++ b/src/init/impl_cmdline/dune
@@ -24,4 +24,5 @@
(name frama_c_very_first_cmdline)
(public_name frama-c.init.cmdline)
(implements frama-c.init)
+ (instrumentation (backend landmarks))
)
diff --git a/src/plugins/aorai/dune b/src/plugins/aorai/dune
index 61c4765284b..8c8a1eba331 100644
--- a/src/plugins/aorai/dune
+++ b/src/plugins/aorai/dune
@@ -44,6 +44,7 @@
( -> aorai_eva_analysis.disabled.ml)
)
)
+ (instrumentation (backend landmarks))
)
(ocamllex yalexer)
diff --git a/src/plugins/callgraph/dune b/src/plugins/callgraph/dune
index 93c3504f362..b1ad818441d 100644
--- a/src/plugins/callgraph/dune
+++ b/src/plugins/callgraph/dune
@@ -36,6 +36,7 @@
(public_name frama-c-callgraph.core)
(flags -open Frama_c_kernel :standard -w -9)
(libraries frama-c.kernel frama-c-eva.core)
+ (instrumentation (backend landmarks))
)
(plugin (optional) (name callgraph) (libraries frama-c-callgraph.core) (site (frama-c plugins)))
diff --git a/src/plugins/constant_propagation/dune b/src/plugins/constant_propagation/dune
index 8f76e14ccbb..048101730ad 100644
--- a/src/plugins/constant_propagation/dune
+++ b/src/plugins/constant_propagation/dune
@@ -36,6 +36,7 @@
(public_name frama-c-constant_propagation.core)
(flags -open Frama_c_kernel :standard -w -9)
(libraries frama-c.kernel frama-c-eva.core)
+ (instrumentation (backend landmarks))
)
(plugin (optional) (name constant_propagation) (libraries frama-c-constant_propagation.core) (site (frama-c plugins)))
diff --git a/src/plugins/dive/dune b/src/plugins/dive/dune
index 3a9b8c63973..85e0415bdd0 100644
--- a/src/plugins/dive/dune
+++ b/src/plugins/dive/dune
@@ -37,6 +37,7 @@
(public_name frama-c-dive.core)
(flags -open Frama_c_kernel :standard -w -9)
(libraries frama-c.kernel frama-c-studia.core frama-c-server.core)
+ (instrumentation (backend landmarks))
)
(plugin (optional) (name dive) (libraries frama-c-dive.core) (site (frama-c plugins)))
diff --git a/src/plugins/e-acsl/src/dune b/src/plugins/e-acsl/src/dune
index 94c58fa5089..ee4a92ec604 100644
--- a/src/plugins/e-acsl/src/dune
+++ b/src/plugins/e-acsl/src/dune
@@ -35,7 +35,9 @@
(optional)
(public_name frama-c-e-acsl.core)
(flags -open Frama_c_kernel :standard -w -9)
- (libraries frama-c.kernel frama-c-rtegen.core))
+ (libraries frama-c.kernel frama-c-rtegen.core)
+ (instrumentation (backend landmarks))
+)
(plugin (optional) (name e-acsl) (libraries frama-c-e-acsl.core) (site (frama-c plugins)))
diff --git a/src/plugins/eva/dune b/src/plugins/eva/dune
index 844043f7d38..6877dfd4327 100644
--- a/src/plugins/eva/dune
+++ b/src/plugins/eva/dune
@@ -39,7 +39,8 @@
(optional)
(public_name frama-c-eva.core)
(flags -open Frama_c_kernel :standard -w -9 -alert -db_deprecated)
- (libraries frama-c.kernel frama-c-server.core))
+ (libraries frama-c.kernel frama-c-server.core)
+ (instrumentation (backend landmarks)))
(plugin
(name eva)
@@ -56,7 +57,8 @@
(optional)
(public_name frama-c-eva.gui)
(flags -open Frama_c_kernel -open Frama_c_gui -open Eva__Private :standard -w -9 -alert -db_deprecated)
- (libraries eva frama-c.kernel frama-c.gui)))
+ (libraries eva frama-c.kernel frama-c.gui)
+ (instrumentation (backend landmarks))))
(plugin
(name eva-gui)
@@ -71,7 +73,8 @@
(optional)
(public_name frama-c-eva.numerors.core)
(flags -open Frama_c_kernel -open Eva__Private :standard)
- (libraries frama-c.kernel frama-c-eva.core mlmpfr)))
+ (libraries frama-c.kernel frama-c-eva.core mlmpfr)
+ (instrumentation (backend landmarks))))
(plugin
(name eva.numerors)
@@ -88,7 +91,8 @@
(flags -open Frama_c_kernel -open Eva__Private :standard -w -9)
(libraries
frama-c.kernel frama-c-eva.core
- apron.octMPQ apron.boxMPQ apron.polkaMPQ apron.apron)))
+ apron.octMPQ apron.boxMPQ apron.polkaMPQ apron.apron)
+ (instrumentation (backend landmarks))))
(plugin
(name eva.apron)
diff --git a/src/plugins/from/dune b/src/plugins/from/dune
index 256d8410d51..649a080ec4f 100644
--- a/src/plugins/from/dune
+++ b/src/plugins/from/dune
@@ -38,6 +38,7 @@
(public_name frama-c-from.core)
(flags -open Frama_c_kernel :standard -w -9)
(libraries frama-c.kernel frama-c-callgraph.core frama-c-eva.core frama-c-postdominators.core)
+ (instrumentation (backend landmarks))
)
(plugin (optional) (name from) (libraries frama-c-from.core) (site (frama-c plugins)))
diff --git a/src/plugins/impact/dune b/src/plugins/impact/dune
index 5fec8c58fef..8bd94fb0581 100644
--- a/src/plugins/impact/dune
+++ b/src/plugins/impact/dune
@@ -40,6 +40,7 @@
(public_name frama-c-impact.core)
(flags -open Frama_c_kernel :standard -w -9)
(libraries frama-c.kernel frama-c-pdg.core frama-c-slicing.core frama-c-callgraph.core frama-c-inout.core)
+ (instrumentation (backend landmarks))
)
(plugin (optional) (name impact) (libraries frama-c-impact.core) (site (frama-c plugins)))
diff --git a/src/plugins/inout/dune b/src/plugins/inout/dune
index e43b239a3f8..1029fd27994 100644
--- a/src/plugins/inout/dune
+++ b/src/plugins/inout/dune
@@ -38,6 +38,7 @@
(public_name frama-c-inout.core)
(flags -open Frama_c_kernel :standard -w -9)
(libraries frama-c.kernel frama-c-callgraph.core frama-c-eva.core frama-c-from.core)
+ (instrumentation (backend landmarks))
)
(plugin (optional) (name inout) (libraries frama-c-inout.core) (site (frama-c plugins)))
diff --git a/src/plugins/instantiate/dune b/src/plugins/instantiate/dune
index a39dc1bfc23..61f0edbbea3 100644
--- a/src/plugins/instantiate/dune
+++ b/src/plugins/instantiate/dune
@@ -35,6 +35,7 @@
(public_name frama-c-instantiate.core)
(flags -open Frama_c_kernel :standard -w -9)
(libraries frama-c.kernel)
+ (instrumentation (backend landmarks))
)
(plugin (optional) (name instantiate) (libraries frama-c-instantiate.core) (site (frama-c plugins)))
diff --git a/src/plugins/loop_analysis/dune b/src/plugins/loop_analysis/dune
index d28c2300bce..178b00973e5 100644
--- a/src/plugins/loop_analysis/dune
+++ b/src/plugins/loop_analysis/dune
@@ -37,6 +37,7 @@
(private_modules region_analysis_sig region_analysis region_analysis_stmt loop_analysis register)
(flags -open Frama_c_kernel :standard)
(libraries frama-c.kernel frama-c-eva.core)
+ (instrumentation (backend landmarks))
)
(plugin (optional) (name loop-analysis) (libraries frama-c-loop-analysis.core) (site (frama-c plugins)))
diff --git a/src/plugins/markdown-report/dune b/src/plugins/markdown-report/dune
index dee6ca9c600..d09f7742970 100644
--- a/src/plugins/markdown-report/dune
+++ b/src/plugins/markdown-report/dune
@@ -37,6 +37,7 @@
(flags -open Frama_c_kernel :standard -w -9)
(libraries frama-c.kernel)
(preprocess (pps ppx_deriving_yojson))
+ (instrumentation (backend landmarks))
)
(plugin (optional) (name markdown-report) (libraries frama-c-markdown-report.core) (site (frama-c plugins)))
diff --git a/src/plugins/markdown-report/eva-info/dune b/src/plugins/markdown-report/eva-info/dune
index 809265f042b..9d6d8395828 100644
--- a/src/plugins/markdown-report/eva-info/dune
+++ b/src/plugins/markdown-report/eva-info/dune
@@ -38,6 +38,7 @@
(flags -open Frama_c_kernel :standard -w -9)
(libraries frama-c.kernel frama-c-eva.core frama-c-markdown-report.core)
(preprocess (pps ppx_deriving_yojson))
+ (instrumentation (backend landmarks))
)
(plugin (optional) (name markdown-report.eva-info) (libraries frama-c-markdown-report.eva-info.core) (site (frama-c plugins)))
diff --git a/src/plugins/metrics/dune b/src/plugins/metrics/dune
index 208dbcdff2e..04d94b06704 100644
--- a/src/plugins/metrics/dune
+++ b/src/plugins/metrics/dune
@@ -37,6 +37,7 @@
(public_name frama-c-metrics.core)
(flags -open Frama_c_kernel :standard -w -9)
(libraries frama-c.kernel frama-c-eva.core frama-c-server.core)
+ (instrumentation (backend landmarks))
)
(plugin (optional) (name metrics) (libraries frama-c-metrics.core) (site (frama-c plugins)))
diff --git a/src/plugins/nonterm/dune b/src/plugins/nonterm/dune
index 6e0713eba1a..b2273574bbb 100644
--- a/src/plugins/nonterm/dune
+++ b/src/plugins/nonterm/dune
@@ -36,6 +36,7 @@
(public_name frama-c-nonterm.core)
(flags -open Frama_c_kernel :standard -w -9)
(libraries frama-c.kernel frama-c-eva.core)
+ (instrumentation (backend landmarks))
)
(plugin (optional) (name nonterm) (libraries frama-c-nonterm.core) (site (frama-c plugins)))
diff --git a/src/plugins/obfuscator/dune b/src/plugins/obfuscator/dune
index d62c751fc66..94ea79b5e98 100644
--- a/src/plugins/obfuscator/dune
+++ b/src/plugins/obfuscator/dune
@@ -35,6 +35,7 @@
(public_name frama-c-obfuscator.core)
(flags -open Frama_c_kernel :standard -w -9)
(libraries frama-c.kernel)
+ (instrumentation (backend landmarks))
)
(plugin (optional) (name obfuscator) (libraries frama-c-obfuscator.core) (site (frama-c plugins)))
diff --git a/src/plugins/occurrence/dune b/src/plugins/occurrence/dune
index b43409ba9a6..e7364f769a2 100644
--- a/src/plugins/occurrence/dune
+++ b/src/plugins/occurrence/dune
@@ -36,6 +36,7 @@
(public_name frama-c-occurrence.core)
(flags -open Frama_c_kernel :standard -w -9)
(libraries frama-c.kernel frama-c-eva.core)
+ (instrumentation (backend landmarks))
)
(plugin (optional) (name occurrence) (libraries frama-c-occurrence.core) (site (frama-c plugins)))
diff --git a/src/plugins/pdg/dune b/src/plugins/pdg/dune
index 0f38d0cc791..863c56b6e2d 100644
--- a/src/plugins/pdg/dune
+++ b/src/plugins/pdg/dune
@@ -39,6 +39,7 @@
(public_name frama-c-pdg.core)
(flags -open Frama_c_kernel :standard -w -9)
(libraries frama-c.kernel frama-c-pdg.types.core frama-c-callgraph.core frama-c-from.core frama-c-eva.core)
+ (instrumentation (backend landmarks))
)
(plugin (optional) (name pdg) (libraries frama-c-pdg.core) (site (frama-c plugins)))
diff --git a/src/plugins/postdominators/dune b/src/plugins/postdominators/dune
index c8e9604aebf..78bb8e11e3e 100644
--- a/src/plugins/postdominators/dune
+++ b/src/plugins/postdominators/dune
@@ -36,6 +36,7 @@
(public_name frama-c-postdominators.core)
(flags -open Frama_c_kernel :standard -w -9)
(libraries frama-c.kernel frama-c-eva.core)
+ (instrumentation (backend landmarks))
)
(plugin (optional) (name postdominators) (libraries frama-c-postdominators.core) (site (frama-c plugins)))
diff --git a/src/plugins/qed/dune b/src/plugins/qed/dune
index 0ff85904577..2bac3d85858 100644
--- a/src/plugins/qed/dune
+++ b/src/plugins/qed/dune
@@ -32,4 +32,5 @@
(optional)
(public_name qed)
(flags (-open Frama_c_kernel :standard -w -9))
- (libraries frama-c.kernel zarith))
+ (libraries frama-c.kernel zarith)
+ (instrumentation (backend landmarks)))
diff --git a/src/plugins/reduc/dune b/src/plugins/reduc/dune
index a58cacadc52..d9506548768 100644
--- a/src/plugins/reduc/dune
+++ b/src/plugins/reduc/dune
@@ -37,6 +37,7 @@
(public_name frama-c-reduc.core)
(flags -open Frama_c_kernel :standard -w -9)
(libraries frama-c.kernel frama-c-inout.core frama-c-eva.core)
+ (instrumentation (backend landmarks))
)
(plugin (optional) (name reduc) (libraries frama-c-reduc.core) (site (frama-c plugins)))
diff --git a/src/plugins/report/dune b/src/plugins/report/dune
index c924241c026..e0d6da73438 100644
--- a/src/plugins/report/dune
+++ b/src/plugins/report/dune
@@ -36,6 +36,7 @@
(private_modules report_parameters scan dump csv register classify)
(flags -open Frama_c_kernel :standard -w -9)
(libraries frama-c.kernel)
+ (instrumentation (backend landmarks))
)
(plugin (optional) (name report) (libraries frama-c-report.core) (site (frama-c plugins)))
diff --git a/src/plugins/rte/dune b/src/plugins/rte/dune
index 71ef5f3f99e..d2ef8a04f8c 100644
--- a/src/plugins/rte/dune
+++ b/src/plugins/rte/dune
@@ -36,6 +36,7 @@
(private_modules api options generator rte visit register)
(flags -open Frama_c_kernel :standard -w -9)
(libraries frama-c.kernel)
+ (instrumentation (backend landmarks))
)
(plugin (optional) (name rtegen) (libraries frama-c-rtegen.core) (site (frama-c plugins)))
diff --git a/src/plugins/scope/dune b/src/plugins/scope/dune
index aa8515905f1..874c095e96c 100644
--- a/src/plugins/scope/dune
+++ b/src/plugins/scope/dune
@@ -38,6 +38,7 @@
(public_name frama-c-scope.core)
(flags -open Frama_c_kernel :standard -w -9)
(libraries frama-c.kernel frama-c-eva.core frama-c-inout.core frama-c-pdg.core)
+ (instrumentation (backend landmarks))
)
(plugin (optional) (name scope) (libraries frama-c-scope.core) (site (frama-c plugins)))
diff --git a/src/plugins/security_slicing/dune b/src/plugins/security_slicing/dune
index 0e391460dfc..e214e44e80c 100644
--- a/src/plugins/security_slicing/dune
+++ b/src/plugins/security_slicing/dune
@@ -37,6 +37,7 @@
(public_name frama-c-security_slicing.core)
(flags -open Frama_c_kernel :standard -w -9)
(libraries frama-c.kernel frama-c-eva.core frama-c-pdg.core)
+ (instrumentation (backend landmarks))
)
(plugin (optional) (name security_slicing) (libraries frama-c-security_slicing.core) (site (frama-c plugins)))
diff --git a/src/plugins/server/dune b/src/plugins/server/dune
index 090fa0b58b4..685cbacd179 100644
--- a/src/plugins/server/dune
+++ b/src/plugins/server/dune
@@ -40,6 +40,7 @@
(zmq -> server_zmq.ok.ml)
( -> server_zmq.ko.ml)
))
+ (instrumentation (backend landmarks))
)
(plugin (optional) (name server) (libraries frama-c-server.core) (site (frama-c plugins)))
diff --git a/src/plugins/slicing/dune b/src/plugins/slicing/dune
index 84ca95b36ce..a8c8753b107 100644
--- a/src/plugins/slicing/dune
+++ b/src/plugins/slicing/dune
@@ -37,6 +37,7 @@
(public_name frama-c-slicing.core)
(flags -open Frama_c_kernel :standard -w -9)
(libraries frama-c.kernel frama-c-pdg.core frama-c-sparecode.core)
+ (instrumentation (backend landmarks))
)
(plugin (optional) (name slicing) (libraries frama-c-slicing.core) (site (frama-c plugins)))
diff --git a/src/plugins/sparecode/dune b/src/plugins/sparecode/dune
index 50182a084b9..5764630f5cf 100644
--- a/src/plugins/sparecode/dune
+++ b/src/plugins/sparecode/dune
@@ -40,6 +40,7 @@
(private_modules sparecode_params globs spare_marks transform register)
(flags :standard -open Frama_c_kernel)
(libraries frama-c.kernel frama-c-users.core frama-c-eva.core frama-c-pdg.core frama-c-inout.core)
+ (instrumentation (backend landmarks))
)
(plugin (optional) (name sparecode) (libraries frama-c-sparecode.core) (site (frama-c plugins)))
diff --git a/src/plugins/studia/dune b/src/plugins/studia/dune
index f8f1ed280bd..841fcb9550f 100644
--- a/src/plugins/studia/dune
+++ b/src/plugins/studia/dune
@@ -36,6 +36,7 @@
(public_name frama-c-studia.core)
(flags -open Frama_c_kernel :standard)
(libraries frama-c.kernel frama-c-eva.core)
+ (instrumentation (backend landmarks))
)
(plugin (optional) (name studia) (libraries frama-c-studia.core) (site (frama-c plugins)))
diff --git a/src/plugins/users/dune b/src/plugins/users/dune
index 62e2d466446..0f48402beda 100644
--- a/src/plugins/users/dune
+++ b/src/plugins/users/dune
@@ -36,6 +36,7 @@
(public_name frama-c-users.core)
(flags -open Frama_c_kernel :standard)
(libraries frama-c.kernel frama-c-callgraph.core)
+ (instrumentation (backend landmarks))
)
(plugin (optional) (name users) (libraries frama-c-users.core) (site (frama-c plugins)))
diff --git a/src/plugins/variadic/dune b/src/plugins/variadic/dune
index f25e755bba7..fbd5f8dbde8 100644
--- a/src/plugins/variadic/dune
+++ b/src/plugins/variadic/dune
@@ -35,6 +35,7 @@
(public_name frama-c-variadic.core)
(flags -open Frama_c_kernel :standard -w -9)
(libraries frama-c.kernel)
+ (instrumentation (backend landmarks))
)
(plugin (optional) (name variadic) (libraries frama-c-variadic.core) (site (frama-c plugins)))
diff --git a/src/plugins/wp/dune b/src/plugins/wp/dune
index 37a17d61438..286e356130a 100644
--- a/src/plugins/wp/dune
+++ b/src/plugins/wp/dune
@@ -43,7 +43,8 @@
qed why3 zarith ocamlgraph
(select wp_eva.ml from
(frama-c-eva.core -> wp_eva.enabled.ml)
- ( -> wp_eva.disabled.ml))))
+ ( -> wp_eva.disabled.ml)))
+ (instrumentation (backend landmarks)))
(plugin (optional) (name wp) (libraries frama-c-wp.core) (site (frama-c plugins)))
--
GitLab