Module `BufferOverrunDomain.ModeledRange`

ModeledRange represents how many times the interval value can be updated by modeled functions. This domain is to support the case where there are mismatches between value of a control variable and actual number of loop iterations. For example,

while((c = file_channel.read(buf)) != -1) { ... }

the loop will iterate as many times as the file size, but the control variable c does not have that value. In these cases, it assigns a symbolic value of the file size to the modeled range of c, which is used when calculating the overall cost.

type t

val of_big_int : trace:BO.Bounds.BoundTrace.t -> Z.t -> t
val of_modeled_function : IR.Procname.t -> IBase.Location.t -> Bounds.Bound.t -> t