Module BO__BufferOverrunProofObligations.ConditionSet

type checked_t
type summary_t
val empty : checked_t
val pp : Stdlib.Format.formatter -> checked_t -> unit
val pp_summary : Stdlib.Format.formatter -> summary_t -> unit
val add_array_access : IBase.Location.t -> offset:ItvPure.t -> idx:ItvPure.t -> size:ItvPure.t -> last_included:bool -> idx_traces:BO.BufferOverrunTrace.Set.t -> arr_traces:BO.BufferOverrunTrace.Set.t -> latest_prune:BO.BufferOverrunDomain.LatestPrune.t -> checked_t -> checked_t
val add_alloc_size : IBase.Location.t -> can_be_zero:bool -> length:ItvPure.t -> BO.BufferOverrunTrace.Set.t -> BO.BufferOverrunDomain.LatestPrune.t -> checked_t -> checked_t
val add_binary_operation : IR.Typ.IntegerWidths.t -> IBase.Location.t -> IR.Procname.t -> IR.Binop.t -> lhs:ItvPure.t -> rhs:ItvPure.t -> lhs_traces:BO.BufferOverrunTrace.Set.t -> rhs_traces:BO.BufferOverrunTrace.Set.t -> latest_prune:BO.BufferOverrunDomain.LatestPrune.t -> checked_t -> checked_t
val join : checked_t -> checked_t -> checked_t
val subst : summary_t -> (mode:BO.BufferOverrunSemantics.eval_mode -> BO.BufferOverrunDomain.eval_sym_trace) -> IR.Procname.t -> IBase.Location.t -> BO.BufferOverrunDomain.LatestPrune.t -> checked_t
val report_errors : report:(Condition.t -> ConditionTrace.t -> IBase.IssueType.t -> unit) -> checked_t -> unit
val for_summary : checked_t -> summary_t