Merge branch 'feature/eva/dune-simplify' into 'master'

[Eva] Simplifies dune file and removes the Private module from Eva.mli

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

.gitattributes

@@ -91,9 +91,7 @@ Make* header_spec=CEA_LGPL
 *.js header_spec=CEA_LGPL
 
 *.ml header_spec=CEA_LGPL
-*.ml.in header_spec=CEA_LGPL
 *.mli header_spec=CEA_LGPL
-*.mli.in header_spec=CEA_LGPL
 *.mll header_spec=CEA_LGPL
 *.mly header_spec=CEA_LGPL
 

.gitignore

@@ -208,7 +208,6 @@ Makefile.plugin.generated
 /src/plugins/gui/GSourceView.mli
 /src/plugins/gui/gtk_compat.ml
 /src/plugins/markdown-report/META
-/src/plugins/eva/Eva.mli
 
 # generated tar.gz files
 

src/plugins/eva/Eva.ml.in → src/plugins/eva/Eva.header

@@ -20,28 +20,19 @@
 (*                                                                        *)
 (**************************************************************************)
 
-module Private = struct
-  module Abstractions = Eva__Abstractions
-  module Analysis = Eva__Analysis
-  module Alarmset = Eva__Alarmset
-  module Parameters = Parameters
-  module Main_values = Eva__Main_values
-  module Eval = Eva__Eval
-  module Eval_terms = Eva__Eval_terms
-  module Eva_utils = Eva_utils
-  module Eva_results = Eva_results
-  module Self = Self
-  module Red_statuses = Eva__Red_statuses
-  module Abstract_value = Eva__Abstract_value
-  module Abstract_domain = Eva__Abstract_domain
-  module Active_behaviors = Active_behaviors
-  module Function_calls = Function_calls
-  module Simple_memory = Eva__Simple_memory
-  module Structure = Eva__Structure
-  module Eval_typ = Eva__Eval_typ
-  module Eval_op = Eva__Eval_op
-  module Domain_builder = Eva__Domain_builder
-  module Main_locations = Eva__Main_locations
-  module Eval_annots = Eva__Eval_annots
-  module Eva_dynamic = Eva_dynamic
-end
+(** Eva public API.
+
+    The main modules are:
+    - Analysis: run the analysis.
+    - Results: access analysis results, especially the values of expressions
+      and memory locations of lvalues at each program point.
+
+    The following modules allow configuring the Eva analysis:
+    - Parameters: change the configuration of the analysis.
+    - Eva_annotations: add local annotations to guide the analysis.
+    - Builtins: register ocaml builtins to be used by the cvalue domain
+      instead of analysing the body of some C functions.
+
+    Other modules are for internal use only. *)
+
+(* This file is generated. Do not edit. *)

src/plugins/eva/dune

@@ -23,186 +23,82 @@
 (rule
  (alias frama-c-configure)
  (deps (universe))
- (action (progn
-          (echo "EVA:" %{lib-available:frama-c-eva.core} "\n")
-          (echo "Numerors:" %{lib-available:frama-c-eva.numerors.core} "\n")
-          (echo " - MLMPFR:" %{lib-available:mlmpfr} "\n")
-          (echo "Apron domains:" %{lib-available:frama-c-eva.apron} "\n")
-          (echo " - apron.octMPQ:" %{lib-available:apron.octMPQ} "\n")
-          (echo " - apron.boxMPQ:" %{lib-available:apron.boxMPQ} "\n")
-          (echo " - apron.polkaMPQ:" %{lib-available:apron.polkaMPQ} "\n")
-          (echo " - apron.apron:" %{lib-available:apron.apron} "\n")
-  )
-  )
-)
+ (action
+  (progn
+   (echo "EVA:" %{lib-available:frama-c-eva.core} "\n")
+   (echo "Numerors:" %{lib-available:frama-c-eva.numerors.core} "\n")
+   (echo " - MLMPFR:" %{lib-available:mlmpfr} "\n")
+   (echo "Apron domains:" %{lib-available:frama-c-eva.apron} "\n")
+   (echo " - apron.octMPQ:" %{lib-available:apron.octMPQ} "\n")
+   (echo " - apron.boxMPQ:" %{lib-available:apron.boxMPQ} "\n")
+   (echo " - apron.polkaMPQ:" %{lib-available:apron.polkaMPQ} "\n")
+   (echo " - apron.apron:" %{lib-available:apron.apron} "\n"))))
 
