diff --git a/nix/frama-c.nix b/nix/frama-c.nix
index 31ecb0a1f1b3a969014fa89c00b3093d357f00f7..fa49766e55efef725e54c30bf93215d422e72d10 100644
--- a/nix/frama-c.nix
+++ b/nix/frama-c.nix
@@ -24,6 +24,7 @@
, mlmpfr
, ocaml
, ocamlgraph
+, ocamlgraph_gtk
, ppx_deriving
, ppx_deriving_yojson
, ppx_import
@@ -71,6 +72,7 @@ stdenvNoCC.mkDerivation rec {
mlmpfr
ocaml
ocamlgraph
+ ocamlgraph_gtk
ppx_deriving
ppx_deriving_yojson
ppx_import
diff --git a/src/plugins/aorai/dune b/src/plugins/aorai/dune
index 32c897cb7ea6cf63fbd4842c6e11c36a8da14033..f58f1a489e26b9ca1311abe662e7c5cfb4bbb147 100644
--- a/src/plugins/aorai/dune
+++ b/src/plugins/aorai/dune
@@ -1,3 +1,13 @@
+(rule
+ (alias frama-c-configure)
+ (deps (universe))
+ (action (progn
+ (echo "Aorai:" %{lib-available:frama-c-aorai.core} "\n")
+ (echo " - (optional) Eva:" %{lib-available:frama-c-eva.core} "\n")
+ )
+ )
+)
+
( library
(name aorai)
(public_name frama-c-aorai.core)
diff --git a/src/plugins/callgraph/callgraph.mli b/src/plugins/callgraph/callgraph.mli
index 6cb4ac6abb6ec76cc0d8283bfa86b19546868eef..175a4de16183527c9262b04efc96d80ba66ed6e9 100644
--- a/src/plugins/callgraph/callgraph.mli
+++ b/src/plugins/callgraph/callgraph.mli
@@ -23,11 +23,13 @@
(** Callgraph plugin. *)
module Options: sig
+ include Plugin.S
module Filename: Parameter_sig.Filepath
module Service_roots: Parameter_sig.Kernel_function_set
module Uncalled: Parameter_sig.Bool
module Uncalled_leaf: Parameter_sig.Bool
module Services: Parameter_sig.Bool
+ module Roots : Parameter_sig.Kernel_function_set
end
module Cg: module type of Cg
diff --git a/src/plugins/callgraph/dune b/src/plugins/callgraph/dune
index c4b119b08e65fd875a514d5eee8a62b9d986cf9b..6e54b6cbe74100c909aa268943aa04af553f9cc5 100644
--- a/src/plugins/callgraph/dune
+++ b/src/plugins/callgraph/dune
@@ -1,22 +1,18 @@
+(rule
+ (alias frama-c-configure)
+ (deps (universe))
+ (action (progn
+ (echo "Callgraph:" %{lib-available:frama-c-callgraph.core} "\n")
+ (echo " - Eva:" %{lib-available:frama-c-eva.core} "\n")
+ )
+ )
+)
+
( library
(name callgraph)
(public_name frama-c-callgraph.core)
- (modules Options Journalize Cg Services Uses Register Callgraph_api Callgraph Subgraph)
-; (private_modules Options Journalize Cg Uses Register)
(flags -open Frama_c_kernel :standard -w -9)
(libraries frama-c.kernel frama-c-eva.core)
)
(plugin (optional) (name callgraph) (libraries frama-c-callgraph.core) (site (frama-c plugins)))
-
-( library
- (name callgraph_gui)
- (public_name frama-c-callgraph.gui)
- (optional)
- (modules Cg_viewer)
-; (private_modules Cg_viewer)
- (flags -open Frama_c_kernel -open Frama_c_gui -open Callgraph :standard)
- (libraries callgraph frama-c.kernel frama-c.gui ocamlgraph.dgraph)
-)
-
-(plugin (optional) (name callgraph) (libraries frama-c-callgraph.gui) (site (frama-c plugins_gui)))
diff --git a/src/plugins/callgraph/cg_viewer.ml b/src/plugins/callgraph/gui/cg_viewer.ml
similarity index 99%
rename from src/plugins/callgraph/cg_viewer.ml
rename to src/plugins/callgraph/gui/cg_viewer.ml
index 7885f9f43dab46a5e8934f5633c4168bfb423d79..c3f460858deff77aa07ad0e1f66bd5dfce731a7c 100644
--- a/src/plugins/callgraph/cg_viewer.ml
+++ b/src/plugins/callgraph/gui/cg_viewer.ml
@@ -20,7 +20,7 @@
(* *)
(**************************************************************************)
-open DGRAPH_MODULE
+open Graph.S
let ($) f x = f x
diff --git a/src/plugins/callgraph/cg_viewer.mli b/src/plugins/callgraph/gui/cg_viewer.mli
similarity index 100%
rename from src/plugins/callgraph/cg_viewer.mli
rename to src/plugins/callgraph/gui/cg_viewer.mli
diff --git a/src/plugins/callgraph/gui/dune b/src/plugins/callgraph/gui/dune
new file mode 100644
index 0000000000000000000000000000000000000000..6e322df4b31d990ad512c56d5f4a4d708fee5d3d
--- /dev/null
+++ b/src/plugins/callgraph/gui/dune
@@ -0,0 +1,28 @@
+(rule
+ (alias frama-c-configure)
+ (deps (universe))
+ (action (progn
+ (echo "Callgraph GUI:" %{lib-available:frama-c-callgraph.gui} "\n")
+ (echo " - Frama-C GUI:" %{lib-available:frama-c.gui} "\n")
+ (echo " - Callgraph:" %{lib-available:frama-c-callgraph.core} "\n")
+ (echo " - Ocamlgraph_gtk:" %{lib-available:ocamlgraph_gtk} "\n")
+ (echo " - Ocamlgraph Dgraph:" %{lib-available:ocamlgraph.dgraph} "\n")
+ )
+ )
+)
+
+( library
+ (name callgraph_gui)
+ (public_name frama-c-callgraph.gui)
+ (optional)
+ (flags -open Frama_c_kernel -open Frama_c_gui -open Callgraph :standard -w -9)
+ (libraries
+ frama-c.kernel frama-c.gui frama-c-callgraph.core
+ (select graph.ml from
+ (ocamlgraph.dgraph -> graph.dgraph.ml)
+ (ocamlgraph_gtk -> graph.gtk.ml)
+ )
+ )
+)
+
+(plugin (optional) (name callgraph-gui) (libraries frama-c-callgraph.gui) (site (frama-c plugins_gui)))
diff --git a/src/plugins/callgraph/gui/graph.dgraph.ml b/src/plugins/callgraph/gui/graph.dgraph.ml
new file mode 100644
index 0000000000000000000000000000000000000000..bddad430e95fa7b2af53e840cea3e2cf9d6e7aa2
--- /dev/null
+++ b/src/plugins/callgraph/gui/graph.dgraph.ml
@@ -0,0 +1 @@
+module S = Dgraph
diff --git a/src/plugins/callgraph/gui/graph.gtk.ml b/src/plugins/callgraph/gui/graph.gtk.ml
new file mode 100644
index 0000000000000000000000000000000000000000..699872d749365dc2175f1bd2debef14e7ddd2b87
--- /dev/null
+++ b/src/plugins/callgraph/gui/graph.gtk.ml
@@ -0,0 +1 @@
+module S = Graph_gtk
diff --git a/src/plugins/constant_propagation/dune b/src/plugins/constant_propagation/dune
index 8a790f823343c49d7e53ed4ca55294d89eab91f2..b9b677a4a8653b1ce368e91ceef88044e85355b1 100644
--- a/src/plugins/constant_propagation/dune
+++ b/src/plugins/constant_propagation/dune
@@ -1,3 +1,13 @@
+(rule
+ (alias frama-c-configure)
+ (deps (universe))
+ (action (progn
+ (echo "Constant Propagation:" %{lib-available:frama-c-constant_propagation.core} "\n")
+ (echo " - Eva:" %{lib-available:frama-c-eva.core} "\n")
+ )
+ )
+)
+
( library
(name Constant_Propagation)
(public_name frama-c-constant_propagation.core)
diff --git a/src/plugins/dive/dune b/src/plugins/dive/dune
index d1dd9bd48ebe47c630bcdb16482fbb5e51d401a2..c161bc03e536a9ca5766f7d3d3353108cc038111 100644
--- a/src/plugins/dive/dune
+++ b/src/plugins/dive/dune
@@ -1,3 +1,14 @@
+(rule
+ (alias frama-c-configure)
+ (deps (universe))
+ (action (progn
+ (echo "Dive:" %{lib-available:frama-c-dive.core} "\n")
+ (echo " - Studia:" %{lib-available:frama-c-studia.core} "\n")
+ (echo " - Server:" %{lib-available:frama-c-server.core} "\n")
+ )
+ )
+)
+
( library
(name dive)
(public_name frama-c-dive.core)
diff --git a/src/plugins/e-acsl/src/dune b/src/plugins/e-acsl/src/dune
index 1be5622aaa95f24df367dbd58048e82790510e63..2b14fb84aac448d13533399f106a03022f455ddf 100644
--- a/src/plugins/e-acsl/src/dune
+++ b/src/plugins/e-acsl/src/dune
@@ -1,3 +1,12 @@
+(rule
+ (alias frama-c-configure)
+ (deps (universe))
+ (action (progn
+ (echo "E-ACSL:" %{lib-available:frama-c-e-acsl.core} "\n")
+ )
+ )
+)
+
(library
(name E_ACSL)
(public_name frama-c-e-acsl.core)
diff --git a/src/plugins/from/dune b/src/plugins/from/dune
index 7d1942b794b58501b763e0dc3a24e2da816279de..e355e70e3ace5ccc27666eefcb3b161746ef0a48 100644
--- a/src/plugins/from/dune
+++ b/src/plugins/from/dune
@@ -3,6 +3,9 @@
(deps (universe))
(action (progn
(echo "From:" %{lib-available:frama-c-from.core} "\n")
+ (echo " - Callgraph:" %{lib-available:frama-c-callgraph.core} "\n")
+ (echo " - Eva:" %{lib-available:frama-c-eva.core} "\n")
+ (echo " - Postdominators:" %{lib-available:frama-c-postdominators.core} "\n")
)
)
)
diff --git a/src/plugins/impact/dune b/src/plugins/impact/dune
index 50da6c3d60e3dd5dfebfc4aaed3c6b9a96de05f1..341ebf7b8202b22746c13ad1eec45e14f224681b 100644
--- a/src/plugins/impact/dune
+++ b/src/plugins/impact/dune
@@ -1,3 +1,16 @@
+(rule
+ (alias frama-c-configure)
+ (deps (universe))
+ (action (progn
+ (echo "Impact:" %{lib-available:frama-c-impact.core} "\n")
+ (echo " - Callgraph:" %{lib-available:frama-c-callgraph.core} "\n")
+ (echo " - Slicing:" %{lib-available:frama-c-slicing.core} "\n")
+ (echo " - Inout:" %{lib-available:frama-c-inout.core} "\n")
+ )
+ )
+)
+
+
( library
(name impact)
(public_name frama-c-impact.core)
diff --git a/src/plugins/inout/dune b/src/plugins/inout/dune
index eedb6e2fbfd600b548b2bac642d30928b9a56e49..a0795192acf0373a656a0a3882dbbfc070693e0a 100644
--- a/src/plugins/inout/dune
+++ b/src/plugins/inout/dune
@@ -1,3 +1,15 @@
+(rule
+ (alias frama-c-configure)
+ (deps (universe))
+ (action (progn
+ (echo "Inout:" %{lib-available:frama-c-inout.core} "\n")
+ (echo " - Callgraph:" %{lib-available:frama-c-callgraph.core} "\n")
+ (echo " - Eva:" %{lib-available:frama-c-eva.core} "\n")
+ (echo " - From:" %{lib-available:frama-c-from.core} "\n")
+ )
+ )
+)
+
( library
(name inout)
(public_name frama-c-inout.core)
diff --git a/src/plugins/instantiate/dune b/src/plugins/instantiate/dune
index 1e0ab048901bd5bb3cffc38bd2eb01bfe5966b52..855f71317f3524df0abe47c789c1f9fa82243b8f 100644
--- a/src/plugins/instantiate/dune
+++ b/src/plugins/instantiate/dune
@@ -1,3 +1,12 @@
+(rule
+ (alias frama-c-configure)
+ (deps (universe))
+ (action (progn
+ (echo "Instantiate:" %{lib-available:frama-c-instantiate.core} "\n")
+ )
+ )
+)
+
( library
(name instantiate)
(public_name frama-c-instantiate.core)
diff --git a/src/plugins/loop_analysis/dune b/src/plugins/loop_analysis/dune
index 6883b813274e2c81f1d98a5baa37a183fc442f84..b7023aab4712b0a5822d9e46cfec2d2982d7f2d1 100644
--- a/src/plugins/loop_analysis/dune
+++ b/src/plugins/loop_analysis/dune
@@ -1,7 +1,16 @@
+(rule
+ (alias frama-c-configure)
+ (deps (universe))
+ (action (progn
+ (echo "Loop-Analysis:" %{lib-available:frama-c-loop-analysis.core} "\n")
+ (echo " - Eva:" %{lib-available:frama-c-eva.core} "\n")
+ )
+ )
+)
+
( library
(name LoopAnalysis)
(public_name frama-c-loop-analysis.core)
- (modules options region_analysis_sig region_analysis region_analysis_stmt loop_analysis register LoopAnalysis)
(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)
diff --git a/src/plugins/metrics/dune b/src/plugins/metrics/dune
index 18609c7e6971dca3a2b25030a7a5ecc315df974d..9d4deca66b4275bc8d548d778c75582d99714f68 100644
--- a/src/plugins/metrics/dune
+++ b/src/plugins/metrics/dune
@@ -1,22 +1,19 @@
+(rule
+ (alias frama-c-configure)
+ (deps (universe))
+ (action (progn
+ (echo "Metrics:" %{lib-available:frama-c-metrics.core} "\n")
+ (echo " - Eva:" %{lib-available:frama-c-eva.core} "\n")
+ (echo " - Server:" %{lib-available:frama-c-server.core} "\n")
+ )
+ )
+)
+
( library
(name metrics)
(public_name frama-c-metrics.core)
- (modules metrics metrics_parameters css_html metrics_base metrics_acsl
- metrics_cabs metrics_cilast metrics_coverage
- register)
(flags -open Frama_c_kernel :standard -w -9)
(libraries frama-c.kernel frama-c-eva.core frama-c-server.core)
)
(plugin (optional) (name metrics) (libraries frama-c-metrics.core) (site (frama-c plugins)))
-
-( library
- (name metrics_gui)
- (public_name frama-c-metrics.gui)
- (optional)
- (modules metrics_gui_panels register_gui)
- (flags -open Frama_c_kernel -open Frama_c_gui -open Metrics :standard -w -9)
- (libraries metrics frama-c.kernel frama-c.gui)
-)
-
-(plugin (optional) (name metrics) (libraries frama-c-metrics.gui) (site (frama-c plugins_gui)))
diff --git a/src/plugins/metrics/gui/dune b/src/plugins/metrics/gui/dune
new file mode 100644
index 0000000000000000000000000000000000000000..b65c898ff9c56ea6ffb2e7e19b1be277db495901
--- /dev/null
+++ b/src/plugins/metrics/gui/dune
@@ -0,0 +1,9 @@
+( library
+ (name metrics_gui)
+ (public_name frama-c-metrics.gui)
+ (optional)
+ (flags -open Frama_c_kernel -open Frama_c_gui -open Metrics :standard -w -9)
+ (libraries frama-c.kernel frama-c.gui frama-c-metrics.core)
+)
+
+(plugin (optional) (name metrics-gui) (libraries frama-c-metrics.gui) (site (frama-c plugins_gui)))
diff --git a/src/plugins/metrics/metrics_gui_panels.ml b/src/plugins/metrics/gui/metrics_gui_panels.ml
similarity index 100%
rename from src/plugins/metrics/metrics_gui_panels.ml
rename to src/plugins/metrics/gui/metrics_gui_panels.ml
diff --git a/src/plugins/metrics/metrics_gui_panels.mli b/src/plugins/metrics/gui/metrics_gui_panels.mli
similarity index 100%
rename from src/plugins/metrics/metrics_gui_panels.mli
rename to src/plugins/metrics/gui/metrics_gui_panels.mli
diff --git a/src/plugins/metrics/register_gui.ml b/src/plugins/metrics/gui/register_gui.ml
similarity index 100%
rename from src/plugins/metrics/register_gui.ml
rename to src/plugins/metrics/gui/register_gui.ml
diff --git a/src/plugins/metrics/register_gui.mli b/src/plugins/metrics/gui/register_gui.mli
similarity index 100%
rename from src/plugins/metrics/register_gui.mli
rename to src/plugins/metrics/gui/register_gui.mli
diff --git a/src/plugins/nonterm/dune b/src/plugins/nonterm/dune
index 957d8c944d3c843a08d0db5b1dc2a125d8996038..567480f1dead559e16e8cce9dd4c36de3e1406f4 100644
--- a/src/plugins/nonterm/dune
+++ b/src/plugins/nonterm/dune
@@ -1,3 +1,13 @@
+(rule
+ (alias frama-c-configure)
+ (deps (universe))
+ (action (progn
+ (echo "NonTerm:" %{lib-available:frama-c-nonterm.core} "\n")
+ (echo " - Eva:" %{lib-available:frama-c-eva.core} "\n")
+ )
+ )
+)
+
( library
(name nonterm)
(public_name frama-c-nonterm.core)
diff --git a/src/plugins/obfuscator/dune b/src/plugins/obfuscator/dune
index 15334ae210e72257a075ff10fdcfe912a4ddb355..6bab90b1ec57723938674c4b3c8e5ae3fe302759 100644
--- a/src/plugins/obfuscator/dune
+++ b/src/plugins/obfuscator/dune
@@ -1,3 +1,12 @@
+(rule
+ (alias frama-c-configure)
+ (deps (universe))
+ (action (progn
+ (echo "Obfuscator:" %{lib-available:frama-c-obfuscator.core} "\n")
+ )
+ )
+)
+
( library
(name obfuscator)
(public_name frama-c-obfuscator.core)
diff --git a/src/plugins/occurrence/Occurrence.ml b/src/plugins/occurrence/Occurrence.ml
index 451f7f806e3b46459c96df360cb88bd081663135..d7961a9f07fe6ce58ced320bd71862a8d8609fd7 100644
--- a/src/plugins/occurrence/Occurrence.ml
+++ b/src/plugins/occurrence/Occurrence.ml
@@ -36,6 +36,12 @@ module Register: sig
val print_all: (unit -> unit)
(** Print all the occurrence of each variable declarations. *)
+
+ (* {2 Internal Use Only}*)
+
+ type access_type = Read | Write | Both
+
+ val classify_accesses: kernel_function option * kinstr *lval -> access_type
end = Register
(*
diff --git a/src/plugins/occurrence/dune b/src/plugins/occurrence/dune
index 53b96ae805fd962e5a687414307b7734c82fb804..032769c4025c79080348719aa083d9903f3cbaf7 100644
--- a/src/plugins/occurrence/dune
+++ b/src/plugins/occurrence/dune
@@ -1,20 +1,18 @@
+(rule
+ (alias frama-c-configure)
+ (deps (universe))
+ (action (progn
+ (echo "Occurrence:" %{lib-available:frama-c-occurrence.core} "\n")
+ (echo " - Eva:" %{lib-available:frama-c-eva.core} "\n")
+ )
+ )
+)
+
( library
(name occurrence)
- (public_name frama-c-occurrence.core)
- (modules options register)
+ (public_name frama-c-occurrence.core)
(flags -open Frama_c_kernel :standard -w -9)
(libraries frama-c.kernel frama-c-eva.core)
)
(plugin (optional) (name occurrence) (libraries frama-c-occurrence.core) (site (frama-c plugins)))
-
-( library
- (name occurrence_gui)
- (public_name frama-c-occurrence.gui)
- (optional)
- (modules register_gui)
- (flags -open Frama_c_kernel -open Frama_c_gui -open Occurrence :standard -w -9)
- (libraries occurrence frama-c.kernel frama-c.gui)
-)
-
-(plugin (optional) (name occurrence) (libraries frama-c-occurrence.gui) (site (frama-c plugins_gui)))
diff --git a/src/plugins/occurrence/gui/dune b/src/plugins/occurrence/gui/dune
new file mode 100644
index 0000000000000000000000000000000000000000..f2fe4f573f6c0bc8b6d2670e4d2a5dae4de705c1
--- /dev/null
+++ b/src/plugins/occurrence/gui/dune
@@ -0,0 +1,20 @@
+(rule
+ (alias frama-c-configure)
+ (deps (universe))
+ (action (progn
+ (echo "Occurrence GUI:" %{lib-available:frama-c-occurrence.gui} "\n")
+ (echo " - Frama-C GUI:" %{lib-available:frama-c.gui} "\n")
+ (echo " - Occurrence:" %{lib-available:frama-c-occurrence.core} "\n")
+ )
+ )
+)
+
+( library
+ (name occurrence_gui)
+ (public_name frama-c-occurrence.gui)
+ (optional)
+ (flags -open Frama_c_kernel -open Frama_c_gui -open Occurrence :standard -w -9)
+ (libraries frama-c.kernel frama-c.gui frama-c-occurrence.core)
+)
+
+(plugin (optional) (name occurrence) (libraries frama-c-occurrence.gui) (site (frama-c plugins_gui)))
diff --git a/src/plugins/occurrence/register_gui.ml b/src/plugins/occurrence/gui/register_gui.ml
similarity index 100%
rename from src/plugins/occurrence/register_gui.ml
rename to src/plugins/occurrence/gui/register_gui.ml
diff --git a/src/plugins/occurrence/register_gui.mli b/src/plugins/occurrence/gui/register_gui.mli
similarity index 100%
rename from src/plugins/occurrence/register_gui.mli
rename to src/plugins/occurrence/gui/register_gui.mli
diff --git a/src/plugins/pdg/dune b/src/plugins/pdg/dune
index 1e9523549c5c25d56186f4100eead94946b69982..af7a614abc8c23ca915949729e914cd1936f083a 100644
--- a/src/plugins/pdg/dune
+++ b/src/plugins/pdg/dune
@@ -3,6 +3,9 @@
(deps (universe))
(action (progn
(echo "PDG:" %{lib-available:frama-c-pdg.core} "\n")
+ (echo " - Callgraph:" %{lib-available:frama-c-callgraph.core} "\n")
+ (echo " - Eva:" %{lib-available:frama-c-eva.core} "\n")
+ (echo " - From:" %{lib-available:frama-c-from.core} "\n")
)
)
)
diff --git a/src/plugins/postdominators/dune b/src/plugins/postdominators/dune
index cef2bbaa639ee6eff0df5420147f08b3fa5510a0..3dfd1bf662cf6998c6e735514f1ad908c607ca51 100644
--- a/src/plugins/postdominators/dune
+++ b/src/plugins/postdominators/dune
@@ -1,3 +1,13 @@
+(rule
+ (alias frama-c-configure)
+ (deps (universe))
+ (action (progn
+ (echo "Postdominators:" %{lib-available:frama-c-postdominators.core} "\n")
+ (echo " - Eva:" %{lib-available:frama-c-eva.core} "\n")
+ )
+ )
+)
+
( library
(name postdominators)
(public_name frama-c-postdominators.core)
diff --git a/src/plugins/qed/dune b/src/plugins/qed/dune
index e0b6b678474f7f4383b14b7f031747e39b3f84de..edd33d5fe328ec84973b1d520cf7fd6193e0d8ae 100644
--- a/src/plugins/qed/dune
+++ b/src/plugins/qed/dune
@@ -1,3 +1,13 @@
+(rule
+ (alias frama-c-configure)
+ (deps (universe))
+ (action (progn
+ (echo "Qed:" %{lib-available:qed} "\n")
+ (echo " - Zarith:" %{lib-available:zarith} "\n")
+ )
+ )
+)
+
(library
(name qed)
(public_name qed)
diff --git a/src/plugins/reduc/dune b/src/plugins/reduc/dune
index d78631cb2e67812edd266260ad5a4c0f4c351f56..b0acc0cdf6e62da14dea109ce868868a4af4bf0c 100644
--- a/src/plugins/reduc/dune
+++ b/src/plugins/reduc/dune
@@ -3,6 +3,8 @@
(deps (universe))
(action (progn
(echo "Reduc:" %{lib-available:frama-c-reduc.core} "\n")
+ (echo " - Eva:" %{lib-available:frama-c-eva.core} "\n")
+ (echo " - Inout:" %{lib-available:frama-c-inout.core} "\n")
)
)
)
diff --git a/src/plugins/report/dune b/src/plugins/report/dune
index f936d1327216d43b471616f722e94b5cc074337e..7603b287637db4d39a243bfec3e73adc1c685d9f 100644
--- a/src/plugins/report/dune
+++ b/src/plugins/report/dune
@@ -1,7 +1,15 @@
+(rule
+ (alias frama-c-configure)
+ (deps (universe))
+ (action (progn
+ (echo "Report:" %{lib-available:frama-c-report.core} "\n")
+ )
+ )
+)
+
( library
(name report)
(public_name frama-c-report.core)
- (modules report_parameters scan dump csv register classify Report)
(private_modules report_parameters scan dump csv register classify)
(flags -open Frama_c_kernel :standard -w -9)
(libraries frama-c.kernel)
diff --git a/src/plugins/rte/dune b/src/plugins/rte/dune
index 0298b35ffeec6e2c9c95463a711675858c09a9a2..157d278dfa3947f2ca864d5d7b0ae371674f8b3f 100644
--- a/src/plugins/rte/dune
+++ b/src/plugins/rte/dune
@@ -1,3 +1,12 @@
+(rule
+ (alias frama-c-configure)
+ (deps (universe))
+ (action (progn
+ (echo "Rtegen:" %{lib-available:frama-c-rtegen.core} "\n")
+ )
+ )
+)
+
(library
(name RteGen)
(public_name frama-c-rtegen.core)
diff --git a/src/plugins/scope/dune b/src/plugins/scope/dune
index 46f1dcdb2bed8053903ed15e817770791c9aab68..32465234efb7ee0750ffcc5186aaefc12dd9ad16 100644
--- a/src/plugins/scope/dune
+++ b/src/plugins/scope/dune
@@ -1,19 +1,19 @@
+(rule
+ (alias frama-c-configure)
+ (deps (universe))
+ (action (progn
+ (echo "Scope:" %{lib-available:frama-c-scope.core} "\n")
+ (echo " - Eva:" %{lib-available:frama-c-eva.core} "\n")
+ (echo " - Inout:" %{lib-available:frama-c-inout.core} "\n")
+ )
+ )
+)
+
(library
(name scope)
(public_name frama-c-scope.core)
- (modules scope datascope zones defs)
(flags -open Frama_c_kernel :standard -w -9)
(libraries frama-c.kernel frama-c-eva.core frama-c-inout.core)
)
-(library
- (name scope_gui)
- (public_name frama-c-scope.gui)
- (optional)
- (modules dpds_gui)
- (flags -open Frama_c_kernel -open Frama_c_gui -open Scope :standard -w -9)
- (libraries frama-c.kernel frama-c.gui frama-c-scope.core)
-)
-
(plugin (optional) (name scope) (libraries frama-c-scope.core) (site (frama-c plugins)))
-(plugin (optional) (name scope) (libraries frama-c-scope.gui) (site (frama-c plugins_gui)))
diff --git a/src/plugins/scope/dpds_gui.ml b/src/plugins/scope/gui/dpds_gui.ml
similarity index 100%
rename from src/plugins/scope/dpds_gui.ml
rename to src/plugins/scope/gui/dpds_gui.ml
diff --git a/src/plugins/scope/dpds_gui.mli b/src/plugins/scope/gui/dpds_gui.mli
similarity index 100%
rename from src/plugins/scope/dpds_gui.mli
rename to src/plugins/scope/gui/dpds_gui.mli
diff --git a/src/plugins/scope/gui/dune b/src/plugins/scope/gui/dune
new file mode 100644
index 0000000000000000000000000000000000000000..0b3f412525bb934336306e21294b132fdd26dd61
--- /dev/null
+++ b/src/plugins/scope/gui/dune
@@ -0,0 +1,20 @@
+(rule
+ (alias frama-c-configure)
+ (deps (universe))
+ (action (progn
+ (echo "Scope GUI:" %{lib-available:frama-c-scope.gui} "\n")
+ (echo " - Frama-C GUI:" %{lib-available:frama-c.gui} "\n")
+ (echo " - Scope:" %{lib-available:frama-c-scope.core} "\n")
+ )
+ )
+)
+
+(library
+ (name scope_gui)
+ (public_name frama-c-scope.gui)
+ (optional)
+ (flags -open Frama_c_kernel -open Frama_c_gui -open Scope :standard -w -9)
+ (libraries frama-c.kernel frama-c.gui frama-c-scope.core)
+)
+
+(plugin (optional) (name scope) (libraries frama-c-scope.gui) (site (frama-c plugins_gui)))
diff --git a/src/plugins/security_slicing/Security_slicing.ml b/src/plugins/security_slicing/Security_slicing.ml
index f2a7ec9e4cdbbf7c17255ba48cd6c9234804c63c..5de90590943e0b8c0bdb1ba58e32ad67b9583066 100644
--- a/src/plugins/security_slicing/Security_slicing.ml
+++ b/src/plugins/security_slicing/Security_slicing.ml
@@ -24,6 +24,11 @@
(** No function is directly exported: they are dynamically registered. *)
+(** {2 Internal use only} *)
+
+module Components = Components
+module Security_slicing_parameters = Security_slicing_parameters
+
(*
Local Variables:
compile-command: "make -C ../../.."
diff --git a/src/plugins/security_slicing/dune b/src/plugins/security_slicing/dune
index 141d22ca9dea76eb7fef23115d689fddca206888..18b641b6e8b24af3daea31314f76c6d6ea991d01 100644
--- a/src/plugins/security_slicing/dune
+++ b/src/plugins/security_slicing/dune
@@ -1,21 +1,18 @@
+(rule
+ (alias frama-c-configure)
+ (deps (universe))
+ (action (progn
+ (echo "Security Slicing:" %{lib-available:frama-c-security_slicing.core} "\n")
+ (echo " - Eva:" %{lib-available:frama-c-eva.core} "\n")
+ )
+ )
+)
+
( library
(name security_slicing)
- (public_name frama-c-security_slicing.core)
- (modules security_slicing_parameters components)
+ (public_name frama-c-security_slicing.core)
(flags -open Frama_c_kernel :standard -w -9)
(libraries frama-c.kernel frama-c-eva.core)
)
(plugin (optional) (name security_slicing) (libraries frama-c-security_slicing.core) (site (frama-c plugins)))
-
-
-( library
- (name security_slicing_gui)
- (public_name frama-c-security_slicing.gui)
- (optional)
- (modules register_gui)
- (flags -open Frama_c_kernel -open Frama_c_gui -open Security_slicing :standard -w -9)
- (libraries security_slicing frama-c.kernel frama-c.gui)
-)
-
-(plugin (optional) (name security_slicing) (libraries frama-c-security_slicing.gui) (site (frama-c plugins_gui)))
diff --git a/src/plugins/security_slicing/gui/dune b/src/plugins/security_slicing/gui/dune
new file mode 100644
index 0000000000000000000000000000000000000000..d6d853294b04efea63a674cffa315b5dcb94deb4
--- /dev/null
+++ b/src/plugins/security_slicing/gui/dune
@@ -0,0 +1,9 @@
+( library
+ (name security_slicing_gui)
+ (public_name frama-c-security_slicing.gui)
+ (optional)
+ (flags -open Frama_c_kernel -open Frama_c_gui -open Security_slicing :standard -w -9)
+ (libraries frama-c.kernel frama-c.gui frama-c-security_slicing.core)
+)
+
+(plugin (optional) (name security_slicing) (libraries frama-c-security_slicing.gui) (site (frama-c plugins_gui)))
diff --git a/src/plugins/security_slicing/register_gui.ml b/src/plugins/security_slicing/gui/register_gui.ml
similarity index 100%
rename from src/plugins/security_slicing/register_gui.ml
rename to src/plugins/security_slicing/gui/register_gui.ml
diff --git a/src/plugins/security_slicing/register_gui.mli b/src/plugins/security_slicing/gui/register_gui.mli
similarity index 100%
rename from src/plugins/security_slicing/register_gui.mli
rename to src/plugins/security_slicing/gui/register_gui.mli
diff --git a/src/plugins/server/dune b/src/plugins/server/dune
index 04f538b0158dc4f7e1eed3bb1fa3cfa336f7ea03..8a535d26c0bf1068da65f62ed2bea9bb793ce77d 100644
--- a/src/plugins/server/dune
+++ b/src/plugins/server/dune
@@ -1,3 +1,13 @@
+(rule
+ (alias frama-c-configure)
+ (deps (universe))
+ (action (progn
+ (echo "Server:" %{lib-available:frama-c-server.core} "\n")
+ (echo " - (optional) Zmq:" %{lib-available:zmq} "\n")
+ )
+ )
+)
+
( library
(name server)
(public_name frama-c-server.core)
diff --git a/src/plugins/slicing/dune b/src/plugins/slicing/dune
index 5b9653b1b2d1d91350c3a38f8359a8a0f12b8984..90c29eb8d57031638fa9798c955e396335347908 100644
--- a/src/plugins/slicing/dune
+++ b/src/plugins/slicing/dune
@@ -1,3 +1,14 @@
+(rule
+ (alias frama-c-configure)
+ (deps (universe))
+ (action (progn
+ (echo "Slicing:" %{lib-available:frama-c-slicing.core} "\n")
+ (echo " - Pdg:" %{lib-available:frama-c-pdg.core} "\n")
+ (echo " - Sparecode:" %{lib-available:frama-c-sparecode.core} "\n")
+ )
+ )
+)
+
( library
(name slicing)
(public_name frama-c-slicing.core)
diff --git a/src/plugins/sparecode/dune b/src/plugins/sparecode/dune
index 5728446da09aff4af62a73e0f6b4edf2352c1847..79af334305f82986a540f75d0ce876cd772c6bea 100644
--- a/src/plugins/sparecode/dune
+++ b/src/plugins/sparecode/dune
@@ -1,3 +1,16 @@
+(rule
+ (alias frama-c-configure)
+ (deps (universe))
+ (action (progn
+ (echo "Sparecode:" %{lib-available:frama-c-sparecode.core} "\n")
+ (echo " - Users:" %{lib-available:frama-c-users.core} "\n")
+ (echo " - Eva:" %{lib-available:frama-c-eva.core} "\n")
+ (echo " - Inout:" %{lib-available:frama-c-inout.core} "\n")
+ (echo " - Pdg:" %{lib-available:frama-c-pdg.core} "\n")
+ )
+ )
+)
+
(library
(name Sparecode)
(public_name frama-c-sparecode.core)
diff --git a/src/plugins/studia/Studia.ml b/src/plugins/studia/Studia.ml
index 4ccf8f0beffd6726f59a2b53b541500abbbbce42..b6ab1c545caf0a3bf41dd5f1175cb1cb2f890780 100644
--- a/src/plugins/studia/Studia.ml
+++ b/src/plugins/studia/Studia.ml
@@ -21,35 +21,41 @@
(**************************************************************************)
(** Computations of the statements that write a given memory zone. *)
-include (struct
- module Writes = Writes
- module Reads = Reads
-end : sig
- module Writes: sig
-
- (** Given an effect [e], something is directly modified by [e] (through an
- affectation, or through a call to a leaf function) if [direct] holds, and
- indirectly (through the effects of a call) otherwise. *)
- type effects = {
- direct: bool (** Direct affectation [lv = ...], or modification through
- a call to a leaf function. *);
- indirect: bool (** Modification inside the body of called function
- [f(...)]*);
- }
-
- val compute: Locations.Zone.t -> (Cil_types.stmt * effects) list
- (** [compute z] finds all the statements that modifies [z], and for each
- statement, indicates whether the modification is direct or indirect. *)
-
- end
-
- (** Computations of the statements that read a given memory zone. *)
- module Reads: sig
-
- val compute: Locations.Zone.t -> (Cil_types.stmt * Writes.effects) list
- (** [compute z] finds all the statements that read [z]. The [effects]
- information indicates whether the read occur on the given statement,
- or through an inner call for [Call] instructions. *)
-
- end
- end)
+include
+ (struct
+ module Writes = Writes
+ module Reads = Reads
+ end :
+ sig
+ module Writes: sig
+
+ (** Given an effect [e], something is directly modified by [e] (through an
+ affectation, or through a call to a leaf function) if [direct] holds, and
+ indirectly (through the effects of a call) otherwise. *)
+ type effects = {
+ direct: bool (** Direct affectation [lv = ...], or modification through
+ a call to a leaf function. *);
+ indirect: bool (** Modification inside the body of called function
+ [f(...)]*);
+ }
+
+ val compute: Locations.Zone.t -> (Cil_types.stmt * effects) list
+ (** [compute z] finds all the statements that modifies [z], and for each
+ statement, indicates whether the modification is direct or indirect. *)
+
+ end
+
+ (** Computations of the statements that read a given memory zone. *)
+ module Reads: sig
+
+ val compute: Locations.Zone.t -> (Cil_types.stmt * Writes.effects) list
+ (** [compute z] finds all the statements that read [z]. The [effects]
+ information indicates whether the read occur on the given statement,
+ or through an inner call for [Call] instructions. *)
+
+ end
+ end)
+
+(** {2 Internal use only} *)
+
+module Options = Options
diff --git a/src/plugins/studia/dune b/src/plugins/studia/dune
index fb00bf6405e9ba039eaccfeb304f2e98127fd6c2..0bcf683188eb5b8986ca319b433c105ed770c5f6 100644
--- a/src/plugins/studia/dune
+++ b/src/plugins/studia/dune
@@ -1,21 +1,18 @@
+(rule
+ (alias frama-c-configure)
+ (deps (universe))
+ (action (progn
+ (echo "Studia:" %{lib-available:frama-c-studia.core} "\n")
+ (echo " - Eva:" %{lib-available:frama-c-eva.core} "\n")
+ )
+ )
+)
+
( library
(name studia)
(public_name frama-c-studia.core)
- (modules options writes reads)
(flags -open Frama_c_kernel :standard)
(libraries frama-c.kernel frama-c-eva.core)
)
(plugin (optional) (name studia) (libraries frama-c-studia.core) (site (frama-c plugins)))
-
-
-( library
- (name studia_gui)
- (public_name frama-c-studia.gui)
- (optional)
- (modules studia_gui)
- (flags -open Frama_c_kernel -open Frama_c_gui -open Studia :standard -w -9)
- (libraries studia frama-c.kernel frama-c.gui frama-c-eva.gui)
-)
-
-(plugin (optional) (name studia) (libraries frama-c-studia.gui) (site (frama-c plugins_gui)))
diff --git a/src/plugins/studia/gui/dune b/src/plugins/studia/gui/dune
new file mode 100644
index 0000000000000000000000000000000000000000..5d79564ddb291d339a2a3d1aaa3f29a2829d16c9
--- /dev/null
+++ b/src/plugins/studia/gui/dune
@@ -0,0 +1,22 @@
+(rule
+ (alias frama-c-configure)
+ (deps (universe))
+ (action (progn
+ (echo "Studia GUI:" %{lib-available:frama-c-studia.gui} "\n")
+ (echo " - Frama-C GUI:" %{lib-available:frama-c.gui} "\n")
+ (echo " - Eva GUI:" %{lib-available:frama-c-eva.gui} "\n")
+ (echo " - Studia:" %{lib-available:frama-c-studia.core} "\n")
+
+ )
+ )
+)
+
+( library
+ (name studia_gui)
+ (public_name frama-c-studia.gui)
+ (optional)
+ (flags -open Frama_c_kernel -open Frama_c_gui -open Studia :standard -w -9)
+ (libraries frama-c.kernel frama-c.gui frama-c-eva.gui frama-c-studia.core)
+)
+
+(plugin (optional) (name studia-gui) (libraries frama-c-studia.gui) (site (frama-c plugins_gui)))
diff --git a/src/plugins/studia/studia_gui.ml b/src/plugins/studia/gui/studia_gui.ml
similarity index 100%
rename from src/plugins/studia/studia_gui.ml
rename to src/plugins/studia/gui/studia_gui.ml
diff --git a/src/plugins/studia/studia_gui.mli b/src/plugins/studia/gui/studia_gui.mli
similarity index 100%
rename from src/plugins/studia/studia_gui.mli
rename to src/plugins/studia/gui/studia_gui.mli
diff --git a/src/plugins/users/dune b/src/plugins/users/dune
index 1b310be7de99a6a657eb25e49ea3578f1f7cd014..3a7d60dac2449a64d4a559eaa505dbf05a69d64b 100644
--- a/src/plugins/users/dune
+++ b/src/plugins/users/dune
@@ -1,3 +1,13 @@
+(rule
+ (alias frama-c-configure)
+ (deps (universe))
+ (action (progn
+ (echo "Users:" %{lib-available:frama-c-users.core} "\n")
+ (echo " - Callgraph:" %{lib-available:frama-c-callgraph.core} "\n")
+ )
+ )
+)
+
(library
(name Users)
(public_name frama-c-users.core)
diff --git a/src/plugins/variadic/dune b/src/plugins/variadic/dune
index f874d815642d057af116b6298bd7ee4b4aaeab7e..58634469eddbd5a4cc2f722843449c73710a6d53 100644
--- a/src/plugins/variadic/dune
+++ b/src/plugins/variadic/dune
@@ -1,3 +1,12 @@
+(rule
+ (alias frama-c-configure)
+ (deps (universe))
+ (action (progn
+ (echo "Variadic:" %{lib-available:frama-c-variadic.core} "\n")
+ )
+ )
+)
+
( library
(name variadic)
(public_name frama-c-variadic.core)
diff --git a/src/plugins/wp/dune b/src/plugins/wp/dune
index cb1db2f1686434f2a6a03fe2c754a3c6108b2b76..6f1ec28f8e7a12bce7c84aa0e58eca17158dac51 100644
--- a/src/plugins/wp/dune
+++ b/src/plugins/wp/dune
@@ -3,7 +3,11 @@
(deps (universe))
(action (progn
(echo "WP:" %{lib-available:frama-c-wp.core} "\n")
- (echo " - why3:" %{lib-available:why3} "\n")
+ (echo " - Ocamlgraph:" %{lib-available:ocamlgraph} "\n")
+ (echo " - Qed:" %{lib-available:qed} "\n")
+ (echo " - Rtegen:" %{lib-available:frama-c-rtegen.core} "\n")
+ (echo " - Why3:" %{lib-available:why3} "\n")
+ (echo " - Zarith:" %{lib-available:zarith} "\n")
)
)
)