goblint · sim642 · Aug 9, 2022 · Jul 23, 2022 · Jul 23, 2022 · Jul 23, 2022
diff --git a/goblint.opam b/goblint.opam
@@ -67,7 +67,7 @@ dev-repo: "git+https://github.com/goblint/analyzer.git"
 # on `dune build` goblint.opam will be generated from goblint.opam.template and dune-project
 # also remember to generate/adjust goblint.opam.locked!
 pin-depends: [
-  [ "goblint-cil.1.8.2" "git+https://github.com/goblint/cil.git#54b0c220a9cea4213ff596eadff877a6ec9b00fb" ]
+  [ "goblint-cil.1.8.2" "git+https://github.com/goblint/cil.git#1faa2355fd350c503b150e43c4577873928c30d9" ]
   # TODO: add back after release, only pinned for optimization (https://github.com/ocaml-ppx/ppx_deriving/pull/252)
   [ "ppx_deriving.5.2.1" "git+https://github.com/ocaml-ppx/ppx_deriving.git#0a89b619f94cbbfc3b0fb3255ab4fe5bc77d32d6" ]
   # quoter workaround reverted for release, so no pin needed

diff --git a/goblint.opam.locked b/goblint.opam.locked
@@ -120,7 +120,7 @@ version: "dev"
 pin-depends: [
   [
     "goblint-cil.1.8.2"
-    "git+https://github.com/goblint/cil.git#54b0c220a9cea4213ff596eadff877a6ec9b00fb"
+    "git+https://github.com/goblint/cil.git#1faa2355fd350c503b150e43c4577873928c30d9"
   ]
   [
     "apron.v0.9.13"

diff --git a/goblint.opam.template b/goblint.opam.template
@@ -1,7 +1,7 @@
 # on `dune build` goblint.opam will be generated from goblint.opam.template and dune-project
 # also remember to generate/adjust goblint.opam.locked!
 pin-depends: [
-  [ "goblint-cil.1.8.2" "git+https://github.com/goblint/cil.git#54b0c220a9cea4213ff596eadff877a6ec9b00fb" ]
+  [ "goblint-cil.1.8.2" "git+https://github.com/goblint/cil.git#1faa2355fd350c503b150e43c4577873928c30d9" ]
   # TODO: add back after release, only pinned for optimization (https://github.com/ocaml-ppx/ppx_deriving/pull/252)
   [ "ppx_deriving.5.2.1" "git+https://github.com/ocaml-ppx/ppx_deriving.git#0a89b619f94cbbfc3b0fb3255ab4fe5bc77d32d6" ]
   # quoter workaround reverted for release, so no pin needed

diff --git a/gobview b/gobview
diff --git a/src/analyses/basePriv.mli b/src/analyses/basePriv.mli
@@ -1,4 +1,4 @@
-open Cil
+open GoblintCil
 (* Cannot use local module substitutions because ppx_import is still stuck at 4.07 AST: https://github.com/ocaml-ppx/ppx_import/issues/50#issuecomment-775817579. *)
 (* TODO: try again, because ppx_import is now removed *)
 

diff --git a/src/analyses/baseUtil.mli b/src/analyses/baseUtil.mli
@@ -1,4 +1,4 @@
-open Cil
+open GoblintCil
 
 val is_global: Queries.ask -> varinfo -> bool
 val is_static: varinfo -> bool

diff --git a/src/analyses/libraryDesc.ml b/src/analyses/libraryDesc.ml
@@ -1,4 +1,5 @@
 (** Library function descriptor (specification). *)
+module Cil = GoblintCil
 
 (** Pointer argument access specification. *)
 module Access =

diff --git a/src/analyses/libraryDsl.mli b/src/analyses/libraryDsl.mli
@@ -1,4 +1,5 @@
 (** Library function descriptor DSL. *)
+open GoblintCil
 
 (** See {!LibraryFunctions} implementation for example usage. *)
 

diff --git a/src/analyses/libraryFunctionEffects.ml b/src/analyses/libraryFunctionEffects.ml
@@ -1,3 +1,5 @@
+open GoblintCil
+
 let effects: (string -> Cil.exp list -> (Cil.lval * _) list option) list ref = ref []
 let add_effects f = effects := f :: !effects
 let effects_for fname args = List.filter_map (fun f -> f fname args) !effects
diff --git a/src/analyses/libraryFunctionEffects.mli b/src/analyses/libraryFunctionEffects.mli
@@ -1,3 +1,5 @@
 (* can't use Base.Main.store b/c of circular build - this is painful... *)
+open GoblintCil
+
 val add_effects : (string -> Cil.exp list -> (Cil.lval * ValueDomain.Compound.t) list option) -> unit
 val effects_for : string -> Cil.exp list -> (Cil.lval * ValueDomain.Compound.t) list list
diff --git a/src/analyses/libraryFunctions.mli b/src/analyses/libraryFunctions.mli
@@ -1,4 +1,5 @@
 (** This allows us to query information about library functions. *)
+open GoblintCil
 
 val add_lib_funs : string list -> unit
 

diff --git a/src/analyses/mCPAccess.ml b/src/analyses/mCPAccess.ml
@@ -1,5 +1,6 @@
 
 open MCPRegistry
+module Pretty = GoblintCil.Pretty
 
 (** Access module corresponding to MCP.
     Separate to avoid dependency cycle. *)

diff --git a/src/cdomains/addressDomain.ml b/src/cdomains/addressDomain.ml
@@ -1,4 +1,4 @@
-open Cil
+open GoblintCil
 open Pretty
 open IntOps
 

diff --git a/src/cdomains/apron/apronDomain.apron.ml b/src/cdomains/apron/apronDomain.apron.ml
@@ -1,5 +1,5 @@
 open Prelude
-open Cil
+open GoblintCil
 open Pretty
 (* A binding to a selection of Apron-Domains *)
 open Apron

diff --git a/src/cdomains/arrayDomain.ml b/src/cdomains/arrayDomain.ml
@@ -1,5 +1,5 @@
+open GoblintCil
 open Pretty
-open Cil
 open GobConfig
 open FlagHelper
 

diff --git a/src/cdomains/arrayDomain.mli b/src/cdomains/arrayDomain.mli
@@ -1,4 +1,5 @@
 open IntOps
+open GoblintCil
 
 (** Abstract domains representing arrays. *)
 module type S =

diff --git a/src/cdomains/baseDomain.ml b/src/cdomains/baseDomain.ml
@@ -1,6 +1,6 @@
 (** domain of the base analysis *)
 
-open Cil
+open GoblintCil
 module VD = ValueDomain.Compound
 module BI = IntOps.BigIntOps
 

diff --git a/src/cdomains/basetype.ml b/src/cdomains/basetype.ml
@@ -1,5 +1,5 @@
 module GU = Goblintutil
-open Cil
+open GoblintCil
 
 
 (** Location with special alphanumeric output for extraction. *)

diff --git a/src/cdomains/floatDomain.ml b/src/cdomains/floatDomain.ml
@@ -1,7 +1,7 @@
+open GoblintCil
 open Pretty
 open PrecisionUtil
 open FloatOps
-open Cil
 
 exception ArithmeticOnFloatBot of string
 

diff --git a/src/cdomains/floatDomain.mli b/src/cdomains/floatDomain.mli
@@ -1,5 +1,6 @@
 (** Abstract Domains for floats. These are domains that support the C
   * operations on double/float values. *)
+open GoblintCil
 
 exception ArithmeticOnFloatBot of string
 

diff --git a/src/cdomains/intDomain.ml b/src/cdomains/intDomain.ml
@@ -1,4 +1,5 @@
 open GobConfig
+open GoblintCil
 open Pretty
 open PrecisionUtil
 

diff --git a/src/cdomains/intDomain.mli b/src/cdomains/intDomain.mli
@@ -1,5 +1,6 @@
 (** Abstract Domains for integers. These are domains that support the C
   * operations on integer values. *)
+open GoblintCil
 
 val should_wrap: Cil.ikind -> bool
 val should_ignore_overflow: Cil.ikind -> bool

diff --git a/src/cdomains/lockDomain.ml b/src/cdomains/lockDomain.ml
@@ -4,7 +4,7 @@ module Equ = MusteqDomain.Equ
 module Exp = CilType.Exp
 module IdxDom = ValueDomain.IndexDomain
 
-open Cil
+open GoblintCil
 
 module Mutexes = SetDomain.ToppedSet (Addr) (struct let topname = "All mutexes" end) (* TODO HoareDomain? *)
 module Simple = Lattice.Reverse (Mutexes)

diff --git a/src/cdomains/lval.ml b/src/cdomains/lval.ml
@@ -1,4 +1,4 @@
-open Cil
+open GoblintCil
 open Pretty
 
 module GU = Goblintutil

diff --git a/src/cdomains/lvalMapDomain.ml b/src/cdomains/lvalMapDomain.ml
@@ -1,5 +1,5 @@
 open Prelude
-open Cil
+open GoblintCil
 
 module M = Messages
 

diff --git a/src/cdomains/mHP.ml b/src/cdomains/mHP.ml
@@ -1,6 +1,7 @@
 include Printable.Std
 
 module TID = ThreadIdDomain.FlagConfiguredTID
+module Pretty = GoblintCil.Pretty
 
 type t = {
   tid: ThreadIdDomain.ThreadLifted.t;

diff --git a/src/cdomains/musteqDomain.ml b/src/cdomains/musteqDomain.ml
@@ -1,4 +1,4 @@
-open Cil
+open GoblintCil
 open Pretty
 
 module V = Basetype.Variables

diff --git a/src/cdomains/regionDomain.ml b/src/cdomains/regionDomain.ml
@@ -1,4 +1,4 @@
-open Cil
+open GoblintCil
 open GobConfig
 
 module GU = Goblintutil

diff --git a/src/cdomains/structDomain.ml b/src/cdomains/structDomain.ml
@@ -1,4 +1,4 @@
-open Cil
+open GoblintCil
 open GobConfig
 open Pretty
 open FlagHelper

diff --git a/src/cdomains/structDomain.mli b/src/cdomains/structDomain.mli
@@ -1,6 +1,6 @@
 (** Abstract domains representing structs. *)
 
-open Cil
+open GoblintCil
 
 module type Arg =
 sig

diff --git a/src/cdomains/symbLocksDomain.ml b/src/cdomains/symbLocksDomain.ml
@@ -1,5 +1,5 @@
+open GoblintCil
 open Pretty
-open Cil
 
 module Exp =
 struct

diff --git a/src/cdomains/threadIdDomain.ml b/src/cdomains/threadIdDomain.ml
@@ -1,4 +1,4 @@
-open Cil
+open GoblintCil
 open FlagHelper
 
 module type S =

diff --git a/src/cdomains/unionDomain.ml b/src/cdomains/unionDomain.ml
@@ -1,3 +1,5 @@
+open GoblintCil
+
 module type Arg = Lattice.S
 
 module type S =

diff --git a/src/cdomains/valueDomain.ml b/src/cdomains/valueDomain.ml
@@ -1,4 +1,4 @@
-open Cil
+open GoblintCil
 open Pretty
 open GobConfig
 open PrecisionUtil

diff --git a/src/domains/access.ml b/src/domains/access.ml
@@ -1,5 +1,5 @@
 open Batteries
-open Cil
+open GoblintCil
 open Pretty
 open GobConfig
 

diff --git a/src/domains/boolDomain.ml b/src/domains/boolDomain.ml
@@ -7,7 +7,7 @@ struct
   let relift x = x
   let arbitrary () = QCheck.bool *)
 
-  let pretty_diff () (x,y) = Pretty.dprintf "%s: %a not leq %a" (name ()) pretty x pretty y
+  let pretty_diff () (x,y) = GoblintCil.Pretty.dprintf "%s: %a not leq %a" (name ()) pretty x pretty y
 end
 
 module MayBool: Lattice.S with type t = bool =

diff --git a/src/domains/hoareDomain.ml b/src/domains/hoareDomain.ml
@@ -1,5 +1,6 @@
 (** Abstract domains with Hoare ordering. *)
 
+module Pretty = GoblintCil.Pretty
 open Pretty
 
 exception Unsupported of string

diff --git a/src/domains/intDomainProperties.ml b/src/domains/intDomainProperties.ml
@@ -1,3 +1,4 @@
+open GoblintCil
 module BI = IntOps.BigIntOps
 
 (* TODO: deduplicate with IntDomain *)

diff --git a/src/domains/invariant.ml b/src/domains/invariant.ml
@@ -1,4 +1,4 @@
-open Cil
+open GoblintCil
 
 (** Symbolic (and fully syntactic) expression "lattice". *)
 module ExpLat =

diff --git a/src/domains/invariantCil.ml b/src/domains/invariantCil.ml
@@ -1,4 +1,4 @@
-open Cil
+open GoblintCil
 
 
 let var_replace_original_name vi =

diff --git a/src/domains/lattice.ml b/src/domains/lattice.ml
@@ -1,5 +1,6 @@
 (** The lattice signature and simple functors for building lattices. *)
 
+module Pretty = GoblintCil.Pretty
 module GU = Goblintutil
 
 (* module type Rel =

diff --git a/src/domains/mapDomain.ml b/src/domains/mapDomain.ml
@@ -1,5 +1,6 @@
 (** Specification and functors for maps. *)
 
+module Pretty = GoblintCil.Pretty
 open Pretty
 module ME = Messages
 module GU = Goblintutil
@@ -263,7 +264,7 @@ module Timed (M: S) : S with
   type key = M.key and
   type value = M.value =
 struct
-  let time str f arg = Stats.time (M.name ()) (Stats.time str f) arg
+  let time str f arg = GoblintCil.Stats.time (M.name ()) (GoblintCil.Stats.time str f) arg
 
   (* Printable.S *)
   type t = M.t

diff --git a/src/domains/myCheck.ml b/src/domains/myCheck.ml
@@ -56,5 +56,6 @@ struct
     let shrinks = List.map shrink arbs in
     make ~shrink:(Shrink.sequence shrinks) (Gen.sequence gens)
 
+  open GoblintCil
   let varinfo: Cil.varinfo arbitrary = QCheck.always (Cil.makeGlobalVar "arbVar" Cil.voidPtrType) (* S TODO: how to generate this *)
 end
diff --git a/src/domains/printable.ml b/src/domains/printable.ml
@@ -1,5 +1,6 @@
 (** Some things are not quite lattices ... *)
 
+module Pretty = GoblintCil.Pretty
 open Pretty
 
 module type S =

diff --git a/src/domains/queries.ml b/src/domains/queries.ml
@@ -1,6 +1,6 @@
 (** Structures for the querying subsystem. *)
 
-open Cil
+open GoblintCil
 
 module GU = Goblintutil
 module ID =

diff --git a/src/domains/setDomain.ml b/src/domains/setDomain.ml
@@ -1,4 +1,5 @@
 (** Abstract domains representing sets. *)
+module Pretty = GoblintCil.Pretty
 open Pretty
 
 (* Exception raised when the set domain can not support the requested operation.

diff --git a/src/framework/analyses.ml b/src/framework/analyses.ml
@@ -1,7 +1,7 @@
 (** Signatures for analyzers, analysis specifications, and result output.  *)
 
 open Prelude
-open Cil
+open GoblintCil
 open Pretty
 open GobConfig
 

diff --git a/src/framework/cfgTools.ml b/src/framework/cfgTools.ml
@@ -1,5 +1,5 @@
 open MyCFG
-open Cil
+open GoblintCil
 open Pretty
 open GobConfig
 

diff --git a/src/framework/constraints.ml b/src/framework/constraints.ml
@@ -1,7 +1,7 @@
 (** How to generate constraints for a solver using specifications described in [Analyses]. *)
 
 open Prelude
-open Cil
+open GoblintCil
 open MyCFG
 open Analyses
 open GobConfig

diff --git a/src/framework/control.ml b/src/framework/control.ml
@@ -1,7 +1,7 @@
 (** An analyzer that takes the CFG from [MyCFG], a solver from [Selector], constraints from [Constraints] (using the specification from [MCP]) *)
 
 open Prelude
-open Cil
+open GoblintCil
 open MyCFG
 open Analyses
 open GobConfig

diff --git a/src/framework/edge.ml b/src/framework/edge.ml
@@ -1,4 +1,4 @@
-open Cil
+open GoblintCil
 open Pretty
 
 type asm_out = (string option * string * CilType.Lval.t) list [@@deriving eq, to_yojson]

diff --git a/src/framework/myCFG.ml b/src/framework/myCFG.ml
@@ -1,6 +1,6 @@
 (** Our Control-flow graph implementation. *)
 
-open Cil
+open GoblintCil
 
 (** Re-exported [Node.t] with constructors. See [Node.t] for documentation. *)
 type node = Node.t =

diff --git a/src/framework/node.ml b/src/framework/node.ml
@@ -1,4 +1,4 @@
-open Cil
+open GoblintCil
 open Pretty
 
 include Printable.Std

diff --git a/src/incremental/compareAST.ml b/src/incremental/compareAST.ml
@@ -1,4 +1,4 @@
-open Cil
+open GoblintCil
 open CilMaps
 
 (* global_type and global_t are implicitly used by GlobalMap to keep GVarDecl apart from GVar and GFun, so do not remove! *)

diff --git a/src/incremental/compareCFG.ml b/src/incremental/compareCFG.ml
@@ -1,6 +1,6 @@
 open MyCFG
 open Queue
-open Cil
+open GoblintCil
 open CilMaps
 include CompareAST
 

diff --git a/src/incremental/compareCIL.ml b/src/incremental/compareCIL.ml
@@ -1,4 +1,4 @@
-open Cil
+open GoblintCil
 open MyCFG
 open CilMaps
 include CompareAST
+1 −0		src/App.re
+1 −1		src/DeadCodeView.re
+1 −0		src/state/gvDisplay.ml
+1 −1		src/state/gvGoblint.ml
+1 −1		src/state/gvInspect.ml
+2 −0		src/state/search.ml
+1 −0		src/state/state.ml
+1 −1		src/ui/content/gvFileView.re
+1 −0		src/ui/navigation/gvFileList.re
+1 −0		src/ui/navigation/search/searchFindBuilder.re
+1 −0		src/ui/navigation/search/searchKindBuilder.re
+1 −1		src/ui/navigation/search/searchResultView.re
+1 −0		src/ui/navigation/search/searchStructureBuilder.re
+1 −0		src/ui/navigation/search/searchTargetBuilder.re
+1 −0		src/ui/panel/gvStatisticsView.re