Module BufferOverrunDomain.MemReach

Domain for memory of reachable node

type 'has_oenv t0

'has_oenv represents an environment for on-demand symbol evaluation, which is required during the analysis, but not in the summary

type t = IStdlib.GOption.some t0
val range : filter_loc:(AbsLoc.Loc.t -> LoopHeadLoc.t option) -> node_id:IR.Procdesc.Node.id -> t -> Polynomials.NonNegativePolynomial.t

Return the multiplication of the ranges of all the abstract locations in memory that satisfy the function filter_loc which filters abstract locations we should care about, e.g., control variables that decide how many times a node is executed