-( library
-  (name eva)
-  (optional)
-  (public_name frama-c-eva.core)
-  (modules
-  abstract
-  abstract_domain
-  abstract_location
-  abstract_memory
-  abstract_offset
-  abstract_structure
-  abstract_value
-  abstractions
-  active_behaviors
-  alarmset
-  analysis
-  auto_loop_unroll
-  backward_formals
-  builtins
-  builtins_float
-  builtins_malloc
-  builtins_memory
-  builtins_misc
-  builtins_print_c
-  builtins_split
-  builtins_string
-  builtins_watchpoint
-  compute_functions
-  cvalue_backward
-  cvalue_callbacks
-  cvalue_domain
-  cvalue_forward
-  cvalue_init
-  cvalue_offsetmap
-  cvalue_specification
-  cvalue_transfer
-  domain_builder
-  domain_lift
-  domain_mode
-  domain_product
-  domain_store
-  equality
-  equality_domain
-  eva
-  eva_annotations
-  eva_audit
-  eva_dynamic
-  eva_perf
-  eva_results
-  eva_utils
-  eval
-  eval_annots
-  eval_op
-  eval_terms
-  eval_typ
-  evaluation
-  function_args
-  function_calls
-  gauges_domain
-  general_requests
-  hcexprs
-  initialization
-  inout_domain
-  iterator
-  library_functions
-  locals_scoping
-  location_lift
-  main_locations
-  main_values
-  mem_exec
-  multidim
-  multidim_domain
-  octagons
-  offsm_domain
-  offsm_value
-  parameters
-  partition
-  partitioning_index
-  partitioning_parameters
-  per_stmt_slevel
-  powerset
-  printer_domain
-  pretty_memory
-  recursion
-  red_statuses
-  register
-  results
-  segmentation
-  self
-  sign_domain
-  sign_value
-  simple_memory
-  simpler_domains
-  split_return
-  split_strategy
-  structure
-  subdivided_evaluation
-  summary
-  symbolic_locs
-  taint_domain
-  trace_partitioning
-  traces_domain
-  transfer_logic
-  transfer_specification
-  transfer_stmt
-  typed_memory
-  unit_domain
-  unit_tests
-  value_product
-  values_request
-  warn
-  widen
-  widen_hints_ext
-)
+(library
+ (name eva)
+ (optional)
+ (public_name frama-c-eva.core)
+ (flags -open Frama_c_kernel :standard -w -9)
+ (libraries frama-c.kernel frama-c-server.core))
 
-;  (public_interfaces (Eva))
-  (flags -open Frama_c_kernel :standard -w -9)
- (libraries frama-c.kernel frama-c-server.core
-            ; frama-c-callgraph.core frama-c-rtegen.core frama-c-loop-analysis.core
-            ; frama-c-scope.core
- )
-)
+(plugin
+ (name eva)
+ (optional)
+ (libraries frama-c-eva.core)
+ (site (frama-c plugins)))
 
-(plugin (optional) (name eva) (libraries frama-c-eva.core) (site (frama-c plugins)))
+(include_subdirs unqualified)
 
-(rule
-  (targets Eva.ml Eva.mli)
-  (deps
-    gen-api.sh Eva.ml.in Eva.mli.in
-    engine/analysis.mli utils/results.mli parameters.mli utils/eva_annotations.mli eval.mli
-    domains/cvalue/builtins.mli  utils/cvalue_callbacks.mli legacy/eval_terms.mli utils/eva_results.mli utils/unit_tests.mli
-  )
-  (action (run %{deps}))
-)
+(subdir gui (include_subdirs no))
+(subdir gui
+ (library
+  (name eva_gui)
+  (optional)
+  (public_name frama-c-eva.gui)
+  (flags -open Frama_c_kernel -open Frama_c_gui -open Eva__Private :standard -w -9)
+  (libraries eva frama-c.kernel frama-c.gui)))
+
+(plugin
+ (name eva-gui)
+ (optional)
+ (libraries frama-c-eva.gui)
+ (site (frama-c plugins_gui)))
 
