Add V module to Spec for global constraint variables (issue #469)

src/analyses/apron/apronAnalysis.apron.ml

@@ -18,6 +18,7 @@ struct
   module C = D
 
   open AD
+  open (ApronDomain: (sig module V: (module type of ApronDomain.V) end)) (* open only V from ApronDomain (to shadow V of Spec), but don't open D (to not shadow D here) *)
 
   open ApronPrecCompareUtil
   (* Result map used for comparison of results *)

src/analyses/mCP.ml

@@ -9,7 +9,8 @@ module QuerySet = Set.Make (Queries.Any)
 type spec_modules = { spec : (module MCPSpec)
                     ; dom  : (module Lattice.S)
                     ; glob : (module Lattice.S)
-                    ; cont : (module Printable.S) }
+                    ; cont : (module Printable.S)
+                    ; var  : (module Printable.S) }
 
 let analyses_list  : (int * spec_modules) list ref = ref []
 let analyses_list' : (int * spec_modules) list ref = ref []
@@ -25,6 +26,7 @@ let register_analysis =
             ; dom  = (module S.D : Lattice.S)
             ; glob = (module S.G : Lattice.S)
             ; cont = (module S.C : Printable.S)
+            ; var  = (module S.V : Printable.S)
             }
     in
     let n = S.name () in
@@ -217,14 +219,22 @@ struct
   let domain_list () = List.map (fun (n,p) -> n, p.cont) !analyses_list
 end
 
+module VarListSpec : DomainListPrintableSpec =
+struct
+  let assoc_dom n = (List.assoc n !analyses_list).var
+  let domain_list () = List.map (fun (n,p) -> n, p.var) !analyses_list
+end
+
 module MCP2 : Analyses.Spec
   with module D = DomListLattice (LocalDomainListSpec)
    and module G = DomListLattice (GlobalDomainListSpec)
-   and module C = DomListPrintable (ContextListSpec) =
+   and module C = DomListPrintable (ContextListSpec)
+   and module V = DomListPrintable (VarListSpec) =
 struct
   module D = DomListLattice (LocalDomainListSpec)
   module G = DomListLattice (GlobalDomainListSpec)
   module C = DomListPrintable (ContextListSpec)
+  module V = DomListPrintable (VarListSpec)
 
   open List open Obj
 

src/framework/analyses.ml

@@ -316,6 +316,7 @@ sig
   module D : Lattice.S
   module G : Lattice.S
   module C : Printable.S
+  module V: Printable.S (** Global constraint variables. *)
 
   val name : unit -> string
 
@@ -487,10 +488,13 @@ struct
     BatPrintf.fprintf f "<context>\n%a</context>\n%a" C.printXml c D.printXml d
 end
 
+module VarinfoV = CilType.Varinfo
 
 (** Relatively safe default implementations of some boring Spec functions. *)
 module DefaultSpec =
 struct
+  module V = VarinfoV
+
   type marshal = unit
   let init _ = ()
   let finalize () = ()

src/framework/constraints.ml

@@ -18,6 +18,7 @@ struct
   module D = Lattice.HConsed (S.D)
   module G = S.G
   module C = S.C
+  module V = S.V
 
   let name () = S.name () ^" hashconsed"
 
@@ -95,6 +96,7 @@ struct
   module D = S.D
   module G = S.G
   module C = Printable.HConsed (S.C)
+  module V = S.V
 
   let name () = S.name () ^" context hashconsed"
 
@@ -182,6 +184,7 @@ struct
   module D = Lattice.Prod (S.D) (Lattice.Reverse (IntDomain.Lifted))
   module G = S.G
   module C = S.C
+  module V = S.V
 
   let name () = S.name ()^" level sliced"
 
@@ -322,6 +325,7 @@ struct
   end
   module G = S.G
   module C = S.C
+  module V = S.V
 
 
   let name () = S.name ()^" with widened contexts"
@@ -391,6 +395,7 @@ struct
   module D = Dom (S.D)
   module G = S.G
   module C = S.C
+  module V = S.V
 
   let name () = S.name ()^" lifted"
 
@@ -897,6 +902,7 @@ module PathSensitive2 (Spec:Spec)
     with type D.t = HoareDomain.Set(Spec.D).t
      and module G = Spec.G
      and module C = Spec.C
+     and module V = Spec.V
 =
 struct
   module D =
@@ -938,6 +944,7 @@ struct
 
   module G = Spec.G
   module C = Spec.C
+  module V = Spec.V
 
   let name () = "PathSensitive2("^Spec.name ()^")"
 

src/witness/witnessConstraints.ml

@@ -152,6 +152,7 @@ struct
 
   module G = Spec.G
   module C = Spec.C
+  module V = Spec.V
 
   let name () = "PathSensitive3("^Spec.name ()^")"