Merge branch 'feature/dune/mode-guis' into 'feature/bobot/jbuilder'

GUI organization and compilation

See merge request frama-c/frama-c!3764

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

src/plugins/security_slicing/dune

+(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)))

src/plugins/security_slicing/gui/dune

+( 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)))

src/plugins/server/dune

+(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)

src/plugins/slicing/dune

+(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)

src/plugins/sparecode/dune

+(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)

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

src/plugins/studia/dune

+(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)))

src/plugins/studia/gui/dune

+(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)))

src/plugins/users/dune

+(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)

src/plugins/variadic/dune

+(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)

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")
   )
   )
 )