Module BO.BufferOverrunDomain

Set of integers for threshold widening

module ItvUpdatedBy : sig ... end

Domain for recording which operations are used for evaluating interval values

module ModeledRange : sig ... end

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,

type eval_sym_trace = {
  1. eval_sym : Bounds.Bound.eval_sym;
    (*

    evaluating symbol

    *)
  2. eval_locpath : AbsLoc.PowLoc.eval_locpath;
    (*

    evaluating path

    *)
  3. eval_func_ptrs : FuncPtr.Set.eval_func_ptrs;
    (*

    evaluating function pointers

    *)
  4. trace_of_sym : Symb.Symbol.t -> BufferOverrunTrace.Set.t;
    (*

    getting traces of symbol

    *)
}

type for on-demand symbol evaluation in Inferbo

module Val : sig ... end
module KeyRhs : sig ... end

Right hand side of the alias domain. See AliasTarget.

module AliasTarget : sig ... end
module AliasTargets : sig ... end
module AliasRet : sig ... end

Alias domain for return values of callees

module CoreVal : sig ... end

CoreVal is similar to Val, but its compare function is defined only on core parts, interval, pointers, and array blocks, of abstract value. This domain is to keep pruned values, where we do not need to care about the other fields in the abstract values.

module PruningExp : sig ... end

Domain to keep assumed expressions

module PrunedVal : sig ... end

Domain to keep pruned history, which are pairs of a pruned value and an assumed expression

module PrunePairs : sig ... end

PrunePairs is a map from abstract locations to abstract values that represents pruned results in the latest pruning. It uses InvertedMap because more pruning means smaller abstract states.

module LatestPrune : sig ... end

Domain to keep latest pruned values

module Reachability : sig ... end

Domain for reachability check

module LoopHeadLoc : sig ... end
module MemReach : sig ... end

Domain for memory of reachable node

module Mem : sig ... end