This file contains ambiguous Unicode characters that may be confused with others in your current locale. If your use case is intentional and legitimate, you can safely ignore this warning. Use the Escape button to highlight these characters.
<!DOCTYPE html>
<htmlxmlns="http://www.w3.org/1999/xhtml"><head><title>BO__BufferOverrunSemantics (infer.BO__BufferOverrunSemantics)</title><linkrel="stylesheet"href="../../odoc.css"/><metacharset="utf-8"/><metaname="generator"content="odoc 1.5.0"/><metaname="viewport"content="width=device-width,initial-scale=1.0"/><scriptsrc="../../highlight.pack.js"></script><script>hljs.initHighlightingOnLoad();</script></head><body><divclass="content"><header><nav><ahref="../index.html">Up</a>–<ahref="../index.html">infer</a>» BO__BufferOverrunSemantics</nav><h1>Module <code>BO__BufferOverrunSemantics</code></h1></header><dl><dtclass="spec value"id="val-is_stack_exp"><ahref="#val-is_stack_exp"class="anchor"></a><code><spanclass="keyword">val</span> is_stack_exp : <ahref="../IR/Exp/index.html#type-t">IR.Exp.t</a><span>-></span><ahref="../BO/BufferOverrunDomain/Mem/index.html#type-t">BO.BufferOverrunDomain.Mem.t</a><span>-></span> bool</code></dt><dd><p>Check if an expression is a stack variable such as <code>n$0</code> or local variable for C array</p></dd></dl><dl><dtclass="spec value"id="val-eval"><ahref="#val-eval"class="anchor"></a><code><spanclass="keyword">val</span> eval : <ahref="../IR/Typ/IntegerWidths/index.html#type-t">IR.Typ.IntegerWidths.t</a><span>-></span><ahref="../IR/Exp/index.html#type-t">IR.Exp.t</a><span>-></span><ahref="../BO/BufferOverrunDomain/Mem/index.html#type-t">BO.BufferOverrunDomain.Mem.t</a><span>-></span><ahref="../BO/BufferOverrunDomain/Val/index.html#type-t">BO.BufferOverrunDomain.Val.t</a></code></dt><dd><p>Evalute an expression</p></dd></dl><dl><dtclass="spec value"id="val-eval_locs"><ahref="#val-eval_locs"class="anchor"></a><code><spanclass="keyword">val</span> eval_locs : <ahref="../IR/Exp/index.html#type-t">IR.Exp.t</a><span>-></span><ahref="../BO/BufferOverrunDomain/Mem/index.html#type-t">BO.BufferOverrunDomain.Mem.t</a><span>-></span><ahref="../BO/AbsLoc/PowLoc/index.html#type-t">BO.AbsLoc.PowLoc.t</a></code></dt><dd><p><code>eval_locs exp mem</code> is like <code>eval exp mem |> Val.get_all_locs</code> but takes some shortcuts to avoid computing useless and/or problematic intermediate values</p></dd></dl><dl><dtclass="spec value"id="val-eval_arr"><ahref="#val-eval_arr"class="anchor"></a><code><spanclass="keyword">val</span> eval_arr : <ahref="../IR/Typ/IntegerWidths/index.html#type-t">IR.Typ.IntegerWidths.t</a><span>-></span><ahref="../IR/Exp/index.html#type-t">IR.Exp.t</a><span>-></span><ahref="../BO/BufferOverrunDomain/Mem/index.html#type-t">BO.BufferOverrunDomain.Mem.t</a><span>-></span><ahref="../BO/BufferOverrunDomain/Val/index.html#type-t">BO.BufferOverrunDomain.Val.t</a></code></dt><dd><p>Return the array value of the input expression. For example, when <code>x</code> is a program variable, <code>eval_arr x</code> returns array blocks the <code>x</code> is pointing to, on the other hand, <code>eval x</code> returns the abstract location of <code>x</code>.</p></dd></dl><dl><dtclass="spec value"id="val-eval_lindex"><ahref="#val-eval_lindex"class="anchor"></a><code><spanclass="keyword">val</span> eval_lindex : <ahref="../IR/Typ/IntegerWidths/index.html#type-t">IR.Typ.IntegerWidths.t</a><span>-></span><ahref="../IR/Exp/index.html#type-t">IR.Exp.t</a><span>-></span><ahref="../IR/Exp/index.html#type-t">IR.Exp.t</a><span>-></span><ahref="../BO/BufferOverrunDomain/Mem/index.html#type-t">BO.BufferOverrunDomain.Mem.t</a><span>-></span><ahref="../BO/BufferOverrunDomain/Val/index.html#type-t">BO.BufferOverrunDomain.Val.t</a></code></dt><dd><p>Evaluate array location with index, i.e., <code>eval_lindex integer_type_widths array_exp index_exp mem</code></p></dd></dl><dl><dtclass="spec value"id="val-eval_array_locs_length"><ahref="#val-eval_array_locs_length"class="anchor"></a><code><spanclass="keyword">val</span> eval_array_locs_length : <ahref="../BO/AbsLoc/PowLoc/index.html#type-t">BO.AbsLoc.PowLoc.t</a><span>-></span><span><spanclass="type-var">_</span><ahref="../BO/BufferOverrunDomain/Mem/index.html#type-t0">BO.BufferOverrunDomain.Mem.t0</a></span><span>-></span><ahref="../BO/BufferOverrunDomain/Val/index.html#type-t">BO.BufferOverrunDomain.Val.t</a></code></dt><dd><p>Evaluate length of array locations</p></dd></dl><dl><dtclass="spec value"id="val-conservative_array_length"><ahref="#val-conservative_array_length"class="anchor"></a><code><spanclass="keyword">val</span> conservative_array_length : <span>?⁠traces:<ahref="../BO/BufferOverrunTrace/Set/index.html#type-t">BO.BufferOverrunTrace.Set.t</a></span><span>-></span><ahref="../BO/AbsLoc/PowLoc/index.html#type-t">BO.AbsLoc.PowLoc.t</a><span>-></span><span><spanclass="type-var">_</span><ahref="../BO/BufferOverrunDomain/Mem/index.html#type-t0">BO.BufferOverrunDomain.Mem.t0</a></span><span>-></span><ahref="../BO/BufferOverrunDomain/Val/index.html#type-t">BO.BufferOverrunDomain.Val.t</a></code></dt><dd><p>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 <code>arr_locs</code> points to two arrays <code>a</code> and <code>b</code> and if their lengths are <code>a.length</code> and <code>b.length</code>, this function evaluates its length as <code>[0, a.length.ub + b.length.ub]</code>.</p></dd></dl><dl><dtclass="spec type"id="type-eval_mode"><ahref="#type-eval_mode"class="anchor"></a><code><spanclass="keyword">type</span> eval_mode</code><code> = </code><tableclass="variant"><trid="type-eval_mode.EvalNormal"class="anchored"><tdclass="def constructor"><ahref="#type-eval_mode.EvalNormal"class="anchor"></a><code>| </code><code><spanclass="constructor">EvalNormal</span></code></td><tdclass="doc"><p>Given a symbolic value of an unknown function <code>Symb.SymbolPath.Callsite</code>, it returns a symbolic interval value.</p></td></tr><trid="type-eval_mode.EvalPOCond"class="anchored"><tdclass="def constructor"><ahref="#type-eval_mode.EvalPOCond"class="anchor"></a><code>| </code><code><spanclass="constructor">EvalPOCond</span></code></td><tdclass="doc"><p>Given a symbolic value of an unknown function, it returns the top interval value. This is used when substituting condition expressions of proof obligations.</p></td></tr><trid="type-eval_mode.EvalPOReachability"class="anchored"><tdclass="def constructor"><ahref="#type-eval_mode.EvalPOReachability"class="anchor"></a><code>| </code><code><spanclass="constructor">EvalPOReachability</span></code></td><tdclass="doc"><p>This is similar to <code>EvalPOCond</code>, 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.</p></td></tr><trid="type-eval_mode.EvalCost"class="anchored"><tdclass="def constructor"><ahref="#type-eval_mode.EvalCost"class="anchor"></a><code>| </code><code><spanclass="constructor">EvalCost</span></code></td><tdclass="doc"><p>This is similar to <code>EvalNormal</code>, 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, <code>s1</code> and <code>s2</code>, becomes top due to the limitation of our domain. On the other hand, in this mode, it returns an upperbound <code>s1+s2</code> for the case, because the cost values only care about the upperbounds.</p></td></tr></table></dt><dd><p>Several modes of ondemand evaluations</p></dd></dl><dl><dtclass="spec value"id="val-mk_eval_sym_trace"><ahref="#val-mk_eval_sym_trace"class="anchor"></a><code><spanclass="keyword">val</span> mk_eval_sym_trace : <span>?⁠is_params_ref:bool</span><span>-></span><ahref="../IR/Typ/IntegerWidths/index.html#type-t">IR.Typ.IntegerWidths.t</a><span>-></span><span><span>(<ahref="../IR/Pvar/index.html#type-t">IR.Pvar.t</a> * <ahref="../IR/Typ/index.html#type-t">IR.Typ.t</a>)</span> list</span><span>-></span><span><span>(<ahref="../IR/Exp/index.html#type-t">IR.Exp.t</a> * <ahref="../IR/Typ/index.html#type-t">IR.Typ.t</a>)</span> list</span><span>-></span><ahref="../BO/BufferOverrunDomain/Mem/index.html#type-t">BO.BufferOverrunDomain.Mem.t</a><span>-></span><span>mode:<ahref="index.html#type-eval_mode">eval_mode</a></span><span>-></span><ahref="../BO/BufferOverrunDomain/index.html#type-eval_sym_trace">BO.BufferOverrunDomain.eval_sym_trace</a></code></dt><dd><p>Make <code>eval_sym</code> function for on-demand symbol evaluation</p></dd></dl><dl><dtclass="spec value"id="val-mk_eval_sym_cost"><ahref="#val-mk_eval_sym_cost"class="anchor"></a><code><spanclass="keyword">val</span> mk_eval_sym_cost : <ahref="../IR/Typ/IntegerWidths/index.html#type-t">IR.Typ.IntegerWidths.t</a><span>-></span><span><span>(<ahref="../IR/Pvar/index.html#type-t">IR.Pvar.t</a> * <ahref="../IR/Typ/index.html#type-t">IR.Typ.t</a>)</span> list</span><span>-></span><span><span>(<ahref="../IR/Exp/index.html#type-t">IR.Exp.t</a> * <ahref="../IR/Typ/index.html#type-t">IR.Typ.t</a>)</span> list</span><span>-></span><ahref="../BO/BufferOverrunDomain/Mem/index.html#type-t">BO.BufferOverrunDomain.Mem.t</a><span>-></span><ahref="../BO/Bounds/Bound/index.html#type-eval_sym">BO.Bounds.Bound.eval_sym</a></code></dt><dd><p>Make <code>eval_sym</code> function of <code>EvalCost</code> mode for on-demand symbol evaluation</p></dd></dl><divclass="spec module"id="module-Prune"><ahref="#module-Prune"class="anchor"></a><code><spanclass="keyword">module</span><ahref="Prune/index.html">Prune</a> : <spanclass="keyword">sig</span> ... <spanclass="keyword">end</span></code></div></div></body></html>
