|
|
<!DOCTYPE html>
|
|
|
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>Prop (infer.InferModules.Prop)</title><link rel="stylesheet" href="../../../odoc.css"/><meta charset="utf-8"/><meta name="viewport" content="width=device-width,initial-scale=1.0"/><meta name="generator" content="doc-ock-html v1.0.0-1-g1fc9bf0"/></head><body><nav id="top"><a href="../index.html">Up</a> — <span class="package">package <a href="../../index.html">infer</a></span></nav><header><h1><span class="keyword">Module</span> <span class="module-path">InferModules.Prop</span></h1></header><p>Functions for Propositions (i.e., Symbolic Heaps)</p><div class="spec type" id="type-normal"><a href="#type-normal" class="anchor"></a><div class="def type"><code><span class="keyword">type </span>normal</code><code></code><code></code></div><div class="doc"><p>kind for normal props, i.e. normalized</p></div></div><div class="spec type" id="type-exposed"><a href="#type-exposed" class="anchor"></a><div class="def type"><code><span class="keyword">type </span>exposed</code><code></code><code></code></div><div class="doc"><p>kind for exposed props</p></div></div><div class="spec type" id="type-sorted"><a href="#type-sorted" class="anchor"></a><div class="def type"><code><span class="keyword">type </span>sorted</code><code></code><code></code></div><div class="doc"><p>kind for sorted props</p></div></div><p>Proposition.</p><div class="spec type" id="type-pi"><a href="#type-pi" class="anchor"></a><div class="def type"><code><span class="keyword">type </span>pi</code><code><span class="keyword"> = </span><a href="../../../InferIR/InferIR/Sil/index.html#type-atom">InferIR.Sil.atom</a> list</code><code></code></div><div class="doc"></div></div><div class="spec type" id="type-sigma"><a href="#type-sigma" class="anchor"></a><div class="def type"><code><span class="keyword">type </span>sigma</code><code><span class="keyword"> = </span><a href="../../../InferIR/InferIR/Sil/index.html#type-hpred">InferIR.Sil.hpred</a> list</code><code></code></div><div class="doc"></div></div><div class="spec type" id="type-t"><a href="#type-t" class="anchor"></a><div class="def type"><code><span class="keyword">type </span>'a t</code><code></code><code><span class="keyword"> = </span><span class="keyword">private </span></code><code>{</code><table class="record"><tr id="type-t.sigma" class="anchored"><td class="def field"><a href="#type-t.sigma" class="anchor"></a><code>sigma : <a href="index.html#type-sigma">sigma</a>;</code></td><td class="doc"><p>(** spatial part *)</p></td></tr><tr id="type-t.sub" class="anchored"><td class="def field"><a href="#type-t.sub" class="anchor"></a><code>sub : <a href="../../../InferIR/InferIR/Sil/index.html#type-exp_subst">InferIR.Sil.exp_subst</a>;</code></td><td class="doc"><p>(** substitution *)</p></td></tr><tr id="type-t.pi" class="anchored"><td class="def field"><a href="#type-t.pi" class="anchor"></a><code>pi : <a href="index.html#type-pi">pi</a>;</code></td><td class="doc"><p>(** pure part *)</p></td></tr><tr id="type-t.sigma_fp" class="anchored"><td class="def field"><a href="#type-t.sigma_fp" class="anchor"></a><code>sigma_fp : <a href="index.html#type-sigma">sigma</a>;</code></td><td class="doc"><p>(** abduced spatial part *)</p></td></tr><tr id="type-t.pi_fp" class="anchored"><td class="def field"><a href="#type-t.pi_fp" class="anchor"></a><code>pi_fp : <a href="index.html#type-pi">pi</a>;</code></td><td class="doc"><p>(** abduced pure part *)</p></td></tr></table><code>}</code><code></code></div><div class="doc"><p>the kind 'a should range over <code class="code">normal</code> and <code class="code">exposed</code></p></div></div><div class="spec include"><div class="doc"></div><details open="open"><summary><span class="def"><code><span class="keyword">include </span><span class="keyword">sig</span> ... <span class="keyword">end</span></code></span></summary><div class="spec val" id="val-compare"><a href="#val-compare" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>compare : (<span class="type-var">'a</span> <span class="keyword">‑></span> <span class="type-var">'a</span> <span class="keyword">‑></span> int) <span class="keyword">‑></span> <span class="type-var">'a</span> <a href="index.html#type-t">t</a> <span class="keyword">‑></span> <span class="type-var">'a</span> <a href="index.html#type-t">t</a> <span class="keyword">‑></span> int</code></div><div class="doc"></div></div></details></div><div class="spec type" id="type-struct_init_mode"><a href="#type-struct_init_mode" class="anchor"></a><div class="def type"><code><span class="keyword">type </span>struct_init_mode</code><code></code><code><span class="keyword"> = </span></code><table class="variant"><tr id="type-struct_init_mode.No_init" class="anchored"><td class="def constructor"><a href="#type-struct_init_mode.No_init" class="anchor"></a><code><span class="keyword">| </span></code><code><span class="constructor">No_init</span></code></td></tr><tr id="type-struct_init_mode.Fld_init" class="anchored"><td class="def constructor"><a href="#type-struct_init_mode.Fld_init" class="anchor"></a><code><span class="keyword">| </span></code><code><span class="constructor">Fld_init</span></code></td></tr></table><code></code></div><div class="doc"><p>type to describe different strategies for initializing fields of a structure. <code class="code">No_init</code> does not
|
|
|
initialize any fields of the struct. <code class="code">Fld_init</code> initializes the fields of the struct with fresh
|
|
|
variables (C) or default values (Java).</p></div></div><h3>Basic Functions for propositions</h3><div class="spec val" id="val-compare_prop"><a href="#val-compare_prop" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>compare_prop : <span class="type-var">'a</span> <a href="index.html#type-t">t</a> <span class="keyword">‑></span> <span class="type-var">'a</span> <a href="index.html#type-t">t</a> <span class="keyword">‑></span> int</code></div><div class="doc"><p>Compare propositions</p></div></div><div class="spec val" id="val-equal_sigma"><a href="#val-equal_sigma" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>equal_sigma : <a href="index.html#type-sigma">sigma</a> <span class="keyword">‑></span> <a href="index.html#type-sigma">sigma</a> <span class="keyword">‑></span> bool</code></div><div class="doc"><p>Check the equality of two sigma's</p></div></div><div class="spec val" id="val-pp_sub"><a href="#val-pp_sub" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>pp_sub : <a href="../../../InferStdlib/InferStdlib/Pp/index.html#type-env">InferStdlib.Pp.env</a> <span class="keyword">‑></span> Format.formatter <span class="keyword">‑></span> <a href="../../../InferIR/InferIR/Sil/index.html#type-subst">InferIR.Sil.subst</a> <span class="keyword">‑></span> unit</code></div><div class="doc"><p>Pretty print a substitution.</p></div></div><div class="spec val" id="val-d_sub"><a href="#val-d_sub" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>d_sub : <a href="../../../InferIR/InferIR/Sil/index.html#type-subst">InferIR.Sil.subst</a> <span class="keyword">‑></span> unit</code></div><div class="doc"><p>Dump a substitution.</p></div></div><div class="spec val" id="val-pp_pi"><a href="#val-pp_pi" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>pp_pi : <a href="../../../InferStdlib/InferStdlib/Pp/index.html#type-env">InferStdlib.Pp.env</a> <span class="keyword">‑></span> Format.formatter <span class="keyword">‑></span> <a href="index.html#type-pi">pi</a> <span class="keyword">‑></span> unit</code></div><div class="doc"><p>Pretty print a pi.</p></div></div><div class="spec val" id="val-d_pi"><a href="#val-d_pi" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>d_pi : <a href="index.html#type-pi">pi</a> <span class="keyword">‑></span> unit</code></div><div class="doc"><p>Dump a pi.</p></div></div><div class="spec val" id="val-pp_sigma"><a href="#val-pp_sigma" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>pp_sigma : <a href="../../../InferStdlib/InferStdlib/Pp/index.html#type-env">InferStdlib.Pp.env</a> <span class="keyword">‑></span> Format.formatter <span class="keyword">‑></span> <a href="index.html#type-sigma">sigma</a> <span class="keyword">‑></span> unit</code></div><div class="doc"><p>Pretty print a sigma.</p></div></div><div class="spec val" id="val-d_sigma"><a href="#val-d_sigma" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>d_sigma : <a href="index.html#type-sigma">sigma</a> <span class="keyword">‑></span> unit</code></div><div class="doc"><p>Dump a sigma.</p></div></div><div class="spec val" id="val-d_pi_sigma"><a href="#val-d_pi_sigma" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>d_pi_sigma : <a href="index.html#type-pi">pi</a> <span class="keyword">‑></span> <a href="index.html#type-sigma">sigma</a> <span class="keyword">‑></span> unit</code></div><div class="doc"><p>Dump a pi and a sigma</p></div></div><div class="spec val" id="val-sigma_get_stack_nonstack"><a href="#val-sigma_get_stack_nonstack" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>sigma_get_stack_nonstack : bool <span class="keyword">‑></span> <a href="index.html#type-sigma">sigma</a> <span class="keyword">‑></span> <a href="index.html#type-sigma">sigma</a><span class="keyword"> * </span><a href="index.html#type-sigma">sigma</a></code></div><div class="doc"><p>Split sigma into stack and nonstack parts.
|
|
|
The boolean indicates whether the stack should only include local variales.</p></div></div><div class="spec val" id="val-prop_update_obj_sub"><a href="#val-prop_update_obj_sub" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>prop_update_obj_sub : <a href="../../../InferStdlib/InferStdlib/Pp/index.html#type-env">InferStdlib.Pp.env</a> <span class="keyword">‑></span> <span class="type-var">'a</span> <a href="index.html#type-t">t</a> <span class="keyword">‑></span> <a href="../../../InferStdlib/InferStdlib/Pp/index.html#type-env">InferStdlib.Pp.env</a></code></div><div class="doc"><p>Update the object substitution given the stack variables in the prop</p></div></div><div class="spec val" id="val-pp_prop"><a href="#val-pp_prop" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>pp_prop : <a href="../../../InferStdlib/InferStdlib/Pp/index.html#type-env">InferStdlib.Pp.env</a> <span class="keyword">‑></span> Format.formatter <span class="keyword">‑></span> <span class="type-var">'a</span> <a href="index.html#type-t">t</a> <span class="keyword">‑></span> unit</code></div><div class="doc"><p>Pretty print a proposition.</p></div></div><div class="spec val" id="val-pp_prop_with_typ"><a href="#val-pp_prop_with_typ" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>pp_prop_with_typ : <a href="../../../InferStdlib/InferStdlib/Pp/index.html#type-env">InferStdlib.Pp.env</a> <span class="keyword">‑></span> Format.formatter <span class="keyword">‑></span> <a href="index.html#type-normal">normal</a> <a href="index.html#type-t">t</a> <span class="keyword">‑></span> unit</code></div><div class="doc"><p>Pretty print a proposition with type information</p></div></div><div class="spec val" id="val-prop_pred_env"><a href="#val-prop_pred_env" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>prop_pred_env : <span class="type-var">'a</span> <a href="index.html#type-t">t</a> <span class="keyword">‑></span> <a href="../../../InferIR/InferIR/Sil/Predicates/index.html#type-env">InferIR.Sil.Predicates.env</a></code></div><div class="doc"><p>Create a predicate environment for a prop</p></div></div><div class="spec val" id="val-d_prop"><a href="#val-d_prop" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>d_prop : <span class="type-var">'a</span> <a href="index.html#type-t">t</a> <span class="keyword">‑></span> unit</code></div><div class="doc"><p>Dump a proposition.</p></div></div><div class="spec val" id="val-pp_proplist_with_typ"><a href="#val-pp_proplist_with_typ" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>pp_proplist_with_typ : <a href="../../../InferStdlib/InferStdlib/Pp/index.html#type-env">InferStdlib.Pp.env</a> <span class="keyword">‑></span> Format.formatter <span class="keyword">‑></span> <a href="index.html#type-normal">normal</a> <a href="index.html#type-t">t</a> list <span class="keyword">‑></span> unit</code></div><div class="doc"><p>Pretty print a list propositions with type information</p></div></div><div class="spec val" id="val-d_proplist_with_typ"><a href="#val-d_proplist_with_typ" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>d_proplist_with_typ : <span class="type-var">'a</span> <a href="index.html#type-t">t</a> list <span class="keyword">‑></span> unit</code></div><div class="doc"></div></div><div class="spec val" id="val-pi_free_vars"><a href="#val-pi_free_vars" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>pi_free_vars : <a href="index.html#type-pi">pi</a> <span class="keyword">‑></span> <a href="../../../InferIR/InferIR/Ident/index.html#type-t">InferIR.Ident.t</a> <a href="../../../InferStdlib/InferStdlib/index.html#module-IStd">InferStdlib.IStd</a>.Sequence.t</code></div><div class="doc"></div></div><div class="spec val" id="val-sigma_free_vars"><a href="#val-sigma_free_vars" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>sigma_free_vars : <a href="index.html#type-sigma">sigma</a> <span class="keyword">‑></span> <a href="../../../InferIR/InferIR/Ident/index.html#type-t">InferIR.Ident.t</a> <a href="../../../InferStdlib/InferStdlib/index.html#module-IStd">InferStdlib.IStd</a>.Sequence.t</code></div><div class="doc"></div></div><div class="spec val" id="val-free_vars"><a href="#val-free_vars" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>free_vars : <a href="index.html#type-normal">normal</a> <a href="index.html#type-t">t</a> <span class="keyword">‑></span> <a href="../../../InferIR/InferIR/Ident/index.html#type-t">InferIR.Ident.t</a> <a href="../../../InferStdlib/InferStdlib/index.html#module-IStd">InferStdlib.IStd</a>.Sequence.t</code></div><div class="doc"></div></div><div class="spec val" id="val-gen_free_vars"><a href="#val-gen_free_vars" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>gen_free_vars : <a href="index.html#type-normal">normal</a> <a href="index.html#type-t">t</a> <span class="keyword">‑></span> (unit, <a href="../../../InferIR/InferIR/Ident/index.html#type-t">InferIR.Ident.t</a>) <a href="../../../InferStdlib/InferStdlib/index.html#module-IStd">InferStdlib.IStd</a>.Sequence.Generator.t</code></div><div class="doc"></div></div><div class="spec val" id="val-footprint_free_vars"><a href="#val-footprint_free_vars" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>footprint_free_vars : <a href="index.html#type-normal">normal</a> <a href="index.html#type-t">t</a> <span class="keyword">‑></span> <a href="../../../InferIR/InferIR/Ident/index.html#type-t">InferIR.Ident.t</a> <a href="../../../InferStdlib/InferStdlib/index.html#module-IStd">InferStdlib.IStd</a>.Sequence.t</code></div><div class="doc"></div></div><div class="spec val" id="val-sorted_gen_free_vars"><a href="#val-sorted_gen_free_vars" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>sorted_gen_free_vars : <a href="index.html#type-sorted">sorted</a> <a href="index.html#type-t">t</a> <span class="keyword">‑></span> (unit, <a href="../../../InferIR/InferIR/Ident/index.html#type-t">InferIR.Ident.t</a>) <a href="../../../InferStdlib/InferStdlib/index.html#module-IStd">InferStdlib.IStd</a>.Sequence.Generator.t</code></div><div class="doc"></div></div><div class="spec val" id="val-non_pure_free_vars"><a href="#val-non_pure_free_vars" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>non_pure_free_vars : <a href="index.html#type-normal">normal</a> <a href="index.html#type-t">t</a> <span class="keyword">‑></span> <a href="../../../InferIR/InferIR/Ident/index.html#type-t">InferIR.Ident.t</a> <a href="../../../InferStdlib/InferStdlib/index.html#module-IStd">InferStdlib.IStd</a>.Sequence.t</code></div><div class="doc"></div></div><div class="spec val" id="val-dfs_sort"><a href="#val-dfs_sort" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>dfs_sort : <a href="../../../InferIR/InferIR/Tenv/index.html#type-t">InferIR.Tenv.t</a> <span class="keyword">‑></span> <a href="index.html#type-normal">normal</a> <a href="index.html#type-t">t</a> <span class="keyword">‑></span> <a href="index.html#type-sorted">sorted</a> <a href="index.html#type-t">t</a></code></div><div class="doc"></div></div><div class="spec val" id="val-pi_sub"><a href="#val-pi_sub" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>pi_sub : <a href="../../../InferIR/InferIR/Sil/index.html#type-subst">InferIR.Sil.subst</a> <span class="keyword">‑></span> <a href="../../../InferIR/InferIR/Sil/index.html#type-atom">InferIR.Sil.atom</a> list <span class="keyword">‑></span> <a href="../../../InferIR/InferIR/Sil/index.html#type-atom">InferIR.Sil.atom</a> list</code></div><div class="doc"><p>Apply substitution for pi</p></div></div><div class="spec val" id="val-sigma_sub"><a href="#val-sigma_sub" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>sigma_sub : <a href="../../../InferIR/InferIR/Sil/index.html#type-subst">InferIR.Sil.subst</a> <span class="keyword">‑></span> <a href="../../../InferIR/InferIR/Sil/index.html#type-hpred">InferIR.Sil.hpred</a> list <span class="keyword">‑></span> <a href="../../../InferIR/InferIR/Sil/index.html#type-hpred">InferIR.Sil.hpred</a> list</code></div><div class="doc"><p>Apply subsitution for sigma</p></div></div><div class="spec val" id="val-prop_sub"><a href="#val-prop_sub" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>prop_sub : <a href="../../../InferIR/InferIR/Sil/index.html#type-subst">InferIR.Sil.subst</a> <span class="keyword">‑></span> <span class="type-var">'a</span> <a href="index.html#type-t">t</a> <span class="keyword">‑></span> <a href="index.html#type-exposed">exposed</a> <a href="index.html#type-t">t</a></code></div><div class="doc"><p>Apply subsitution to prop. Result is not normalized.</p></div></div><div class="spec val" id="val-prop_expmap"><a href="#val-prop_expmap" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>prop_expmap : (<a href="../../../InferIR/InferIR/Exp/index.html#type-t">InferIR.Exp.t</a> <span class="keyword">‑></span> <a href="../../../InferIR/InferIR/Exp/index.html#type-t">InferIR.Exp.t</a>) <span class="keyword">‑></span> <span class="type-var">'a</span> <a href="index.html#type-t">t</a> <span class="keyword">‑></span> <a href="index.html#type-exposed">exposed</a> <a href="index.html#type-t">t</a></code></div><div class="doc"><p>Apply the substitution to all the expressions in the prop.</p></div></div><div class="spec val" id="val-sigma_replace_exp"><a href="#val-sigma_replace_exp" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>sigma_replace_exp : <a href="../../../InferIR/InferIR/Tenv/index.html#type-t">InferIR.Tenv.t</a> <span class="keyword">‑></span> (<a href="../../../InferIR/InferIR/Exp/index.html#type-t">InferIR.Exp.t</a><span class="keyword"> * </span><a href="../../../InferIR/InferIR/Exp/index.html#type-t">InferIR.Exp.t</a>) list <span class="keyword">‑></span> <a href="../../../InferIR/InferIR/Sil/index.html#type-hpred">InferIR.Sil.hpred</a> list <span class="keyword">‑></span> <a href="../../../InferIR/InferIR/Sil/index.html#type-hpred">InferIR.Sil.hpred</a> list</code></div><div class="doc"><p>Relaces all expressions in the <code class="code">hpred list</code> using the first argument.
|
|
|
Assume that the first parameter defines a partial function.
|
|
|
No expressions inside hpara are replaced.</p></div></div><h3>Normalization</h3><div class="spec val" id="val-mk_inequality"><a href="#val-mk_inequality" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>mk_inequality : <a href="../../../InferIR/InferIR/Tenv/index.html#type-t">InferIR.Tenv.t</a> <span class="keyword">‑></span> <a href="../../../InferIR/InferIR/Exp/index.html#type-t">InferIR.Exp.t</a> <span class="keyword">‑></span> <a href="../../../InferIR/InferIR/Sil/index.html#type-atom">InferIR.Sil.atom</a></code></div><div class="doc"><p>Turn an inequality expression into an atom</p></div></div><div class="spec val" id="val-atom_is_inequality"><a href="#val-atom_is_inequality" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>atom_is_inequality : <a href="../../../InferIR/InferIR/Sil/index.html#type-atom">InferIR.Sil.atom</a> <span class="keyword">‑></span> bool</code></div><div class="doc"><p>Return <code class="code">true</code> if the atom is an inequality</p></div></div><div class="spec val" id="val-atom_exp_le_const"><a href="#val-atom_exp_le_const" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>atom_exp_le_const : <a href="../../../InferIR/InferIR/Sil/index.html#type-atom">InferIR.Sil.atom</a> <span class="keyword">‑></span> (<a href="../../../InferIR/InferIR/Exp/index.html#type-t">InferIR.Exp.t</a><span class="keyword"> * </span><a href="../../../InferIR/InferIR/IntLit/index.html#type-t">InferIR.IntLit.t</a>) option</code></div><div class="doc"><p>If the atom is <code class="code">e<=n</code> return <code class="code">e,n</code></p></div></div><div class="spec val" id="val-atom_const_lt_exp"><a href="#val-atom_const_lt_exp" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>atom_const_lt_exp : <a href="../../../InferIR/InferIR/Sil/index.html#type-atom">InferIR.Sil.atom</a> <span class="keyword">‑></span> (<a href="../../../InferIR/InferIR/IntLit/index.html#type-t">InferIR.IntLit.t</a><span class="keyword"> * </span><a href="../../../InferIR/InferIR/Exp/index.html#type-t">InferIR.Exp.t</a>) option</code></div><div class="doc"><p>If the atom is <code class="code">n<e</code> return <code class="code">n,e</code></p></div></div><div class="spec val" id="val-exp_normalize_prop"><a href="#val-exp_normalize_prop" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>exp_normalize_prop : ?⁠destructive:bool <span class="keyword">‑></span> <a href="../../../InferIR/InferIR/Tenv/index.html#type-t">InferIR.Tenv.t</a> <span class="keyword">‑></span> <span class="type-var">'a</span> <a href="index.html#type-t">t</a> <span class="keyword">‑></span> <a href="../../../InferIR/InferIR/Exp/index.html#type-t">InferIR.Exp.t</a> <span class="keyword">‑></span> <a href="../../../InferIR/InferIR/Exp/index.html#type-t">InferIR.Exp.t</a></code></div><div class="doc"><p>Normalize <code class="code">exp</code> using the pure part of <code class="code">prop</code>. Later, we should change this such that the
|
|
|
normalization exposes offsets of <code class="code">exp</code> as much as possible.</p><p>If <code class="code">destructive</code> is true then normalize more aggressively, which may lose some useful structure
|
|
|
or types.</p></div></div><div class="spec val" id="val-exp_normalize_noabs"><a href="#val-exp_normalize_noabs" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>exp_normalize_noabs : <a href="../../../InferIR/InferIR/Tenv/index.html#type-t">InferIR.Tenv.t</a> <span class="keyword">‑></span> <a href="../../../InferIR/InferIR/Sil/index.html#type-subst">InferIR.Sil.subst</a> <span class="keyword">‑></span> <a href="../../../InferIR/InferIR/Exp/index.html#type-t">InferIR.Exp.t</a> <span class="keyword">‑></span> <a href="../../../InferIR/InferIR/Exp/index.html#type-t">InferIR.Exp.t</a></code></div><div class="doc"><p>Normalize the expression without abstracting complex subexpressions</p></div></div><div class="spec val" id="val-exp_collapse_consecutive_indices_prop"><a href="#val-exp_collapse_consecutive_indices_prop" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>exp_collapse_consecutive_indices_prop : <a href="../../../InferIR/InferIR/Typ/index.html#type-t">InferIR.Typ.t</a> <span class="keyword">‑></span> <a href="../../../InferIR/InferIR/Exp/index.html#type-t">InferIR.Exp.t</a> <span class="keyword">‑></span> <a href="../../../InferIR/InferIR/Exp/index.html#type-t">InferIR.Exp.t</a></code></div><div class="doc"><p>Collapse consecutive indices that should be added. For instance,
|
|
|
this function reduces x<code class="code">1</code><code class="code">1</code> to x<code class="code">2</code>. The <code class="code">typ</code> argument is used
|
|
|
to ensure the soundness of this collapsing.</p></div></div><div class="spec val" id="val-lexp_normalize_prop"><a href="#val-lexp_normalize_prop" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>lexp_normalize_prop : <a href="../../../InferIR/InferIR/Tenv/index.html#type-t">InferIR.Tenv.t</a> <span class="keyword">‑></span> <span class="type-var">'a</span> <a href="index.html#type-t">t</a> <span class="keyword">‑></span> <a href="../../../InferIR/InferIR/Exp/index.html#type-t">InferIR.Exp.t</a> <span class="keyword">‑></span> <a href="../../../InferIR/InferIR/Exp/index.html#type-t">InferIR.Exp.t</a></code></div><div class="doc"><p>Normalize <code class="code">exp</code> used for the address of a heap cell.
|
|
|
This normalization does not combine two offsets inside <code class="code">exp</code>.</p></div></div><div class="spec val" id="val-atom_normalize_prop"><a href="#val-atom_normalize_prop" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>atom_normalize_prop : <a href="../../../InferIR/InferIR/Tenv/index.html#type-t">InferIR.Tenv.t</a> <span class="keyword">‑></span> <span class="type-var">'a</span> <a href="index.html#type-t">t</a> <span class="keyword">‑></span> <a href="../../../InferIR/InferIR/Sil/index.html#type-atom">InferIR.Sil.atom</a> <span class="keyword">‑></span> <a href="../../../InferIR/InferIR/Sil/index.html#type-atom">InferIR.Sil.atom</a></code></div><div class="doc"></div></div><div class="spec val" id="val-sigma_normalize_prop"><a href="#val-sigma_normalize_prop" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>sigma_normalize_prop : <a href="../../../InferIR/InferIR/Tenv/index.html#type-t">InferIR.Tenv.t</a> <span class="keyword">‑></span> <span class="type-var">'a</span> <a href="index.html#type-t">t</a> <span class="keyword">‑></span> <a href="../../../InferIR/InferIR/Sil/index.html#type-hpred">InferIR.Sil.hpred</a> list <span class="keyword">‑></span> <a href="../../../InferIR/InferIR/Sil/index.html#type-hpred">InferIR.Sil.hpred</a> list</code></div><div class="doc"></div></div><div class="spec val" id="val-normalize"><a href="#val-normalize" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>normalize : <a href="../../../InferIR/InferIR/Tenv/index.html#type-t">InferIR.Tenv.t</a> <span class="keyword">‑></span> <a href="index.html#type-exposed">exposed</a> <a href="index.html#type-t">t</a> <span class="keyword">‑></span> <a href="index.html#type-normal">normal</a> <a href="index.html#type-t">t</a></code></div><div class="doc"><p>normalize a prop</p></div></div><div class="spec val" id="val-expose"><a href="#val-expose" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>expose : <a href="index.html#type-normal">normal</a> <a href="index.html#type-t">t</a> <span class="keyword">‑></span> <a href="index.html#type-exposed">exposed</a> <a href="index.html#type-t">t</a></code></div><div class="doc"><p>expose a prop, no-op used to instantiate the sub-type relation</p></div></div><h3>Compaction</h3><div class="spec val" id="val-prop_compact"><a href="#val-prop_compact" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>prop_compact : <a href="../../../InferIR/InferIR/Sil/index.html#type-sharing_env">InferIR.Sil.sharing_env</a> <span class="keyword">‑></span> <a href="index.html#type-normal">normal</a> <a href="index.html#type-t">t</a> <span class="keyword">‑></span> <a href="index.html#type-normal">normal</a> <a href="index.html#type-t">t</a></code></div><div class="doc"><p>Return a compact representation of the prop</p></div></div><h3>Queries about propositions</h3><div class="spec val" id="val-prop_is_emp"><a href="#val-prop_is_emp" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>prop_is_emp : <span class="type-var">'a</span> <a href="index.html#type-t">t</a> <span class="keyword">‑></span> bool</code></div><div class="doc"><p>Check if the sigma part of the proposition is emp</p></div></div><h3>Functions for changing and generating propositions</h3><div class="spec val" id="val-mk_neq"><a href="#val-mk_neq" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>mk_neq : <a href="../../../InferIR/InferIR/Tenv/index.html#type-t">InferIR.Tenv.t</a> <span class="keyword">‑></span> <a href="../../../InferIR/InferIR/Exp/index.html#type-t">InferIR.Exp.t</a> <span class="keyword">‑></span> <a href="../../../InferIR/InferIR/Exp/index.html#type-t">InferIR.Exp.t</a> <span class="keyword">‑></span> <a href="../../../InferIR/InferIR/Sil/index.html#type-atom">InferIR.Sil.atom</a></code></div><div class="doc"><p>Construct a disequality.</p></div></div><div class="spec val" id="val-mk_eq"><a href="#val-mk_eq" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>mk_eq : <a href="../../../InferIR/InferIR/Tenv/index.html#type-t">InferIR.Tenv.t</a> <span class="keyword">‑></span> <a href="../../../InferIR/InferIR/Exp/index.html#type-t">InferIR.Exp.t</a> <span class="keyword">‑></span> <a href="../../../InferIR/InferIR/Exp/index.html#type-t">InferIR.Exp.t</a> <span class="keyword">‑></span> <a href="../../../InferIR/InferIR/Sil/index.html#type-atom">InferIR.Sil.atom</a></code></div><div class="doc"><p>Construct an equality.</p></div></div><div class="spec val" id="val-mk_pred"><a href="#val-mk_pred" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>mk_pred : <a href="../../../InferIR/InferIR/Tenv/index.html#type-t">InferIR.Tenv.t</a> <span class="keyword">‑></span> <a href="../../../InferIR/InferIR/PredSymb/index.html#type-t">InferIR.PredSymb.t</a> <span class="keyword">‑></span> <a href="../../../InferIR/InferIR/Exp/index.html#type-t">InferIR.Exp.t</a> list <span class="keyword">‑></span> <a href="../../../InferIR/InferIR/Sil/index.html#type-atom">InferIR.Sil.atom</a></code></div><div class="doc"><p>Construct a positive pred.</p></div></div><div class="spec val" id="val-mk_npred"><a href="#val-mk_npred" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>mk_npred : <a href="../../../InferIR/InferIR/Tenv/index.html#type-t">InferIR.Tenv.t</a> <span class="keyword">‑></span> <a href="../../../InferIR/InferIR/PredSymb/index.html#type-t">InferIR.PredSymb.t</a> <span class="keyword">‑></span> <a href="../../../InferIR/InferIR/Exp/index.html#type-t">InferIR.Exp.t</a> list <span class="keyword">‑></span> <a href="../../../InferIR/InferIR/Sil/index.html#type-atom">InferIR.Sil.atom</a></code></div><div class="doc"><p>Construct a negative pred.</p></div></div><div class="spec val" id="val-create_strexp_of_type"><a href="#val-create_strexp_of_type" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>create_strexp_of_type : <a href="../../../InferIR/InferIR/Tenv/index.html#type-t">InferIR.Tenv.t</a> <span class="keyword">‑></span> <a href="index.html#type-struct_init_mode">struct_init_mode</a> <span class="keyword">‑></span> <a href="../../../InferIR/InferIR/Typ/index.html#type-t">InferIR.Typ.t</a> <span class="keyword">‑></span> <a href="../../../InferIR/InferIR/Exp/index.html#type-t">InferIR.Exp.t</a> option <span class="keyword">‑></span> <a href="../../../InferIR/InferIR/Sil/index.html#type-inst">InferIR.Sil.inst</a> <span class="keyword">‑></span> <a href="../../../InferIR/InferIR/Sil/index.html#type-strexp">InferIR.Sil.strexp</a></code></div><div class="doc"><p>create a strexp of the given type, populating the structures if <code class="code">expand_structs</code> is true</p></div></div><div class="spec val" id="val-mk_ptsto"><a href="#val-mk_ptsto" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>mk_ptsto : <a href="../../../InferIR/InferIR/Tenv/index.html#type-t">InferIR.Tenv.t</a> <span class="keyword">‑></span> <a href="../../../InferIR/InferIR/Exp/index.html#type-t">InferIR.Exp.t</a> <span class="keyword">‑></span> <a href="../../../InferIR/InferIR/Sil/index.html#type-strexp">InferIR.Sil.strexp</a> <span class="keyword">‑></span> <a href="../../../InferIR/InferIR/Exp/index.html#type-t">InferIR.Exp.t</a> <span class="keyword">‑></span> <a href="../../../InferIR/InferIR/Sil/index.html#type-hpred">InferIR.Sil.hpred</a></code></div><div class="doc"><p>Construct a pointsto.</p></div></div><div class="spec val" id="val-mk_ptsto_exp"><a href="#val-mk_ptsto_exp" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>mk_ptsto_exp : <a href="../../../InferIR/InferIR/Tenv/index.html#type-t">InferIR.Tenv.t</a> <span class="keyword">‑></span> <a href="index.html#type-struct_init_mode">struct_init_mode</a> <span class="keyword">‑></span> (<a href="../../../InferIR/InferIR/Exp/index.html#type-t">InferIR.Exp.t</a><span class="keyword"> * </span><a href="../../../InferIR/InferIR/Exp/index.html#type-t">InferIR.Exp.t</a><span class="keyword"> * </span><a href="../../../InferIR/InferIR/Exp/index.html#type-t">InferIR.Exp.t</a> option) <span class="keyword">‑></span> <a href="../../../InferIR/InferIR/Sil/index.html#type-inst">InferIR.Sil.inst</a> <span class="keyword">‑></span> <a href="../../../InferIR/InferIR/Sil/index.html#type-hpred">InferIR.Sil.hpred</a></code></div><div class="doc"><p>Construct a points-to predicate for an expression using either the provided expression <code class="code">name</code> as
|
|
|
base for fresh identifiers.</p></div></div><div class="spec val" id="val-mk_ptsto_lvar"><a href="#val-mk_ptsto_lvar" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>mk_ptsto_lvar : <a href="../../../InferIR/InferIR/Tenv/index.html#type-t">InferIR.Tenv.t</a> <span class="keyword">‑></span> <a href="index.html#type-struct_init_mode">struct_init_mode</a> <span class="keyword">‑></span> <a href="../../../InferIR/InferIR/Sil/index.html#type-inst">InferIR.Sil.inst</a> <span class="keyword">‑></span> (<a href="../../../InferIR/InferIR/Pvar/index.html#type-t">InferIR.Pvar.t</a><span class="keyword"> * </span><a href="../../../InferIR/InferIR/Exp/index.html#type-t">InferIR.Exp.t</a><span class="keyword"> * </span><a href="../../../InferIR/InferIR/Exp/index.html#type-t">InferIR.Exp.t</a> option) <span class="keyword">‑></span> <a href="../../../InferIR/InferIR/Sil/index.html#type-hpred">InferIR.Sil.hpred</a></code></div><div class="doc"><p>Construct a points-to predicate for a single program variable.
|
|
|
If <code class="code">expand_structs</code> is true, initialize the fields of structs with fresh variables.</p></div></div><div class="spec val" id="val-mk_lseg"><a href="#val-mk_lseg" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>mk_lseg : <a href="../../../InferIR/InferIR/Tenv/index.html#type-t">InferIR.Tenv.t</a> <span class="keyword">‑></span> <a href="../../../InferIR/InferIR/Sil/index.html#type-lseg_kind">InferIR.Sil.lseg_kind</a> <span class="keyword">‑></span> <a href="../../../InferIR/InferIR/Sil/index.html#type-hpara">InferIR.Sil.hpara</a> <span class="keyword">‑></span> <a href="../../../InferIR/InferIR/Exp/index.html#type-t">InferIR.Exp.t</a> <span class="keyword">‑></span> <a href="../../../InferIR/InferIR/Exp/index.html#type-t">InferIR.Exp.t</a> <span class="keyword">‑></span> <a href="../../../InferIR/InferIR/Exp/index.html#type-t">InferIR.Exp.t</a> list <span class="keyword">‑></span> <a href="../../../InferIR/InferIR/Sil/index.html#type-hpred">InferIR.Sil.hpred</a></code></div><div class="doc"><p>Construct a lseg predicate</p></div></div><div class="spec val" id="val-mk_dllseg"><a href="#val-mk_dllseg" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>mk_dllseg : <a href="../../../InferIR/InferIR/Tenv/index.html#type-t">InferIR.Tenv.t</a> <span class="keyword">‑></span> <a href="../../../InferIR/InferIR/Sil/index.html#type-lseg_kind">InferIR.Sil.lseg_kind</a> <span class="keyword">‑></span> <a href="../../../InferIR/InferIR/Sil/index.html#type-hpara_dll">InferIR.Sil.hpara_dll</a> <span class="keyword">‑></span> <a href="../../../InferIR/InferIR/Exp/index.html#type-t">InferIR.Exp.t</a> <span class="keyword">‑></span> <a href="../../../InferIR/InferIR/Exp/index.html#type-t">InferIR.Exp.t</a> <span class="keyword">‑></span> <a href="../../../InferIR/InferIR/Exp/index.html#type-t">InferIR.Exp.t</a> <span class="keyword">‑></span> <a href="../../../InferIR/InferIR/Exp/index.html#type-t">InferIR.Exp.t</a> <span class="keyword">‑></span> <a href="../../../InferIR/InferIR/Exp/index.html#type-t">InferIR.Exp.t</a> list <span class="keyword">‑></span> <a href="../../../InferIR/InferIR/Sil/index.html#type-hpred">InferIR.Sil.hpred</a></code></div><div class="doc"><p>Construct a dllseg predicate</p></div></div><div class="spec val" id="val-prop_emp"><a href="#val-prop_emp" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>prop_emp : <a href="index.html#type-normal">normal</a> <a href="index.html#type-t">t</a></code></div><div class="doc"><p>Proposition <code class="code">true /\ emp</code>.</p></div></div><div class="spec val" id="val-prop_reset_inst"><a href="#val-prop_reset_inst" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>prop_reset_inst : (<a href="../../../InferIR/InferIR/Sil/index.html#type-inst">InferIR.Sil.inst</a> <span class="keyword">‑></span> <a href="../../../InferIR/InferIR/Sil/index.html#type-inst">InferIR.Sil.inst</a>) <span class="keyword">‑></span> <span class="type-var">'a</span> <a href="index.html#type-t">t</a> <span class="keyword">‑></span> <a href="index.html#type-exposed">exposed</a> <a href="index.html#type-t">t</a></code></div><div class="doc"><p>Reset every inst in the prop using the given map</p></div></div><div class="spec val" id="val-prop_hpred_star"><a href="#val-prop_hpred_star" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>prop_hpred_star : <span class="type-var">'a</span> <a href="index.html#type-t">t</a> <span class="keyword">‑></span> <a href="../../../InferIR/InferIR/Sil/index.html#type-hpred">InferIR.Sil.hpred</a> <span class="keyword">‑></span> <a href="index.html#type-exposed">exposed</a> <a href="index.html#type-t">t</a></code></div><div class="doc"><p>Conjoin a heap predicate by separating conjunction.</p></div></div><div class="spec val" id="val-prop_sigma_star"><a href="#val-prop_sigma_star" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>prop_sigma_star : <span class="type-var">'a</span> <a href="index.html#type-t">t</a> <span class="keyword">‑></span> <a href="../../../InferIR/InferIR/Sil/index.html#type-hpred">InferIR.Sil.hpred</a> list <span class="keyword">‑></span> <a href="index.html#type-exposed">exposed</a> <a href="index.html#type-t">t</a></code></div><div class="doc"><p>Conjoin a list of heap predicates by separating conjunction</p></div></div><div class="spec val" id="val-prop_atom_and"><a href="#val-prop_atom_and" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>prop_atom_and : <a href="../../../InferIR/InferIR/Tenv/index.html#type-t">InferIR.Tenv.t</a> <span class="keyword">‑></span> ?⁠footprint:bool <span class="keyword">‑></span> <a href="index.html#type-normal">normal</a> <a href="index.html#type-t">t</a> <span class="keyword">‑></span> <a href="../../../InferIR/InferIR/Sil/index.html#type-atom">InferIR.Sil.atom</a> <span class="keyword">‑></span> <a href="index.html#type-normal">normal</a> <a href="index.html#type-t">t</a></code></div><div class="doc"><p>Conjoin a pure atomic predicate by normal conjunction.</p></div></div><div class="spec val" id="val-conjoin_eq"><a href="#val-conjoin_eq" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>conjoin_eq : <a href="../../../InferIR/InferIR/Tenv/index.html#type-t">InferIR.Tenv.t</a> <span class="keyword">‑></span> ?⁠footprint:bool <span class="keyword">‑></span> <a href="../../../InferIR/InferIR/Exp/index.html#type-t">InferIR.Exp.t</a> <span class="keyword">‑></span> <a href="../../../InferIR/InferIR/Exp/index.html#type-t">InferIR.Exp.t</a> <span class="keyword">‑></span> <a href="index.html#type-normal">normal</a> <a href="index.html#type-t">t</a> <span class="keyword">‑></span> <a href="index.html#type-normal">normal</a> <a href="index.html#type-t">t</a></code></div><div class="doc"><p>Conjoin <code class="code">exp1</code>=<code class="code">exp2</code> with a symbolic heap <code class="code">prop</code>.</p></div></div><div class="spec val" id="val-conjoin_neq"><a href="#val-conjoin_neq" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>conjoin_neq : <a href="../../../InferIR/InferIR/Tenv/index.html#type-t">InferIR.Tenv.t</a> <span class="keyword">‑></span> ?⁠footprint:bool <span class="keyword">‑></span> <a href="../../../InferIR/InferIR/Exp/index.html#type-t">InferIR.Exp.t</a> <span class="keyword">‑></span> <a href="../../../InferIR/InferIR/Exp/index.html#type-t">InferIR.Exp.t</a> <span class="keyword">‑></span> <a href="index.html#type-normal">normal</a> <a href="index.html#type-t">t</a> <span class="keyword">‑></span> <a href="index.html#type-normal">normal</a> <a href="index.html#type-t">t</a></code></div><div class="doc"><p>Conjoin <code class="code">exp1</code>!=<code class="code">exp2</code> with a symbolic heap <code class="code">prop</code>.</p></div></div><div class="spec val" id="val-get_pure"><a href="#val-get_pure" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>get_pure : <span class="type-var">'a</span> <a href="index.html#type-t">t</a> <span class="keyword">‑></span> <a href="../../../InferIR/InferIR/Sil/index.html#type-atom">InferIR.Sil.atom</a> list</code></div><div class="doc"><p>Return the pure part of <code class="code">prop</code>.</p></div></div><div class="spec val" id="val-prop_rename_primed_footprint_vars"><a href="#val-prop_rename_primed_footprint_vars" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>prop_rename_primed_footprint_vars : <a href="../../../InferIR/InferIR/Tenv/index.html#type-t">InferIR.Tenv.t</a> <span class="keyword">‑></span> <a href="index.html#type-normal">normal</a> <a href="index.html#type-t">t</a> <span class="keyword">‑></span> <a href="index.html#type-normal">normal</a> <a href="index.html#type-t">t</a></code></div><div class="doc"><p>Canonicalize the names of primed variables.</p></div></div><div class="spec val" id="val-extract_footprint"><a href="#val-extract_footprint" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>extract_footprint : <span class="type-var">'a</span> <a href="index.html#type-t">t</a> <span class="keyword">‑></span> <a href="index.html#type-exposed">exposed</a> <a href="index.html#type-t">t</a></code></div><div class="doc"><p>Extract the footprint and return it as a prop</p></div></div><div class="spec val" id="val-extract_spec"><a href="#val-extract_spec" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>extract_spec : <a href="index.html#type-normal">normal</a> <a href="index.html#type-t">t</a> <span class="keyword">‑></span> <a href="index.html#type-normal">normal</a> <a href="index.html#type-t">t</a><span class="keyword"> * </span><a href="index.html#type-normal">normal</a> <a href="index.html#type-t">t</a></code></div><div class="doc"><p>Extract the (footprint,current) pair</p></div></div><div class="spec val" id="val-prop_expand"><a href="#val-prop_expand" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>prop_expand : <a href="../../../InferIR/InferIR/Tenv/index.html#type-t">InferIR.Tenv.t</a> <span class="keyword">‑></span> <a href="index.html#type-normal">normal</a> <a href="index.html#type-t">t</a> <span class="keyword">‑></span> <a href="index.html#type-normal">normal</a> <a href="index.html#type-t">t</a> list</code></div><div class="doc"><p>Expand PE listsegs if the flag is on.</p></div></div><h3>Functions for existentially quantifying and unquantifying variables</h3><div class="spec val" id="val-exist_quantify"><a href="#val-exist_quantify" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>exist_quantify : <a href="../../../InferIR/InferIR/Tenv/index.html#type-t">InferIR.Tenv.t</a> <span class="keyword">‑></span> ?⁠ids_queue:unit <a href="../../../InferIR/InferIR__Ident/index.html#module-HashQueue">InferIR.Ident.HashQueue</a>.t <span class="keyword">‑></span> <a href="../../../InferIR/InferIR/Ident/index.html#type-t">InferIR.Ident.t</a> list <span class="keyword">‑></span> <a href="index.html#type-normal">normal</a> <a href="index.html#type-t">t</a> <span class="keyword">‑></span> <a href="index.html#type-normal">normal</a> <a href="index.html#type-t">t</a></code></div><div class="doc"><p>Existentially quantify the <code class="code">ids</code> in <code class="code">prop</code>.</p></div></div><div class="spec val" id="val-prop_normal_vars_to_primed_vars"><a href="#val-prop_normal_vars_to_primed_vars" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>prop_normal_vars_to_primed_vars : <a href="../../../InferIR/InferIR/Tenv/index.html#type-t">InferIR.Tenv.t</a> <span class="keyword">‑></span> <a href="index.html#type-normal">normal</a> <a href="index.html#type-t">t</a> <span class="keyword">‑></span> <a href="index.html#type-normal">normal</a> <a href="index.html#type-t">t</a></code></div><div class="doc"><p>convert the footprint vars to primed vars.</p></div></div><div class="spec val" id="val-prop_primed_vars_to_normal_vars"><a href="#val-prop_primed_vars_to_normal_vars" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>prop_primed_vars_to_normal_vars : <a href="../../../InferIR/InferIR/Tenv/index.html#type-t">InferIR.Tenv.t</a> <span class="keyword">‑></span> <a href="index.html#type-normal">normal</a> <a href="index.html#type-t">t</a> <span class="keyword">‑></span> <a href="index.html#type-normal">normal</a> <a href="index.html#type-t">t</a></code></div><div class="doc"><p>convert the primed vars to normal vars.</p></div></div><div class="spec val" id="val-from_pi"><a href="#val-from_pi" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>from_pi : <a href="index.html#type-pi">pi</a> <span class="keyword">‑></span> <a href="index.html#type-exposed">exposed</a> <a href="index.html#type-t">t</a></code></div><div class="doc"><p>Build an exposed prop from pi</p></div></div><div class="spec val" id="val-from_sigma"><a href="#val-from_sigma" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>from_sigma : <a href="index.html#type-sigma">sigma</a> <span class="keyword">‑></span> <a href="index.html#type-exposed">exposed</a> <a href="index.html#type-t">t</a></code></div><div class="doc"><p>Build an exposed prop from sigma</p></div></div><div class="spec val" id="val-set"><a href="#val-set" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>set : ?⁠sub:<a href="../../../InferIR/InferIR/Sil/index.html#type-exp_subst">InferIR.Sil.exp_subst</a> <span class="keyword">‑></span> ?⁠pi:<a href="index.html#type-pi">pi</a> <span class="keyword">‑></span> ?⁠sigma:<a href="index.html#type-sigma">sigma</a> <span class="keyword">‑></span> ?⁠pi_fp:<a href="index.html#type-pi">pi</a> <span class="keyword">‑></span> ?⁠sigma_fp:<a href="index.html#type-sigma">sigma</a> <span class="keyword">‑></span> <span class="type-var">'a</span> <a href="index.html#type-t">t</a> <span class="keyword">‑></span> <a href="index.html#type-exposed">exposed</a> <a href="index.html#type-t">t</a></code></div><div class="doc"><p>Set individual fields of the prop.</p></div></div><h3>Prop iterators</h3><div class="spec type" id="type-prop_iter"><a href="#type-prop_iter" class="anchor"></a><div class="def type"><code><span class="keyword">type </span>'a prop_iter</code><code></code><code></code></div><div class="doc"><p>Iterator over the sigma part. Each iterator has a current <code class="code">hpred</code>.</p></div></div><div class="spec val" id="val-prop_iter_create"><a href="#val-prop_iter_create" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>prop_iter_create : <a href="index.html#type-normal">normal</a> <a href="index.html#type-t">t</a> <span class="keyword">‑></span> unit <a href="index.html#type-prop_iter">prop_iter</a> option</code></div><div class="doc"><p>Create an iterator, return None if sigma part is empty.</p></div></div><div class="spec val" id="val-prop_iter_to_prop"><a href="#val-prop_iter_to_prop" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>prop_iter_to_prop : <a href="../../../InferIR/InferIR/Tenv/index.html#type-t">InferIR.Tenv.t</a> <span class="keyword">‑></span> <span class="type-var">'a</span> <a href="index.html#type-prop_iter">prop_iter</a> <span class="keyword">‑></span> <a href="index.html#type-normal">normal</a> <a href="index.html#type-t">t</a></code></div><div class="doc"><p>Return the prop associated to the iterator.</p></div></div><div class="spec val" id="val-prop_iter_add_atom"><a href="#val-prop_iter_add_atom" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>prop_iter_add_atom : bool <span class="keyword">‑></span> <span class="type-var">'a</span> <a href="index.html#type-prop_iter">prop_iter</a> <span class="keyword">‑></span> <a href="../../../InferIR/InferIR/Sil/index.html#type-atom">InferIR.Sil.atom</a> <span class="keyword">‑></span> <span class="type-var">'a</span> <a href="index.html#type-prop_iter">prop_iter</a></code></div><div class="doc"><p>Add an atom to the pi part of prop iter. The
|
|
|
first parameter records whether it is done
|
|
|
during footprint or during re - execution.</p></div></div><div class="spec val" id="val-prop_iter_remove_curr_then_to_prop"><a href="#val-prop_iter_remove_curr_then_to_prop" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>prop_iter_remove_curr_then_to_prop : <a href="../../../InferIR/InferIR/Tenv/index.html#type-t">InferIR.Tenv.t</a> <span class="keyword">‑></span> <span class="type-var">'a</span> <a href="index.html#type-prop_iter">prop_iter</a> <span class="keyword">‑></span> <a href="index.html#type-normal">normal</a> <a href="index.html#type-t">t</a></code></div><div class="doc"><p>Remove the current element from the iterator, and return the prop
|
|
|
associated to the resulting iterator.</p></div></div><div class="spec val" id="val-prop_iter_current"><a href="#val-prop_iter_current" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>prop_iter_current : <a href="../../../InferIR/InferIR/Tenv/index.html#type-t">InferIR.Tenv.t</a> <span class="keyword">‑></span> <span class="type-var">'a</span> <a href="index.html#type-prop_iter">prop_iter</a> <span class="keyword">‑></span> <a href="../../../InferIR/InferIR/Sil/index.html#type-hpred">InferIR.Sil.hpred</a><span class="keyword"> * </span><span class="type-var">'a</span></code></div><div class="doc"><p>Return the current hpred and state.</p></div></div><div class="spec val" id="val-prop_iter_next"><a href="#val-prop_iter_next" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>prop_iter_next : <span class="type-var">'a</span> <a href="index.html#type-prop_iter">prop_iter</a> <span class="keyword">‑></span> unit <a href="index.html#type-prop_iter">prop_iter</a> option</code></div><div class="doc"><p>Return the next iterator.</p></div></div><div class="spec val" id="val-prop_iter_update_current"><a href="#val-prop_iter_update_current" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>prop_iter_update_current : <span class="type-var">'a</span> <a href="index.html#type-prop_iter">prop_iter</a> <span class="keyword">‑></span> <a href="../../../InferIR/InferIR/Sil/index.html#type-hpred">InferIR.Sil.hpred</a> <span class="keyword">‑></span> <span class="type-var">'a</span> <a href="index.html#type-prop_iter">prop_iter</a></code></div><div class="doc"><p>Update the current element of the iterator.</p></div></div><div class="spec val" id="val-prop_iter_prev_then_insert"><a href="#val-prop_iter_prev_then_insert" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>prop_iter_prev_then_insert : <span class="type-var">'a</span> <a href="index.html#type-prop_iter">prop_iter</a> <span class="keyword">‑></span> <a href="../../../InferIR/InferIR/Sil/index.html#type-hpred">InferIR.Sil.hpred</a> <span class="keyword">‑></span> <span class="type-var">'a</span> <a href="index.html#type-prop_iter">prop_iter</a></code></div><div class="doc"><p>Insert before the current element of the iterator.</p></div></div><div class="spec val" id="val-prop_iter_footprint_free_vars"><a href="#val-prop_iter_footprint_free_vars" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>prop_iter_footprint_free_vars : <span class="type-var">'a</span> <a href="index.html#type-prop_iter">prop_iter</a> <span class="keyword">‑></span> <a href="../../../InferIR/InferIR/Ident/index.html#type-t">InferIR.Ident.t</a> <a href="../../../InferStdlib/InferStdlib/index.html#module-IStd">InferStdlib.IStd</a>.Sequence.t</code></div><div class="doc"><p>Find fav of the footprint part of the iterator</p></div></div><div class="spec val" id="val-prop_iter_free_vars"><a href="#val-prop_iter_free_vars" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>prop_iter_free_vars : <span class="type-var">'a</span> <a href="index.html#type-prop_iter">prop_iter</a> <span class="keyword">‑></span> <a href="../../../InferIR/InferIR/Ident/index.html#type-t">InferIR.Ident.t</a> <a href="../../../InferStdlib/InferStdlib/index.html#module-IStd">InferStdlib.IStd</a>.Sequence.t</code></div><div class="doc"><p>Find fav of the iterator</p></div></div><div class="spec val" id="val-prop_iter_get_footprint_sigma"><a href="#val-prop_iter_get_footprint_sigma" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>prop_iter_get_footprint_sigma : <span class="type-var">'a</span> <a href="index.html#type-prop_iter">prop_iter</a> <span class="keyword">‑></span> <a href="../../../InferIR/InferIR/Sil/index.html#type-hpred">InferIR.Sil.hpred</a> list</code></div><div class="doc"><p>Extract the sigma part of the footprint</p></div></div><div class="spec val" id="val-prop_iter_replace_footprint_sigma"><a href="#val-prop_iter_replace_footprint_sigma" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>prop_iter_replace_footprint_sigma : <span class="type-var">'a</span> <a href="index.html#type-prop_iter">prop_iter</a> <span class="keyword">‑></span> <a href="../../../InferIR/InferIR/Sil/index.html#type-hpred">InferIR.Sil.hpred</a> list <span class="keyword">‑></span> <span class="type-var">'a</span> <a href="index.html#type-prop_iter">prop_iter</a></code></div><div class="doc"><p>Replace the sigma part of the footprint</p></div></div><div class="spec val" id="val-prop_iter_find"><a href="#val-prop_iter_find" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>prop_iter_find : unit <a href="index.html#type-prop_iter">prop_iter</a> <span class="keyword">‑></span> (<a href="../../../InferIR/InferIR/Sil/index.html#type-hpred">InferIR.Sil.hpred</a> <span class="keyword">‑></span> <span class="type-var">'a</span> option) <span class="keyword">‑></span> <span class="type-var">'a</span> <a href="index.html#type-prop_iter">prop_iter</a> option</code></div><div class="doc"><p>Scan sigma to find an <code class="code">hpred</code> satisfying the filter function.</p></div></div><div class="spec val" id="val-prop_iter_update_current_by_list"><a href="#val-prop_iter_update_current_by_list" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>prop_iter_update_current_by_list : <span class="type-var">'a</span> <a href="index.html#type-prop_iter">prop_iter</a> <span class="keyword">‑></span> <a href="../../../InferIR/InferIR/Sil/index.html#type-hpred">InferIR.Sil.hpred</a> list <span class="keyword">‑></span> unit <a href="index.html#type-prop_iter">prop_iter</a></code></div><div class="doc"><p>Update the current element of the iterator by a nonempty list of elements.</p></div></div><div class="spec val" id="val-prop_iter_set_state"><a href="#val-prop_iter_set_state" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>prop_iter_set_state : <span class="type-var">'a</span> <a href="index.html#type-prop_iter">prop_iter</a> <span class="keyword">‑></span> <span class="type-var">'b</span> <span class="keyword">‑></span> <span class="type-var">'b</span> <a href="index.html#type-prop_iter">prop_iter</a></code></div><div class="doc"><p>Set the state of an iterator</p></div></div><div class="spec val" id="val-prop_iter_make_id_primed"><a href="#val-prop_iter_make_id_primed" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>prop_iter_make_id_primed : <a href="../../../InferIR/InferIR/Tenv/index.html#type-t">InferIR.Tenv.t</a> <span class="keyword">‑></span> <a href="../../../InferIR/InferIR/Ident/index.html#type-t">InferIR.Ident.t</a> <span class="keyword">‑></span> <span class="type-var">'a</span> <a href="index.html#type-prop_iter">prop_iter</a> <span class="keyword">‑></span> <span class="type-var">'a</span> <a href="index.html#type-prop_iter">prop_iter</a></code></div><div class="doc"><p>Rename <code class="code">ident</code> in <code class="code">iter</code> by a fresh primed identifier</p></div></div><div class="spec val" id="val-prop_iter_gc_fields"><a href="#val-prop_iter_gc_fields" class="anchor"></a><div class="def val"><code><span class="keyword">val </span>prop_iter_gc_fields : unit <a href="index.html#type-prop_iter">prop_iter</a> <span class="keyword">‑></span> unit <a href="index.html#type-prop_iter">prop_iter</a></code></div><div class="doc"><p>Collect garbage fields.</p></div></div><h3>Internal modules</h3><div class="spec module" id="module-Metrics"><a href="#module-Metrics" class="anchor"></a><div class="def module"><code><span class="keyword">module </span><a href="Metrics/index.html">Metrics</a> : <span class="keyword">sig</span> ... <span class="keyword">end</span></code></div><div class="doc"></div></div><div class="spec module" id="module-CategorizePreconditions"><a href="#module-CategorizePreconditions" class="anchor"></a><div class="def module"><code><span class="keyword">module </span><a href="CategorizePreconditions/index.html">CategorizePreconditions</a> : <span class="keyword">sig</span> ... <span class="keyword">end</span></code></div><div class="doc"></div></div></body></html> |
