Module `BufferOverrunUtils.Check`

val array_access : arr:Dom.Val.t -> idx:Dom.Val.t -> is_plus:bool -> last_included:bool -> latest_prune:Dom.LatestPrune.t -> IBase.Location.t -> PO.ConditionSet.checked_t -> PO.ConditionSet.checked_t
val lindex : IR.Typ.IntegerWidths.t -> array_exp:IR.Exp.t -> index_exp:IR.Exp.t -> last_included:bool -> Dom.Mem.t -> IBase.Location.t -> PO.ConditionSet.checked_t -> PO.ConditionSet.checked_t
val lindex_byte : IR.Typ.IntegerWidths.t -> array_exp:IR.Exp.t -> byte_index_exp:IR.Exp.t -> last_included:bool -> Dom.Mem.t -> IBase.Location.t -> PO.ConditionSet.checked_t -> PO.ConditionSet.checked_t
val binary_operation : IR.Typ.IntegerWidths.t -> IR.Procname.t -> IR.Binop.t -> lhs:Dom.Val.t -> rhs:Dom.Val.t -> latest_prune:Dom.LatestPrune.t -> IBase.Location.t -> PO.ConditionSet.checked_t -> PO.ConditionSet.checked_t