Module `BO.BufferOverrunSemantics`

val is_stack_exp : IR.Exp.t -> BufferOverrunDomain.Mem.t -> bool: Check if an expression is a stack variable such as n$0 or local variable for C array

val eval : IR.Typ.IntegerWidths.t -> IR.Exp.t -> BufferOverrunDomain.Mem.t -> BufferOverrunDomain.Val.t: Evalute an expression

val eval_locs : IR.Exp.t -> BufferOverrunDomain.Mem.t -> AbsLoc.PowLoc.t: eval_locs exp mem is like eval exp mem |> Val.get_all_locs but takes some shortcuts to avoid computing useless and/or problematic intermediate values

val eval_arr : IR.Typ.IntegerWidths.t -> IR.Exp.t -> BufferOverrunDomain.Mem.t -> BufferOverrunDomain.Val.t: Return the array value of the input expression. For example, when x is a program variable, eval_arr x returns array blocks the x is pointing to, on the other hand, eval x returns the abstract location of x.

val eval_lindex : IR.Typ.IntegerWidths.t -> IR.Exp.t -> IR.Exp.t -> BufferOverrunDomain.Mem.t -> BufferOverrunDomain.Val.t: Evaluate array location with index, i.e., eval_lindex integer_type_widths array_exp index_exp mem

val eval_array_locs_length : AbsLoc.PowLoc.t -> _ BufferOverrunDomain.Mem.t0 -> BufferOverrunDomain.Val.t: Evaluate length of array locations

val eval_string_len : IR.Exp.t -> BufferOverrunDomain.Mem.t -> BufferOverrunDomain.Val.t: Evaluate length of C string

val conservative_array_length : ?⁠traces:BufferOverrunTrace.Set.t -> AbsLoc.PowLoc.t -> _ BufferOverrunDomain.Mem.t0 -> BufferOverrunDomain.Val.t: Evaluate the array length conservatively, which is useful when there are multiple array locations and their lengths are joined to top. For example, if the arr_locs points to two arrays a and b and if their lengths are a.length and b.length, this function evaluates its length as [0, a.length.ub + b.length.ub].

type eval_mode = | EvalNormal Given a symbolic value of an unknown function Symb.SymbolPath.Callsite, it returns a symbolic interval value. | EvalPOCond Given a symbolic value of an unknown function, it returns the top interval value. This is used when substituting condition expressions of proof obligations. | EvalPOReachability This is similar to EvalPOCond, but it returns the bottom location, instead of the unknown location, when a location to substitute is not found. This is used when substituting reachabilities of proof obligations. | EvalCost This is similar to EvalNormal, but it is designed to be used in substitutions of the cost results, avoiding precision loss by joining of symbolic values. Normal join of two different symbolic values, s1 and s2, becomes top due to the limitation of our domain. On the other hand, in this mode, it returns an upperbound s1+s2 for the case, because the cost values only care about the upperbounds.: Several modes of ondemand evaluations

val mk_eval_sym_trace : ?⁠is_args_ref:bool -> IR.Typ.IntegerWidths.t -> (IR.Pvar.t * IR.Typ.t) list -> (IR.Exp.t * IR.Typ.t) list -> BufferOverrunDomain.Mem.t -> mode:eval_mode -> BufferOverrunDomain.eval_sym_trace: Make eval_sym function for on-demand symbol evaluation

val mk_eval_sym_cost : IR.Typ.IntegerWidths.t -> (IR.Pvar.t * IR.Typ.t) list -> (IR.Exp.t * IR.Typ.t) list -> BufferOverrunDomain.Mem.t -> BufferOverrunDomain.eval_sym_trace: Make eval_sym function of EvalCost mode for on-demand symbol evaluation

module Prune : sig ... end

`\|` `EvalNormal`	Given a symbolic value of an unknown function `Symb.SymbolPath.Callsite`, it returns a symbolic interval value.
`\|` `EvalPOCond`	Given a symbolic value of an unknown function, it returns the top interval value. This is used when substituting condition expressions of proof obligations.
`\|` `EvalPOReachability`	This is similar to `EvalPOCond`, but it returns the bottom location, instead of the unknown location, when a location to substitute is not found. This is used when substituting reachabilities of proof obligations.
`\|` `EvalCost`	This is similar to `EvalNormal`, but it is designed to be used in substitutions of the cost results, avoiding precision loss by joining of symbolic values. Normal join of two different symbolic values, `s1` and `s2`, becomes top due to the limitation of our domain. On the other hand, in this mode, it returns an upperbound `s1+s2` for the case, because the cost values only care about the upperbounds.