BufferOverrunProofObligations.ConditionSetval empty : checked_tval pp : Stdlib.Format.formatter -> checked_t -> unitval pp_summary : Stdlib.Format.formatter -> summary_t -> unitval 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_tval add_alloc_size :
IBase.Location.t ->
can_be_zero:bool ->
length:ItvPure.t ->
BufferOverrunTrace.Set.t ->
BufferOverrunDomain.LatestPrune.t ->
checked_t ->
checked_tval add_binary_operation :
IR.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_tval subst :
summary_t ->
(mode:BufferOverrunSemantics.eval_mode -> BufferOverrunDomain.eval_sym_trace) ->
IR.Procname.t ->
IBase.Location.t ->
BufferOverrunDomain.LatestPrune.t ->
checked_tval report_errors :
report:(Condition.t -> ConditionTrace.t -> IBase.IssueType.t -> unit) ->
checked_t ->
unit