BufferOverrunUtils.Checkval 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_tval lindex :
IR.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_tval lindex_byte :
IR.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_tval binary_operation :
IR.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