BufferOverrunModels (infer.BO.BufferOverrunModels)

type exec_fun =
  BufferOverrunUtils.ModelEnv.model_env ->
  ret:(IR.Ident.t * IR.Typ.t) ->
  BufferOverrunDomain.Mem.t ->
  BufferOverrunDomain.Mem.t

type check_fun =
  BufferOverrunUtils.ModelEnv.model_env ->
  BufferOverrunDomain.Mem.t ->
  BufferOverrunProofObligations.ConditionSet.checked_t ->
  BufferOverrunProofObligations.ConditionSet.checked_t

type model = {

exec : exec_fun;
check : check_fun;

}

module Collection : sig ... end

module Container : sig ... end

module NSCollection : sig ... end

module NSString : sig ... end

module JavaString : sig ... end

module Call : sig ... end