Module InferModules.BufferOverrunSemantics

val eval_const : InferIR.Typ.IntegerWidths.t -> InferIR.Const.t -> BufferOverrunDomain.Val.t
val must_alias : InferIR.Exp.t -> InferIR.Exp.t -> BufferOverrunDomain.Mem.t -> bool
val must_alias_opt : InferIR.Exp.t option -> InferIR.Exp.t option -> BufferOverrunDomain.Mem.t -> bool
val comp_rev : InferIR.Binop.t -> InferIR.Binop.t
val comp_not : InferIR.Binop.t -> InferIR.Binop.t
val must_alias_cmp : InferIR.Exp.t -> BufferOverrunDomain.Mem.t -> bool
val set_array_stride : InferIR.Typ.IntegerWidths.t -> InferIR.Typ.t -> BufferOverrunDomain.Val.t -> BufferOverrunDomain.Val.t
val eval : InferIR.Typ.IntegerWidths.t -> InferIR.Exp.t -> BufferOverrunDomain.Mem.t -> BufferOverrunDomain.Val.t
val eval_lindex : InferIR.Typ.IntegerWidths.t -> InferIR.Exp.t -> InferIR.Exp.t -> BufferOverrunDomain.Mem.t -> BufferOverrunDomain.Val.t
val eval_unop : InferIR.Typ.IntegerWidths.t -> InferIR.Unop.t -> InferIR.Exp.t -> BufferOverrunDomain.Mem.t -> BufferOverrunDomain.Val.t
val eval_binop : InferIR.Typ.IntegerWidths.t -> InferIR.Binop.t -> InferIR.Exp.t -> InferIR.Exp.t -> BufferOverrunDomain.Mem.t -> BufferOverrunDomain.Val.t
val eval_locs : InferIR.Exp.t -> BufferOverrunDomain.Mem.t -> AbsLoc.PowLoc.t

eval_locs exp mem is like eval exp mem |> Val.get_all_locs but takes some shortcuts to avoid computing useless and/or problematic intermediate values

val eval_arr : InferIR.Typ.IntegerWidths.t -> InferIR.Exp.t -> BufferOverrunDomain.Mem.t -> BufferOverrunDomain.Val.t
val is_stack_exp : InferIR.Exp.t -> BufferOverrunDomain.Mem.t -> bool
module ParamBindings : sig ... end
type eval_mode =
| EvalNormal
| EvalPOCond
| EvalPOReachability
val eval_sympath_modeled_partial : mode:eval_mode -> Symb.SymbolPath.partial -> BufferOverrunDomain.Val.t
val eval_sympath_partial : mode:eval_mode -> BufferOverrunDomain.Val.t ParamBindings.t -> Symb.SymbolPath.partial -> 'a BufferOverrunDomain.Mem.t0 -> BufferOverrunDomain.Val.t
val eval_locpath : mode:eval_mode -> BufferOverrunDomain.Val.t ParamBindings.t -> Symb.SymbolPath.partial -> 'a BufferOverrunDomain.Mem.t0 -> AbsLoc.PowLoc.t
val eval_sympath : mode:eval_mode -> BufferOverrunDomain.Val.t ParamBindings.t -> Symb.SymbolPath.t -> 'a BufferOverrunDomain.Mem.t0 -> Itv.t * InferModules__BufferOverrunDomain.TraceSet.t
val mk_eval_sym_trace : InferIR.Typ.IntegerWidths.t -> (ParamBindings.key * 'a) list -> (InferIR.Exp.t * 'b) InferStdlib.IStd.List.t -> BufferOverrunDomain.Mem.t -> mode:eval_mode -> BufferOverrunDomain.eval_sym_trace
val mk_eval_sym : InferIR.Typ.IntegerWidths.t -> (ParamBindings.key * 'a) list -> (InferIR.Exp.t * 'b) InferStdlib.IStd.List.t -> BufferOverrunDomain.Mem.t -> Bounds.Bound.eval_sym
val get_sym_f : InferIR.Typ.IntegerWidths.t -> BufferOverrunDomain.Mem.t -> InferIR.Exp.t -> InferModules__BufferOverrunDomain.Relation.Sym.t
val get_offset_sym_f : InferIR.Typ.IntegerWidths.t -> BufferOverrunDomain.Mem.t -> InferIR.Exp.t -> InferModules__BufferOverrunDomain.Relation.Sym.t
val get_size_sym_f : InferIR.Typ.IntegerWidths.t -> BufferOverrunDomain.Mem.t -> InferIR.Exp.t -> InferModules__BufferOverrunDomain.Relation.Sym.t
module Prune : sig ... end
val get_matching_pairs : InferIR.Tenv.t -> InferIR.Typ.IntegerWidths.t -> BufferOverrunDomain.Val.t -> BufferOverrunDomain.Val.t -> InferIR.Exp.t option -> InferIR.Typ.t -> BufferOverrunDomain.Mem.t -> 'a BufferOverrunDomain.Mem.t0 -> (BufferOverrunDomain.Relation.Var.t * BufferOverrunDomain.Relation.SymExp.t option) list
val subst_map_of_rel_pairs : (BufferOverrunDomain.Relation.Var.t * BufferOverrunDomain.Relation.SymExp.t option) list -> BufferOverrunDomain.Relation.SubstMap.t
val list_fold2_def : default:(BufferOverrunDomain.Val.t * InferIR.Exp.t option) -> f:('a -> (BufferOverrunDomain.Val.t * InferIR.Exp.t option) -> 'b -> 'b) -> 'a list -> (BufferOverrunDomain.Val.t * InferIR.Exp.t option) list -> init:'b -> 'b
val get_subst_map : InferIR.Tenv.t -> InferIR.Typ.IntegerWidths.t -> (InferIR.Pvar.t * InferIR.Typ.t) list -> (InferIR.Exp.t * 'a) list -> BufferOverrunDomain.Mem.t -> 'b BufferOverrunDomain.Mem.t0 -> BufferOverrunDomain.Relation.SubstMap.t