Merge pull request #1349 from goblint/apron_cleanup

Remove intermediate module definition in `AffineEqualityAnalysis`

src/analyses/apron/affineEqualityAnalysis.apron.ml

@@ -9,16 +9,10 @@ include RelationAnalysis
 let spec_module: (module MCPSpec) Lazy.t =
   lazy (
     let module AD = AffineEqualityDomain.D2 (VectorMatrix.ArrayVector) (VectorMatrix.ArrayMatrix) in
-    let module RD: RelationDomain.RD =
-    struct
-      module V = AffineEqualityDomain.V
-      include AD
-    end
-    in
     let module Priv = (val RelationPriv.get_priv ()) in
     let module Spec =
     struct
-      include SpecFunctor (Priv) (RD) (RelationPrecCompareUtil.DummyUtil)
+      include SpecFunctor (Priv) (AD) (RelationPrecCompareUtil.DummyUtil)
       let name () = "affeq"
     end
     in

src/analyses/apron/apronAnalysis.apron.ml

@@ -9,18 +9,11 @@ let spec_module: (module MCPSpec) Lazy.t =
     let module Man = (val ApronDomain.get_manager ()) in
     let module AD = ApronDomain.D2 (Man) in
     let diff_box = GobConfig.get_bool "ana.apron.invariant.diff-box" in
-    let module AD = (val if diff_box then (module ApronDomain.BoxProd (AD): ApronDomain.S3) else (module AD)) in
-    let module RD: RelationDomain.RD =
-    struct
-      module V = ApronDomain.V
-      include AD
-      type var = Apron.Var.t
-    end
-    in
+    let module AD = (val if diff_box then (module ApronDomain.BoxProd (AD): RelationDomain.RD) else (module AD)) in
     let module Priv = (val RelationPriv.get_priv ()) in
     let module Spec =
     struct
-      include SpecFunctor (Priv) (RD) (ApronPrecCompareUtil.Util)
+      include SpecFunctor (Priv) (AD) (ApronPrecCompareUtil.Util)
       let name () = "apron"
     end
     in

src/cdomains/apron/affineEqualityDomain.apron.ml

@@ -26,8 +26,6 @@ module Mpqf = struct
   let hash x = 31 * (Z.hash (get_den x)) + Z.hash (get_num x)
 end
 
-module V = RelationDomain.V
-
 (** It defines the type t of the affine equality domain (a struct that contains an optional matrix and an apron environment) and provides the functions needed for handling variables (which are defined by RelationDomain.D2) such as add_vars remove_vars.
     Furthermore, it provides the function get_coeff_vec that parses an apron expression into a vector of coefficients if the apron expression has an affine form. *)
 module VarManagement (Vec: AbstractVector) (Mx: AbstractMatrix)=
@@ -240,7 +238,7 @@ struct
   include VarManagement (Vc) (Mx)
 
   module Bounds = ExpressionBounds (Vc) (Mx)
-
+  module V = RelationDomain.V
   module Convert = SharedFunctions.Convert (V) (Bounds) (struct let allow_global = true end) (SharedFunctions.Tracked)
 
   type var = V.t
@@ -703,9 +701,9 @@ struct
   let unmarshal t = t
 end
 
-module D2(Vc: AbstractVector) (Mx: AbstractMatrix): RelationDomain.S3 with type var = Var.t =
+module D2(Vc: AbstractVector) (Mx: AbstractMatrix): RelationDomain.RD with type var = Var.t =
 struct
   module D =  D (Vc) (Mx)
-  include SharedFunctions.AssertionModule (V) (D)
+  include SharedFunctions.AssertionModule (D.V) (D)
   include D
 end

src/cdomains/apron/apronDomain.apron.ml

@@ -779,6 +779,7 @@ module type S2 =
 (* TODO: ExS3 or better extend RelationDomain.S3 directly?*)
 sig
   module Man: Manager
+  module V: RV
   include module type of AOps (Tracked) (Man)
   include SLattice with type t = Man.mt A.t
 
@@ -803,6 +804,7 @@ sig
   include SLattice
   include AOps with type t := t
 
+  module V: RV
   module Tracked: RelationDomain.Tracked
 
   val assert_inv : t -> exp -> bool -> bool Lazy.t -> t
@@ -813,6 +815,7 @@ end
 module D2 (Man: Manager) : S2 with module Man = Man  =
 struct
   include D (Man)
+  module V = RelationDomain.V
 
   type marshal = OctagonD.marshal
 
@@ -926,8 +929,10 @@ struct
     |> Lincons1Set.elements
 end
 
-module BoxProd (D: S3): S3 =
+module BoxProd (D: S3): RD =
 struct
+  module V = D.V
+  type var = V.t
   module BP0 = BoxProd0 (D)
   module Tracked = SharedFunctions.Tracked
   include BP0

src/cdomains/apron/relationDomain.apron.ml

@@ -128,7 +128,6 @@ end
 module type S3 =
 sig
   include S2
-
   val cil_exp_of_lincons1: Lincons1.t -> exp option
   val invariant: t -> Lincons1.t list
 end