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>PulseTopl (infer.Pulselib.PulseTopl)</title><linkrel="stylesheet"href="../../../odoc.css"/><metacharset="utf-8"/><metaname="generator"content="odoc 1.5.1"/><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>»<ahref="../index.html">Pulselib</a>» PulseTopl</nav><h1>Module <code>Pulselib.PulseTopl</code></h1></header><dl><dtclass="spec type"id="type-value"><ahref="#type-value"class="anchor"></a><code><spanclass="keyword">type</span> value</code><code> = <ahref="../PulseAbstractValue/index.html#type-t">PulseAbstractValue.t</a></code></dt><dtclass="spec type"id="type-event"><ahref="#type-event"class="anchor"></a><code><spanclass="keyword">type</span> event</code><code> = </code><tableclass="variant"><trid="type-event.ArrayWrite"class="anchored"><tdclass="def constructor"><ahref="#type-event.ArrayWrite"class="anchor"></a><code>| </code><code><spanclass="constructor">ArrayWrite</span><spanclass="keyword">of</span></code><code>{</code><tableclass="record"><trid="type-event.aw_array"class="anchored"><tdclass="def field"><ahref="#type-event.aw_array"class="anchor"></a><code>aw_array : <ahref="index.html#type-value">value</a>;</code></td></tr><trid="type-event.aw_index"class="anchored"><tdclass="def field"><ahref="#type-event.aw_index"class="anchor"></a><code>aw_index : <ahref="index.html#type-value">value</a>;</code></td></tr></table><code>}</code></td></tr><trid="type-event.Call"class="anchored"><tdclass="def constructor"><ahref="#type-event.Call"class="anchor"></a><code>| </code><code><spanclass="constructor">Call</span><spanclass="keyword">of</span></code><code>{</code><tableclass="record"><trid="type-event.return"class="anchored"><tdclass="def field"><ahref="#type-event.return"class="anchor"></a><code>return : <span><ahref="index.html#type-value">value</a> option</span>;</code></td></tr><trid="type-event.arguments"class="anchored"><tdclass="def field"><ahref="#type-event.arguments"class="anchor"></a><code>arguments : <span><ahref="index.html#type-value">value</a> list</span>;</code></td></tr><trid="type-event.procname"class="anchored"><tdclass="def field"><ahref="#type-event.procname"class="anchor"></a><code>procname : <ahref="../../IR/Procname/index.html#type-t">IR.Procname.t</a>;</code></td></tr></table><code>}</code></td></tr></table></dt><dtclass="spec type"id="type-state"><ahref="#type-state"class="anchor"></a><code><spanclass="keyword">type</span> state</code></dt></dl><div><divclass="spec include"><divclass="doc"><dl><dtclass="spec value"id="val-compare_state"><ahref="#val-compare_state"class="anchor"></a><code><spanclass="keyword">val</span> compare_state : <ahref="index.html#type-state">state</a><span>-></span><ahref="index.html#type-state">state</a><span>-></span> int</code></dt><dtclass="spec value"id="val-equal_state"><ahref="#val-equal_state"class="anchor"></a><code><spanclass="keyword">val</span> equal_state : <ahref="index.html#type-state">state</a><span>-></span><ahref="index.html#type-state">state</a><span>-></span> bool</code></dt></dl></div></div></div><dl><dtclass="spec value"id="val-start"><ahref="#val-start"class="anchor"></a><code><spanclass="keyword">val</span> start : unit <span>-></span><ahref="index.html#type-state">state</a></code></dt><dd><p>Return the initial state of <code>Topl.automaton ()</code>.</p></dd></dl><dl><dtclass="spec value"id="val-small_step"><ahref="#val-small_step"class="anchor"></a><code><spanclass="keyword">val</span> small_step : <ahref="../../IBase/Location/index.html#type-t">IBase.Location.t</a><span>-></span><ahref="../PulsePathCondition/index.html#type-t">PulsePathCondition.t</a><span>-></span><ahref="index.html#type-event">event</a><span>-></span><ahref="index.html#type-state">state</a><span>-></span><ahref="index.html#type-state">state</a></code></dt><dtclass="spec value"id="val-large_step"><ahref="#val-large_step"class="anchor"></a><code><spanclass="keyword">val</span> large_step : <span>call_location:<ahref="../../IBase/Location/index.html#type-t">IBase.Location.t</a></span><span>-></span><span>callee_proc_name:<ahref="../../IR/Procname/index.html#type-t">IR.Procname.t</a></span><span>-></span><span>substitution:<span><span>(<ahref="index.html#type-value">value</a> * <ahref="../PulseValueHistory/index.html#type-t">PulseValueHistory.t</a>)</span><ahref="../../Pulselib__PulseAbstractValue/index.html#module-Map">Pulselib.PulseAbstractValue.Map</a>.t</span></span><span>-></span><span>condition:<ahref="../PulsePathCondition/index.html#type-t">PulsePathCondition.t</a></span><span>-></span><span>callee_prepost:<ahref="index.html#type-state">state</a></span><span>-></span><ahref="index.html#type-state">state</a><span>-></span><ahref="index.html#type-state">state</a></code></dt><dd><p><code>large_step ~substitution ~condition state ~callee_prepost</code> updates <code>state</code> according to <code>callee_prepost</code>. The abstract values in <code>condition</code> and <code>state</code> are in one scope, and those in <code>callee_prepost</code> in another scope: the <code>substitution</code> maps from the callee scope to the condition&state scope.</p></dd></dl><dl><dtclass="spec value"id="val-filter_for_summary"><ahref="#val-filter_for_summary"class="anchor"></a><code><spanclass="keyword">val</span> filter_for_summary : <ahref="../PulsePathCondition/index.html#type-t">PulsePathCondition.t</a><span>-></span><ahref="index.html#type-state">state</a><span>-></span><ahref="index.html#type-state">state</a></code></dt><dd><p>Remove from state those parts that are inconsistent with the path condition. (We do a cheap check to not introduce inconsistent Topl states, but they mey become inconsistent because the program path condition is updated later.)</p></dd></dl><dl><dtclass="spec value"id="val-simplify"><ahref="#val-simplify"class="anchor"></a><code><spanclass="keyword">val</span> simplify : <span>keep:<ahref="../../Pulselib__PulseAbstractValue/index.html#module-Set">Pulselib.PulseAbstractValue.Set</a>.t</span><span>-></span><ahref="index.html#type-state">state</a><span>-></span><ahref="index.html#type-state">state</a></code></dt><dd><p>Keep only a subset of abstract values. This is used for extracting summaries.</p></dd></dl><dl><dtclass="spec value"id="val-report_errors"><ahref="#val-report_errors"class="anchor"></a><code><spanclass="keyword">val</span> report_errors : <ahref="../../IR/Procdesc/index.html#type-t">IR.Procdesc.t</a><span>-></span><ahref="../../Absint/Errlog/index.html#type-t">Absint.Errlog.t</a><span>-></span><ahref="index.html#type-state">state</a><span>-></span> unit</code></dt><dd><p>Calls <code>Reporting.log_issue</code> with error traces, if any.</p></dd></dl><dl><dtclass="spec value"id="val-pp_state"><ahref="#val-pp_state"class="anchor"></a><code><spanclass="keyword">val</span> pp_state : Stdlib.Format.formatter <span>-></span><ahref="index.html#type-state">state</a><span>-></span> unit</code></dt></dl></div></body></html>
