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>PulseAbductiveDomain (infer.Pulselib.PulseAbductiveDomain)</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>»<ahref="../index.html">Pulselib</a>» PulseAbductiveDomain</nav><h1>Module <code>Pulselib.PulseAbductiveDomain</code></h1></header><divclass="spec module"id="module-F"><ahref="#module-F"class="anchor"></a><code><spanclass="keyword">module</span> F = Stdlib.Format</code></div><divclass="spec module"id="module-BaseAddressAttributes"><ahref="#module-BaseAddressAttributes"class="anchor"></a><code><spanclass="keyword">module</span> BaseAddressAttributes = <ahref="../index.html#module-PulseBaseAddressAttributes">PulseBaseAddressAttributes</a></code></div><divclass="spec module"id="module-BaseDomain"><ahref="#module-BaseDomain"class="anchor"></a><code><spanclass="keyword">module</span> BaseDomain = <ahref="../index.html#module-PulseBaseDomain">PulseBaseDomain</a></code></div><divclass="spec module"id="module-BaseMemory"><ahref="#module-BaseMemory"class="anchor"></a><code><spanclass="keyword">module</span> BaseMemory = <ahref="../index.html#module-PulseBaseMemory">PulseBaseMemory</a></code></div><divclass="spec module"id="module-BaseStack"><ahref="#module-BaseStack"class="anchor"></a><code><spanclass="keyword">module</span> BaseStack = <ahref="../index.html#module-PulseBaseStack">PulseBaseStack</a></code></div><aside><p>Layer on top of <ahref="BaseDomain/index.html"><code>BaseDomain</code></a> to propagate operations on the current state to the pre-condition when necessary</p><p>The abstract type <code>t</code> is a pre/post pair in the style of biabduction.</p></aside><dl><dtclass="spec module-type"id="module-type-BaseDomainSig"><ahref="#module-type-BaseDomainSig"class="anchor"></a><code><spanclass="keyword">module</span><spanclass="keyword">type</span><ahref="module-type-BaseDomainSig/index.html">BaseDomainSig</a> = <spanclass="keyword">sig</span> ... <spanclass="keyword">end</span></code></dt><dd><p>signature common to the "normal"<code>Domain</code>, representing the post at the current program point, and the inverted <code>PreDomain</code>, representing the inferred pre-condition</p></dd></dl><dl><dtclass="spec module"id="module-PostDomain"><ahref="#module-PostDomain"class="anchor"></a><code><spanclass="keyword">module</span><ahref="PostDomain/index.html">PostDomain</a> : <ahref="index.html#module-type-BaseDomainSig">BaseDomainSig</a></code></dt><dd><p>The post abstract state at each program point, or current state.</p></dd></dl><dl><dtclass="spec module"id="module-PreDomain"><ahref="#module-PreDomain"class="anchor"></a><code><spanclass="keyword">module</span><ahref="PreDomain/index.html">PreDomain</a> : <ahref="index.html#module-type-BaseDomainSig">BaseDomainSig</a></code></dt><dd><p>The inferred pre-condition at each program point, biabduction style.</p></dd></dl><dl><dtclass="spec type"id="type-t"><ahref="#type-t"class="anchor"></a><code><spanclass="keyword">type</span> t</code><code> = <spanclass="keyword">private</span></code><code>{</code><tableclass="record"><trid="type-t.post"class="anchored"><tdclass="def field"><ahref="#type-t.post"class="anchor"></a><code>post : <ahref="PostDomain/index.html#type-t">PostDomain.t</a>;</code></td><tdclass="doc"><p>state at the current program point</p></td></tr><trid="type-t.pre"class="anchored"><tdclass="def field"><ahref="#type-t.pre"class="anchor"></a><code>pre : <ahref="PreDomain/index.html#type-t">PreDomain.t</a>;</code></td><tdclass="doc"><p>inferred pre at the current program point</p></td></tr><trid="type-t.skipped_calls"class="anchored"><tdclass="def field"><ahref="#type-t.skipped_calls"class="anchor"></a><code>skipped_calls : <ahref="../PulseSkippedCalls/index.html#type-t">PulseBasicInterface.SkippedCalls.t</a>;</code></td><tdclass="doc"><p>set of skipped calls</p></td></tr><trid="type-t.path_condition"class="anchored"><tdclass="def field"><ahref="#type-t.path_condition"class="anchor"></a><code>path_condition : <ahref="../PulsePathCondition/index.html#type-t">PulseBasicInterface.PathCondition.t</a>;</code></td><tdclass="doc"><p>arithmetic facts</p></td></tr></table><code>}</code></dt><dd><p>biabduction-style pre/post state + skipped calls</p></dd></dl><dl><dtclass="spec value"id="val-leq"><ahref="#val-leq"class="anchor"></a><code><spanclass="keyword">val</span> leq : <span>lhs:<ahref="index.html#type-t">t</a></span><span>-></span><span>rhs:<ahref="index.html#type-t">t</a></span><span>-></span> bool</code></dt><dtclass="spec value"id="val-pp"><ahref="#val-pp"class="anchor"></a><code><spanclass="keyword">val</span> pp : Stdlib.Format.formatter <span>-></span><ahref="index.html#type-t">t</a><span>-></span> unit</code></dt><dtclass="spec value"id="val-mk_initial"><ahref="#val-mk_initial"class="anchor"></a><code><spanclass="keyword">val</span> mk_initial : <ahref="../../IR/Procdesc/index.html#type-t">IR.Procdesc.t</a><span>-></span><ahref="index.html#type-t">t</a></code></dt><dtclass="spec value"id="val-get_pre"><ahref="#val-get_pre"class="anchor"></a><code><spanclass="keyword">val</span> get_pre : <ahref="index.html#type-t">t</a><span>-></span><ahref="../PulseBaseDomain/index.html#type-t">BaseDomain.t</a></code></dt><dtclass="spec value"id="val-get_post"><ahref="#val-get_post"class="anchor"></a><code><spanclass="keyword">val</span> get_post : <ahref="index.html#type-t">t</a><span>-></span><ahref="../PulseBaseDomain/index.html#type-t">BaseDomain.t</a></code></dt></dl><dl><dtclass="spec module"id="module-Stack"><ahref="#module-Stack"class="anchor"></a><code><spanclass="keyword">module</span><ahref="Stack/index.html">Stack</a> : <spanclass="keyword">sig</span> ... <spanclass="keyword">end</span></code></dt><dd><p>stack operations like <ahref="BaseStack/index.html"><code>BaseStack</code></a> but that also take care of propagating facts to the precondition</p></dd></dl><dl><dtclass="spec module"id="module-Memory"><ahref="#module-Memory"class="anchor"></a><code><spanclass="keyword">module</span><ahref="Memory/index.html">Memory</a> : <spanclass="keyword">sig</span> ... <spanclass="keyword">end</span></code></dt><dd><p>memory operations like <ahref="BaseMemory/index.html"><code>BaseMemory</code></a> but that also take care of propagating facts to the precondition</p></dd></dl><dl><dtclass="spec module"id="module-AddressAttributes"><ahref="#module-AddressAttributes"class="anchor"></a><code><spanclass="keyword">module</span><ahref="AddressAttributes/index.html">AddressAttributes</a> : <spanclass="keyword">sig</span> ... <spanclass="keyword">end</span></code></dt><dd><p>attribute operations like <ahref="BaseAddressAttributes/index.html"><code>BaseAddressAttributes</code></a> but that also take care of propagating facts to the precondition</p></dd></dl><dl><dtclass="spec value"id="val-is_local"><ahref="#val-is_local"class="anchor"></a><code><spanclass="keyword">val</span> is_local : <ahref="../../IR/Var/index.html#type-t">IR.Var.t</a><span>-></span><ahref="index.html#type-t">t</a><span>-></span> bool</code></dt><dtclass="spec value"id="val-find_post_cell_opt"><ahref="#val-find_post_cell_opt"class="anchor"></a><code><spanclass="keyword">val</span> find_post_cell_opt : <ahref="../PulseAbstractValue/index.html#type-t">PulseBasicInterface.AbstractValue.t</a><span>-></span><ahref="index.html#type-t">t</a><span>-></span><span><ahref="../PulseBaseDomain/index.html#type-cell">BaseDomain.cell</a> option</span></code></dt><dtclass="spec value"id="val-discard_unreachable"><ahref="#val-discard_unreachable"class="anchor"></a><code><spanclass="keyword">val</span> discard_unreachable : <ahref="index.html#type-t">t</a><span>-></span><ahref="index.html#type-t">t</a> * <ahref="../../Pulselib__PulseAbstractValue/index.html#module-Set">Pulselib.PulseBasicInterface.AbstractValue.Set</a>.t * <span><ahref="../PulseAbstractValue/index.html#type-t">PulseBasicInterface.AbstractValue.t</a> list</span></code></dt><dd><p>garbage collect unreachable addresses in the state to make it smaller and return the new state, the live addresses, and the discarded addresses that used to have attributes attached</p></dd></dl><dl><dtclass="spec value"id="val-add_skipped_call"><ahref="#val-add_skipped_call"class="anchor"></a><code><spanclass="keyword">val</span> add_skipped_call : <ahref="../../IR/Procname/index.html#type-t">IR.Procname.t</a><span>-></span><ahref="../PulseTrace/index.html#type-t">PulseBasicInterface.Trace.t</a><span>-></span><ahref="index.html#type-t">t</a><span>-></span><ahref="index.html#type-t">t</a></code></dt><dtclass="spec value"id="val-add_skipped_calls"><ahref="#val-add_skipped_calls"class="anchor"></a><code><spanclass="keyword">val</span> add_skipped_calls : <ahref="../PulseSkippedCalls/index.html#type-t">PulseBasicInterface.SkippedCalls.t</a><span>-></span><ahref="index.html#type-t">t</a><span>-></span><ahref="index.html#type-t">t</a></code></dt><dtclass="spec value"id="val-set_path_condition"><ahref="#val-set_path_condition"class="anchor"></a><code><spanclass="keyword">val</span> set_path_condition : <ahref="../PulsePathCondition/index.html#type-t">PulseBasicInterface.PathCondition.t</a><span>-></span><ahref="index.html#type-t">t</a><span>-></span><ahref="index.html#type-t">t</a></code></dt><dtclass="spec value"id="val-of_post"><ahref="#val-of_post"class="anchor"></a><code><spanclass="keyword">val</span> of_post : <ahref="../../IR/Procdesc/index.html#type-t">IR.Procdesc.t</a><span>-></span><ahref="index.html#type-t">t</a><span>-></span><ahref="index.html#type-t">t</a></code></dt><dtclass="spec value"id="val-set_post_edges"><ahref="#val-set_post_edges"class="anchor"></a><code><spanclass="keyword">val</span> set_post_edges : <ahref="../PulseAbstractValue/index.html#type-t">PulseBasicInterface.AbstractValue.t</a><span>-></span><ahref="../../Pulselib__PulseBaseMemory/Edges/index.html#type-t">BaseMemory.Edges.t</a><span>-></span><ahref="index.html#type-t">t</a><span>-></span><ahref="index.html#type-t">t</a></code></dt><dd><p>directly set the edges for the given address, bypassing abduction altogether</p></dd></dl><dl><dtclass="spec value"id="val-set_post_cell"><ahref="#val-set_post_cell"class="anchor"></a><code><spanclass="keyword">val</span> set_post_cell : <span>(<ahref="../PulseAbstractValue/index.html#type-t">PulseBasicInterface.AbstractValue.t</a> * <ahref="../PulseValueHistory/index.html#type-t">PulseBasicInterface.ValueHistory.t</a>)</span><span>-></span><ahref="../PulseBaseDomain/index.html#type-cell">BaseDomain.cell</a><span>-></span><ahref="../../IBase/Location/index.html#type-t">IBase.Location.t</a><span>-></span><ahref="index.html#type-t">t</a><span>-></span><ahref="index.html#type-t">t</a></code></dt><dd><p>directly set the edges and attributes for the given address, bypassing abduction altogether</p></dd></dl></div></body></html>
