Exec (infer.BO.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

load_locs id typ locs mem loads the contents of the memory locations locs (which have type typ) into the identifier id.

If locs represents a single location, also create an aliasing relation between this location and id. This is useful, e.g., to constrain also the location when the identifier is constrained.

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 ->
  BO.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