-( library
+(subdir domains/numerors (include_subdirs no))
+(subdir domains/numerors
+ (library
   (name numerors)
-  (public_name frama-c-eva.numerors.core)
-  (flags -open Frama_c_kernel -open Eva.Private :standard)
-  (modules numerors_domain numerors_utils numerors_float numerors_interval numerors_arithmetics numerors_value)
-  (libraries frama-c.kernel frama-c-eva.core mlmpfr)
   (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)))
 
-(plugin (optional) (name eva.numerors) (libraries frama-c-eva.numerors.core) (site (frama-c plugins)))
+(plugin
+ (name eva.numerors)
+ (optional)
+ (libraries frama-c-eva.numerors.core)
+ (site (frama-c plugins)))
 
-( library
+(subdir domains/apron (include_subdirs no))
+(subdir domains/apron
+ (library
   (name apron_domain)
-  (public_name frama-c-eva.apron)
-  (flags -open Frama_c_kernel -open Eva.Private :standard -w -9)
-  (modules apron_domain)
-  (libraries frama-c.kernel frama-c-eva.core apron.octMPQ apron.boxMPQ apron.polkaMPQ apron.apron)
   (optional)
-)
+  (public_name frama-c-eva.apron)
+  (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)))
 
 ;(plugin (optional) (name eva-apron) (libraries frama-c-eva.apron) (site (frama-c plugins)))
 
-( library
-  (name eva_gui)
-  (public_name frama-c-eva.gui)
-  (optional)
-  (modules gui_callstacks_filters gui_callstacks_manager gui_eval gui_types register_gui gui_red)
-;  (public_interfaces ())
-  (flags -open Frama_c_kernel -open Frama_c_gui -open Eva -open Eva.Private :standard -w -9)
-  (libraries eva frama-c.kernel frama-c.gui)
-)
-
-(plugin (optional) (name eva-gui) (libraries frama-c-eva.gui) (site (frama-c plugins_gui)))
-
-(include_subdirs unqualified)
+(rule
+ (targets Eva.ml Eva.mli)
+ (mode (promote (only Eva.mli)))
+ (deps
+  gen-api.sh Eva.header
+  engine/analysis.mli utils/results.mli parameters.mli
+  utils/eva_annotations.mli eval.mli domains/cvalue/builtins.mli
+  utils/cvalue_callbacks.mli legacy/eval_terms.mli utils/eva_results.mli
+  utils/unit_tests.mli)
+ (action (run %{deps})))

src/plugins/eva/gen-api.sh

@@ -27,28 +27,11 @@ dir=$(dirname $0)
 
 # Generate MLI
 
-cat $dir/Eva.mli.in >> Eva.mli
-
-printf '\n(** Eva public API.
-
-   The main modules are:
-   - Analysis: run the analysis.
-   - Results: access analysis results, especially the values of expressions
-      and memory locations of lvalues at each program point.
-
-   The following modules allow configuring the Eva analysis:
-   - Parameters: change the configuration of the analysis.
-   - Eva_annotations: add local annotations to guide the analysis.
-   - Builtins: register ocaml builtins to be used by the cvalue domain
-       instead of analysing the body of some C functions.
-
-   Other modules are for internal use only. *)\n' >> Eva.mli
-
-printf '\n(* This file is generated. Do not edit. *)\n' >> Eva.mli
+cat $dir/Eva.header >> Eva.mli
 
 for i in "$@"
 do
-    if [[ ! "$i" =~ [.]in$ ]]; then
+    if [[ ! "$i" =~ [.]header$ ]]; then
         file=$(basename $i)
         module=${file%.*}
         Module="$(echo "${module:0:1}" | tr '[:lower:]' '[:upper:]')${module:1}"
@@ -60,11 +43,11 @@ done
 
 # Generate ML
 
-cat $dir/Eva.ml.in >> Eva.ml
+cat $dir/Eva.header >> Eva.ml
 
 for i in "$@"
 do
-    if [[ ! "$i" =~ [.]in$ ]]; then
+    if [[ ! "$i" =~ [.]header$ ]]; then
         file=$(basename $i)
         module=${file%.*}
         Module="$(echo "${module:0:1}" | tr '[:lower:]' '[:upper:]')${module:1}"