module Init (ZZ3 : ZZ3_sigs.S) (SMTg : module type of Smtgraph.Make(ZZ3)) : sig .. end
val env : (Llvm.llvalue * bool, Z3.Expr.expr) Hashtbl.t
Environment mapping llvm values (primed, or not) to smt values.
A phi variable is primed if it's used from a split node.
val get_var : primed:bool -> Llvm.llvalue -> [> ZZ3.znum ] ZZ3.term
val get_block : primed:bool -> Llvm.llbasicblock -> [> ZZ3.zbool ] ZZ3.term
val llvm2smt : Llvm.llvalue -> Llvm.llbasicblock list -> Llvmcfg.t -> SMTg.t
Transform an Llvm graph into a formula graph, filling env on the way.