Module 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:BufferOverrunTrace.Set.t -> arr_traces:BufferOverrunTrace.Set.t -> latest_prune:BufferOverrunDomain.LatestPrune.t -> checked_t -> checked_t
val add_alloc_size : IBase.Location.t -> can_be_zero:bool -> length:ItvPure.t -> BufferOverrunTrace.Set.t -> 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:BufferOverrunTrace.Set.t -> rhs_traces:BufferOverrunTrace.Set.t -> latest_prune:BufferOverrunDomain.LatestPrune.t -> checked_t -> checked_t
val join : checked_t -> checked_t -> checked_t
val subst : summary_t -> (mode:BufferOverrunSemantics.eval_mode -> BufferOverrunDomain.eval_sym_trace) -> IR.Procname.t -> IBase.Location.t -> 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