infer_clone/website/static/odoc/next/infer/Biabduction/State/index.html

<!DOCTYPE html>
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>State (infer.Biabduction.State)</title><link rel="stylesheet" href="../../../odoc.css"/><meta charset="utf-8"/><meta name="generator" content="odoc 1.5.0"/><meta name="viewport" content="width=device-width,initial-scale=1.0"/><script src="../../../highlight.pack.js"></script><script>hljs.initHighlightingOnLoad();</script></head><body><div class="content"><header><nav><a href="../index.html">Up</a> – <a href="../../index.html">infer</a> &#x00BB; <a href="../index.html">Biabduction</a> &#x00BB; State</nav><h1>Module <code>Biabduction.State</code></h1></header><aside><p>State of symbolic execution</p></aside><dl><dt class="spec type" id="type-t"><a href="#type-t" class="anchor"></a><code><span class="keyword">type</span> t</code></dt><dd><p>Internal state</p></dd></dl><dl><dt class="spec value" id="val-add_diverging_states"><a href="#val-add_diverging_states" class="anchor"></a><code><span class="keyword">val</span> add_diverging_states : <a href="../Paths/PathSet/index.html#type-t">Paths.PathSet.t</a> <span>&#45;&gt;</span> unit</code></dt><dd><p>Add diverging states</p></dd></dl><dl><dt class="spec value" id="val-get_diverging_states_node"><a href="#val-get_diverging_states_node" class="anchor"></a><code><span class="keyword">val</span> get_diverging_states_node : unit <span>&#45;&gt;</span> <a href="../Paths/PathSet/index.html#type-t">Paths.PathSet.t</a></code></dt><dd><p>Get the diverging states for the node</p></dd></dl><dl><dt class="spec value" id="val-get_diverging_states_proc"><a href="#val-get_diverging_states_proc" class="anchor"></a><code><span class="keyword">val</span> get_diverging_states_proc : unit <span>&#45;&gt;</span> <a href="../Paths/PathSet/index.html#type-t">Paths.PathSet.t</a></code></dt><dd><p>Get the diverging states for the procedure</p></dd></dl><dl><dt class="spec value" id="val-get_inst_update"><a href="#val-get_inst_update" class="anchor"></a><code><span class="keyword">val</span> get_inst_update : <a href="../../IR/PredSymb/index.html#type-path_pos">IR.PredSymb.path_pos</a> <span>&#45;&gt;</span> <a href="../Predicates/index.html#type-inst">Predicates.inst</a></code></dt><dd><p>Get update instrumentation for the current loc</p></dd></dl><dl><dt class="spec value" id="val-get_loc_trace"><a href="#val-get_loc_trace" class="anchor"></a><code><span class="keyword">val</span> get_loc_trace : unit <span>&#45;&gt;</span> <a href="../../Absint/Errlog/index.html#type-loc_trace">Absint.Errlog.loc_trace</a></code></dt><dd><p>Get the location trace of the last path seen in symbolic execution</p></dd></dl><dl><dt class="spec value" id="val-get_normalized_pre"><a href="#val-get_normalized_pre" class="anchor"></a><code><span class="keyword">val</span> get_normalized_pre : <span>(<a href="../../IR/Tenv/index.html#type-t">IR.Tenv.t</a> <span>&#45;&gt;</span> <span><a href="../Prop/index.html#type-normal">Prop.normal</a> <a href="../Prop/index.html#type-t">Prop.t</a></span> <span>&#45;&gt;</span> <span><a href="../Prop/index.html#type-normal">Prop.normal</a> <a href="../Prop/index.html#type-t">Prop.t</a></span>)</span> <span>&#45;&gt;</span> <span><span><a href="../Prop/index.html#type-normal">Prop.normal</a> <a href="../Prop/index.html#type-t">Prop.t</a></span> option</span></code></dt><dd><p>return the normalized precondition extracted form the last prop seen, if any the abstraction function is a parameter to get around module dependencies</p></dd></dl><dl><dt class="spec value" id="val-get_path"><a href="#val-get_path" class="anchor"></a><code><span class="keyword">val</span> get_path : unit <span>&#45;&gt;</span> <a href="../Paths/Path/index.html#type-t">Paths.Path.t</a> * <span><a href="../../IR/PredSymb/index.html#type-path_pos">IR.PredSymb.path_pos</a> option</span></code></dt><dd><p>Get last path seen in symbolic execution</p></dd></dl><dl><dt class="spec value" id="val-get_path_pos"><a href="#val-get_path_pos" class="anchor"></a><code><span class="keyword">val</span> get_path_pos : unit <span>&#45;&gt;</span> <a href="../../IR/PredSymb/index.
[website] docs for current master Summary: Run `make doc-publish` and adjust links in website/docs/04-internal-API.md to point to odoc/next/infer/infer.html as the starting point of the docs has changed (was: odoc/index.html but now this also contains dead links to sledge and ppx_trace... also infer.mld is a me-written exposé of the various libraries and index.mld is an auto-generated list of all the modules now). Reviewed By: ngorogiannis Differential Revision: D21552864 fbshipit-source-id: c3977f645 5 years ago				`<!DOCTYPE html>`
[website] make doc-publish Summary: New website! Now with one page per checker, and only one page containing all issue types for easy tooling. Each checker page also lists the issue types it can report. For now only issue types with documentation appear in either page, filling these up is still TODO. Reviewed By: mityal Differential Revision: D21934465 fbshipit-source-id: 82ae1e417 5 years ago				<html xmlns="http://www.w3.org/1999/xhtml"><head><title>State (infer.Biabduction.State)</title><link rel="stylesheet" href="../../../odoc.css"/><meta charset="utf-8"/><meta name="generator" content="odoc 1.5.0"/><meta name="viewport" content="width=device-width,initial-scale=1.0"/><script src="../../../highlight.pack.js"></script><script>hljs.initHighlightingOnLoad();</script></head><body><div class="content"><header><nav><a href="../index.html">Up</a> – <a href="../../index.html">infer</a> » <a href="../index.html">Biabduction</a> » State</nav><h1>Module <code>Biabduction.State</code></h1></header><aside><p>State of symbolic execution</p></aside><dl><dt class="spec type" id="type-t"><a href="#type-t" class="anchor"></a><code><span class="keyword">type</span> t</code></dt><dd><p>Internal state</p></dd></dl><dl><dt class="spec value" id="val-add_diverging_states"><a href="#val-add_diverging_states" class="anchor"></a><code><span class="keyword">val</span> add_diverging_states : <a href="../Paths/PathSet/index.html#type-t">Paths.PathSet.t</a> <span>-></span> unit</code></dt><dd><p>Add diverging states</p></dd></dl><dl><dt class="spec value" id="val-get_diverging_states_node"><a href="#val-get_diverging_states_node" class="anchor"></a><code><span class="keyword">val</span> get_diverging_states_node : unit <span>-></span> <a href="../Paths/PathSet/index.html#type-t">Paths.PathSet.t</a></code></dt><dd><p>Get the diverging states for the node</p></dd></dl><dl><dt class="spec value" id="val-get_diverging_states_proc"><a href="#val-get_diverging_states_proc" class="anchor"></a><code><span class="keyword">val</span> get_diverging_states_proc : unit <span>-></span> <a href="../Paths/PathSet/index.html#type-t">Paths.PathSet.t</a></code></dt><dd><p>Get the diverging states for the procedure</p></dd></dl><dl><dt class="spec value" id="val-get_inst_update"><a href="#val-get_inst_update" class="anchor"></a><code><span class="keyword">val</span> get_inst_update : <a href="../../IR/PredSymb/index.html#type-path_pos">IR.PredSymb.path_pos</a> <span>-></span> <a href="../Predicates/index.html#type-inst">Predicates.inst</a></code></dt><dd><p>Get update instrumentation for the current loc</p></dd></dl><dl><dt class="spec value" id="val-get_loc_trace"><a href="#val-get_loc_trace" class="anchor"></a><code><span class="keyword">val</span> get_loc_trace : unit <span>-></span> <a href="../../Absint/Errlog/index.html#type-loc_trace">Absint.Errlog.loc_trace</a></code></dt><dd><p>Get the location trace of the last path seen in symbolic execution</p></dd></dl><dl><dt class="spec value" id="val-get_normalized_pre"><a href="#val-get_normalized_pre" class="anchor"></a><code><span class="keyword">val</span> get_normalized_pre : <span>(<a href="../../IR/Tenv/index.html#type-t">IR.Tenv.t</a> <span>-></span> <span><a href="../Prop/index.html#type-normal">Prop.normal</a> <a href="../Prop/index.html#type-t">Prop.t</a></span> <span>-></span> <span><a href="../Prop/index.html#type-normal">Prop.normal</a> <a href="../Prop/index.html#type-t">Prop.t</a></span>)</span> <span>-></span> <span><span><a href="../Prop/index.html#type-normal">Prop.normal</a> <a href="../Prop/index.html#type-t">Prop.t</a></span> option</span></code></dt><dd><p>return the normalized precondition extracted form the last prop seen, if any the abstraction function is a parameter to get around module dependencies</p></dd></dl><dl><dt class="spec value" id="val-get_path"><a href="#val-get_path" class="anchor"></a><code><span class="keyword">val</span> get_path : unit <span>-></span> <a href="../Paths/Path/index.html#type-t">Paths.Path.t</a> * <span><a href="../../IR/PredSymb/index.html#type-path_pos">IR.PredSymb.path_pos</a> option</span></code></dt><dd><p>Get last path seen in symbolic execution</p></dd></dl><dl><dt class="spec value" id="val-get_path_pos"><a href="#val-get_path_pos" class="anchor"></a><code><span class="keyword">val</span> get_path_pos : unit <span>-></span> <a href="../../IR/PredSymb/index.