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>PulsePathCondition (infer.Pulselib.PulsePathCondition)</title><linkrel="stylesheet"href="../../../odoc.css"/><metacharset="utf-8"/><metaname="generator"content="odoc 1.5.2"/><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>» PulsePathCondition</nav><h1>Module <code>Pulselib.PulsePathCondition</code></h1><navclass="toc"><ul><li><ahref="#building-arithmetic-constraints">Building arithmetic constraints</a></li><li><ahref="#operations">Operations</a></li><li><ahref="#queries">Queries</a></li></ul></nav></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-AbstractValue"><ahref="#module-AbstractValue"class="anchor"></a><code><spanclass="keyword">module</span> AbstractValue = <ahref="../index.html#module-PulseAbstractValue">PulseAbstractValue</a></code></div><divclass="spec module"id="module-SatUnsat"><ahref="#module-SatUnsat"class="anchor"></a><code><spanclass="keyword">module</span> SatUnsat = <ahref="../index.html#module-PulseSatUnsat">PulseSatUnsat</a></code></div><divclass="spec module"id="module-ValueHistory"><ahref="#module-ValueHistory"class="anchor"></a><code><spanclass="keyword">module</span> ValueHistory = <ahref="../index.html#module-PulseValueHistory">PulseValueHistory</a></code></div><dl><dtclass="spec type"id="type-t"><ahref="#type-t"class="anchor"></a><code><spanclass="keyword">type</span> t</code></dt></dl><div><divclass="spec include"><divclass="doc"><dl><dtclass="spec value"id="val-compare"><ahref="#val-compare"class="anchor"></a><code><spanclass="keyword">val</span> compare : <ahref="index.html#type-t">t</a><span>-></span><ahref="index.html#type-t">t</a><span>-></span> int</code></dt><dtclass="spec value"id="val-equal"><ahref="#val-equal"class="anchor"></a><code><spanclass="keyword">val</span> equal : <ahref="index.html#type-t">t</a><span>-></span><ahref="index.html#type-t">t</a><span>-></span> bool</code></dt><dtclass="spec value"id="val-yojson_of_t"><ahref="#val-yojson_of_t"class="anchor"></a><code><spanclass="keyword">val</span> yojson_of_t : <ahref="index.html#type-t">t</a><span>-></span> Ppx_yojson_conv_lib.Yojson.Safe.t</code></dt></dl></div></div></div><dl><dtclass="spec value"id="val-true_"><ahref="#val-true_"class="anchor"></a><code><spanclass="keyword">val</span> true_ : <ahref="index.html#type-t">t</a></code></dt><dtclass="spec value"id="val-false_"><ahref="#val-false_"class="anchor"></a><code><spanclass="keyword">val</span> false_ : <ahref="index.html#type-t">t</a></code></dt><dtclass="spec value"id="val-pp"><ahref="#val-pp"class="anchor"></a><code><spanclass="keyword">val</span> pp : <ahref="index.html#module-F">F</a>.formatter <span>-></span><ahref="index.html#type-t">t</a><span>-></span> unit</code></dt></dl><dl><dtclass="spec type"id="type-new_eqs"><ahref="#type-new_eqs"class="anchor"></a><code><spanclass="keyword">type</span> new_eqs</code><code> = <ahref="../PulseFormula/index.html#type-new_eqs">PulseFormula.new_eqs</a></code></dt></dl><section><header><h3id="building-arithmetic-constraints"><ahref="#building-arithmetic-constraints"class="anchor"></a>Building arithmetic constraints</h3></header><dl><dtclass="spec value"id="val-and_nonnegative"><ahref="#val-and_nonnegative"class="anchor"></a><code><spanclass="keyword">val</span> and_nonnegative : <ahref="../PulseAbstractValue/index.html#type-t">AbstractValue.t</a><span>-></span><ahref="index.html#type-t">t</a><span>-></span><ahref="index.html#type-t">t</a> * <ahref="index.html#type-new_eqs">new_eqs</a></code></dt><dd><p><code>and_nonnegative v phi</code> is <code>phi ∧ v≥0</code></p></dd></dl><dl><dtclass="spec value"id="val-and_positive"><ahref="#val-and_positive"class="anchor"></a><code><spanclass="keyword">val</span> and_positive : <ahref="../PulseAbstractValue/index.html#type-t">AbstractValue.t</a><span>-></span><ahref="index.html#type-t">t</a><span>-></span><ahref="index.html#type-t">t</a> * <ahref="index.html#type-new_eqs">new_eqs</a></code></dt><dd><p><code>and_positive v phi</code> is <code>phi ∧ v>0</code></p></dd></dl><dl><dtclass="spec value"id="val-and_eq_int"><ahref="#val-and_eq_int"class="anchor"></a><code><spanclass="keyword">val</span> and_eq_int : <ahref="../PulseAbstractValue/index.html#type-t">AbstractValue.t</a><span>-></span><ahref="../../IR/IntLit/index.html#type-t">IR.IntLit.t</a><span>-></span><ahref="index.html#type-t">t</a><span>-></span><ahref="index.html#type-t">t</a> * <ahref="index.html#type-new_eqs">new_eqs</a></code></dt><dd><p><code>and_eq_int v i phi</code> is <code>phi ∧ v=i</code></p></dd></dl><dl><dtclass="spec value"id="val-and_eq_vars"><ahref="#val-and_eq_vars"class="anchor"></a><code><spanclass="keyword">val</span> and_eq_vars : <ahref="../PulseAbstractValue/index.html#type-t">AbstractValue.t</a><span>-></span><ahref="../PulseAbstractValue/index.html#type-t">AbstractValue.t</a><span>-></span><ahref="index.html#type-t">t</a><span>-></span><ahref="index.html#type-t">t</a> * <ahref="index.html#type-new_eqs">new_eqs</a></code></dt><dtclass="spec value"id="val-simplify"><ahref="#val-simplify"class="anchor"></a><code><spanclass="keyword">val</span> simplify : <ahref="../../IR/Tenv/index.html#type-t">IR.Tenv.t</a><span>-></span><span>keep:<ahref="../../Pulselib__PulseAbstractValue/index.html#module-Set">AbstractValue.Set</a>.t</span><span>-></span><span>get_dynamic_type:<span>(<ahref="../PulseAbstractValue/index.html#type-t">AbstractValue.t</a><span>-></span><span><ahref="../../IR/Typ/index.html#type-t">IR.Typ.t</a> option</span>)</span></span><span>-></span><ahref="index.html#type-t">t</a><span>-></span><span><span>(<ahref="index.html#type-t">t</a> * <ahref="index.html#type-new_eqs">new_eqs</a>)</span><ahref="../PulseSatUnsat/index.html#type-t">SatUnsat.t</a></span></code></dt><dd><p><code>simplify ~keep phi</code> attempts to get rid of as many variables in <code>fv phi</code> but not in <code>keep</code> as possible</p></dd></dl><dl><dtclass="spec value"id="val-simplify_instanceof"><ahref="#val-simplify_instanceof"class="anchor"></a><code><spanclass="keyword">val</span> simplify_instanceof : <ahref="../../IR/Tenv/index.html#type-t">IR.Tenv.t</a><span>-></span><span>get_dynamic_type:<span>(<ahref="../PulseAbstractValue/index.html#type-t">AbstractValue.t</a><span>-></span><span><ahref="../../IR/Typ/index.html#type-t">IR.Typ.t</a> option</span>)</span></span><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-and_callee"><ahref="#val-and_callee"class="anchor"></a><code><spanclass="keyword">val</span> and_callee : <span><span>(<ahref="../PulseAbstractValue/index.html#type-t">AbstractValue.t</a> * <ahref="../PulseValueHistory/index.html#type-t">ValueHistory.t</a>)</span><ahref="../../Pulselib__PulseAbstractValue/index.html#module-Map">AbstractValue.Map</a>.t</span><span>-></span><ahref="index.html#type-t">t</a><span>-></span><span>callee:<ahref="index.html#type-t">t</a></span><span>-></span><span><span>(<ahref="../PulseAbstractValue/index.html#type-t">AbstractValue.t</a> * <ahref="../PulseValueHistory/index.html#type-t">ValueHistory.t</a>)</span><ahref="../../Pulselib__PulseAbstractValue/index.html#module-Map">AbstractValue.Map</a>.t</span> * <ahref="index.html#type-t">t</a> * <ahref="index.html#type-new_eqs">new_eqs</a></code></dt></dl></section><section><header><h3id="operations"><ahref="#operations"class="anchor"></a>Operations</h3></header><dl><dtclass="spec type"id="type-operand"><ahref="#type-operand"class="anchor"></a><code><spanclass="keyword">type</span> operand</code><code> = </code><tableclass="variant"><trid="type-operand.LiteralOperand"class="anchored"><tdclass="def constructor"><ahref="#type-operand.LiteralOperand"class="anchor"></a><code>| </code><code><spanclass="constructor">LiteralOperand</span><spanclass="keyword">of</span><ahref="../../IR/IntLit/index.html#type-t">IR.IntLit.t</a></code></td></tr><trid="type-operand.AbstractValueOperand"class="anchored"><tdclass="def constructor"><ahref="#type-operand.AbstractValueOperand"class="anchor"></a><code>| </code><code><spanclass="constructor">AbstractValueOperand</span><spanclass="keyword">of</span><ahref="../PulseAbstractValue/index.html#type-t">AbstractValue.t</a></code></td></tr></table></dt></dl><div><divclass="spec include"><divclass="doc"><dl><dtclass="spec value"id="val-compare_operand"><ahref="#val-compare_operand"class="anchor"></a><code><spanclass="keyword">val</span> compare_operand : <ahref="index.html#type-operand">operand</a><span>-></span><ahref="index.html#type-operand">operand</a><span>-></span> int</code></dt></dl></div></div></div><dl><dtclass="spec value"id="val-pp_operand"><ahref="#val-pp_operand"class="anchor"></a><code><spanclass="keyword">val</span> pp_operand : <ahref="../../IStdlib/index.html#module-IStd">IStdlib.IStd</a>.Formatter.t <span>-></span><ahref="index.html#type-operand">operand</a><span>-></span> unit</code></dt><dtclass="spec value"id="val-eval_binop"><ahref="#val-eval_binop"class="anchor"></a><code><spanclass="keyword">val</span> eval_binop : <ahref="../PulseAbstractValue/index.html#type-t">AbstractValue.t</a><span>-></span><ahref="../../IR/Binop/index.html#type-t">IR.Binop.t</a><span>-></span><ahref="index.html#type-operand">operand</a><span>-></span><ahref="index.html#type-operand">operand</a><span>-></span><ahref="index.html#type-t">t</a><span>-></span><ahref="index.html#type-t">t</a> * <ahref="index.html#type-new_eqs">new_eqs</a></code></dt><dtclass="spec value"id="val-eval_unop"><ahref="#val-eval_unop"class="anchor"></a><code><spanclass="keyword">val</span> eval_unop : <ahref="../PulseAbstractValue/index.html#type-t">AbstractValue.t</a><span>-></span><ahref="../../IR/Unop/index.html#type-t">IR.Unop.t</a><span>-></span><ahref="../PulseAbstractValue/index.html#type-t">AbstractValue.t</a><span>-></span><ahref="index.html#type-t">t</a><span>-></span><ahref="index.html#type-t">t</a> * <ahref="index.html#type-new_eqs">new_eqs</a></code></dt><dtclass="spec value"id="val-prune_binop"><ahref="#val-prune_binop"class="anchor"></a><code><spanclass="keyword">val</span> prune_binop : <span>negated:bool</span><span>-></span><ahref="../../IR/Binop/index.html#type-t">IR.Binop.t</a><span>-></span><ahref="index.html#type-operand">operand</a><span>-></span><ahref="index.html#type-operand">operand</a><span>-></span><ahref="index.html#type-t">t</a><span>-></span><ahref="index.html#type-t">t</a> * <ahref="index.html#type-new_eqs">new_eqs</a></code></dt><dtclass="spec value"id="val-and_eq_instanceof"><ahref="#val-and_eq_instanceof"class="anchor"></a><code><spanclass="keyword">val</span> and_eq_instanceof : <ahref="../PulseAbstractValue/index.html#type-t">AbstractValue.t</a><span>-></span><ahref="../PulseAbstractValue/index.html#type-t">AbstractValue.t</a><span>-></span><ahref="../../IR/Typ/index.html#type-t">IR.Typ.t</a><span>-></span><ahref="index.html#type-t">t</a><span>-></span><ahref="index.html#type-t">t</a> * <ahref="index.html#type-new_eqs">new_eqs</a></code></dt></dl></section><section><header><h3id="queries"><ahref="#queries"class="anchor"></a>Queries</h3></header><dl><dtclass="spec value"id="val-is_known_zero"><ahref="#val-is_known_zero"class="anchor"></a><code><spanclass="keyword">val</span> is_known_zero : <ahref="index.html#type-t">t</a><span>-></span><ahref="../PulseAbstractValue/index.html#type-t">AbstractValue.t</a><span>-></span> bool</code></dt><dd><p><code>is_known_zero phi t</code> returns <code>true</code> if <code>phi |- t = 0</code>, <code>false</code> if we don't know for sure</p></dd></dl><dl><dtclass="spec value"id="val-is_known_not_equal_zero"><ahref="#val-is_known_not_equal_zero"class="anchor"></a><code><spanclass="keyword">val</span> is_known_not_equal_zero : <ahref="index.html#type-t">t</a><span>-></span><ahref="../PulseAbstractValue/index.html#type-t">AbstractValue.t</a><span>-></span> bool</code></dt><dd><p><code>is_known_not_equal_zero phi t</code> returns <code>true</code> if <code>phi |- t != 0</code>, <code>false</code> if we don't know for sure</p></dd></dl><dl><dtclass="spec value"id="val-is_unsat_cheap"><ahref="#val-is_unsat_cheap"class="anchor"></a><code><spanclass="keyword">val</span> is_unsat_cheap : <ahref="index.html#type-t">t</a><span>-></span> bool</code></dt><dd><p>whether the state contains a contradiction, call this as often as you want</p></dd></dl><dl><dtclass="spec value"id="val-is_unsat_expensive"><ahref="#val-is_unsat_expensive"class="anchor"></a><code><spanclass="keyword">val</span> is_unsat_expensive : <ahref="../../IR/Tenv/index.html#type-t">IR.Tenv.t</a><span>-></span><span>get_dynamic_type:<span>(<ahref="../PulseAbstractValue/index.html#type-t">AbstractValue.t</a><span>-></span><span><ahref="../../IR/Typ/index.html#type-t">IR.Typ.t</a> option</span>)</span></span><span>-></span><ahref="index.html#type-t">t</a><span>-></span><ahref="index.html#type-t">t</a> * bool * <ahref="index.html#type-new_eqs">new_eqs</a></code></dt><dd><p>whether the state contains a contradiction, only call this when you absolutely have to</p></dd></dl><dl><dtclass="spec value"id="val-as_int"><ahref="#val-as_int"class="anchor"></a><code><spanclass="keyword">val</span> as_int : <ahref="index.html#type-t">t</a><span>-></span><ahref="../PulseAbstractValue/index.html#type-t">AbstractValue.t</a><span>-></span><span>int option</span></code></dt><dd><p><code>as_int phi t</code> returns an integer x such that <code>phi |- t = x</code>, if known for sure; see also <code>is_known_zero</code></p></dd></dl><dl><dtclass="spec value"id="val-has_no_assumptions"><ahref="#val-has_no_assumptions"class="anchor"></a><code><spanclass="keyword">val</span> has_no_assumptions : <ahref="index.html#type-t">t</a><span>-></span> bool</code></dt><dd><p>whether the current path is independent of any calling context</p></dd></dl><dl><dtclass="spec value"id="val-get_var_repr"><ahref="#val-get_var_repr"class="anchor"></a><code><spanclass="keyword">val</span> get_var_repr : <ahref="index.html#type-t">t</a><span>-></span><ahref="../PulseAbstractValue/index.html#type-t">AbstractValue.t</a><span>-></span><ahref="../PulseAbstractValue/index.html#type-t">AbstractValue.t</a></code></dt><dd><p>get the canonical representative for the variable according to the equality relation</p></dd></dl></section></div></body></html>
