Module `BufferOverrunUtils.Exec`

val load_locs : represents_multiple_values:bool -> modeled_range:Dom.ModeledRange.t option -> IR.Ident.t -> IR.Typ.t -> AbsLoc.PowLoc.t -> Dom.Mem.t -> Dom.Mem.t
val decl_local : ModelEnv.model_env -> (Dom.Mem.t * int) -> (AbsLoc.Loc.t * IR.Typ.t) -> Dom.Mem.t * int
val init_c_array_fields : ModelEnv.model_env -> Itv.SymbolPath.partial option -> IR.Typ.t -> AbsLoc.PowLoc.t -> ?⁠dyn_length:IR.Exp.t -> Dom.Mem.t -> Dom.Mem.t
val set_dyn_length : ModelEnv.model_env -> IR.Typ.t -> AbsLoc.PowLoc.t -> Itv.t -> Dom.Mem.t -> Dom.Mem.t
val decl_string : ModelEnv.model_env -> do_alloc:bool -> AbsLoc.PowLoc.t -> string -> Dom.Mem.t -> Dom.Mem.t
val set_c_strlen : tgt:Dom.Val.t -> src:Dom.Val.t -> Dom.Mem.t -> Dom.Mem.t