|
|
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>Prover (infer.Biabduction.Prover)</title><link rel="stylesheet" href="../../../odoc.css"/><meta charset="utf-8"/><meta name="generator" content="odoc 1.5.1"/><meta name="viewport" content="width=device-width,initial-scale=1.0"/><script src="../../../highlight.pack.js"></script><script>hljs.initHighlightingOnLoad();</script></head><body><div class="content"><header><nav><a href="../index.html">Up</a> – <a href="../../index.html">infer</a> » <a href="../index.html">Biabduction</a> » Prover</nav><h1>Module <code>Biabduction.Prover</code></h1><nav class="toc"><ul><li><a href="#ordinary-theorem-proving">Ordinary Theorem Proving</a></li><li><a href="#abduction-prover">Abduction prover</a></li><li><a href="#cover:-minimum-set-of-pi's-whose-disjunction-is-equivalent-to-true">Cover: minimum set of pi's whose disjunction is equivalent to true</a></li></ul></nav></header><aside><p>Functions for Theorem Proving</p></aside><dl><dt class="spec value" id="val-atom_negate"><a href="#val-atom_negate" class="anchor"></a><code><span class="keyword">val</span> atom_negate : <a href="../../IR/Tenv/index.html#type-t">IR.Tenv.t</a> <span>-></span> <a href="../Predicates/index.html#type-atom">Predicates.atom</a> <span>-></span> <a href="../Predicates/index.html#type-atom">Predicates.atom</a></code></dt><dd><p>Negate an atom</p></dd></dl><section><header><h3 id="ordinary-theorem-proving"><a href="#ordinary-theorem-proving" class="anchor"></a>Ordinary Theorem Proving</h3></header><dl><dt class="spec value" id="val-check_zero"><a href="#val-check_zero" class="anchor"></a><code><span class="keyword">val</span> check_zero : <a href="../../IR/Tenv/index.html#type-t">IR.Tenv.t</a> <span>-></span> <a href="../../IR/Exp/index.html#type-t">IR.Exp.t</a> <span>-></span> bool</code></dt><dd><p>Check <code>|- e=0</code>. Result <code>false</code> means "don't know".</p></dd></dl><dl><dt class="spec value" id="val-check_equal"><a href="#val-check_equal" class="anchor"></a><code><span class="keyword">val</span> check_equal : <a href="../../IR/Tenv/index.html#type-t">IR.Tenv.t</a> <span>-></span> <span><a href="../Prop/index.html#type-normal">Prop.normal</a> <a href="../Prop/index.html#type-t">Prop.t</a></span> <span>-></span> <a href="../../IR/Exp/index.html#type-t">IR.Exp.t</a> <span>-></span> <a href="../../IR/Exp/index.html#type-t">IR.Exp.t</a> <span>-></span> bool</code></dt><dd><p>Check <code>prop |- exp1=exp2</code>. Result <code>false</code> means "don't know".</p></dd></dl><dl><dt class="spec value" id="val-check_disequal"><a href="#val-check_disequal" class="anchor"></a><code><span class="keyword">val</span> check_disequal : <a href="../../IR/Tenv/index.html#type-t">IR.Tenv.t</a> <span>-></span> <span><a href="../Prop/index.html#type-normal">Prop.normal</a> <a href="../Prop/index.html#type-t">Prop.t</a></span> <span>-></span> <a href="../../IR/Exp/index.html#type-t">IR.Exp.t</a> <span>-></span> <a href="../../IR/Exp/index.html#type-t">IR.Exp.t</a> <span>-></span> bool</code></dt><dd><p>Check whether <code>prop |- exp1!=exp2</code>. Result <code>false</code> means "don't know".</p></dd></dl><dl><dt class="spec value" id="val-check_atom"><a href="#val-check_atom" class="anchor"></a><code><span class="keyword">val</span> check_atom : <a href="../../IR/Tenv/index.html#type-t">IR.Tenv.t</a> <span>-></span> <span><a href="../Prop/index.html#type-normal">Prop.normal</a> <a href="../Prop/index.html#type-t">Prop.t</a></span> <span>-></span> <a href="../Predicates/index.html#type-atom">Predicates.atom</a> <span>-></span> bool</code></dt><dd><p>Check whether <code>prop |- a</code>. Result <code>false</code> means "don't know".</p></dd></dl><dl><dt class="spec value" id="val-check_inconsistency_base"><a href="#val-check_inconsistency_base" class="anchor"></a><code><span class="keyword">val</span> check_inconsistency_base : <a href="../../IR/Tenv/index.html#type-t">IR.Tenv.t</a> <span>-></span> <span><a href="../Prop/index.html#type-normal">Prop.normal</a> <a href="../Prop/index.html#type-t">Prop.t</a></span> <span>-></span> bool</code></dt><dd><p>Inconsistency checking ignoring footprint.</p></dd></dl><dl><dt class="spec value" id="val-check_inconsistency"><a href="#val-check_inconsistency" class="anchor"></a><code><span class="keyword">val</span> check_inconsistency : <a href="../../IR/Tenv/index.html#type-t">IR.Tenv.t</a> <span>-></span> <span><a href="../Prop/index.html#type-normal">Prop.normal</a> <a href="../Prop/index.html#type-t">Prop.t</a></span> <span>-></span> bool</code></dt><dd><p>Inconsistency checking.</p></dd></dl><dl><dt class="spec value" id="val-check_allocatedness"><a href="#val-check_allocatedness" class="anchor"></a><code><span class="keyword">val</span> check_allocatedness : <a href="../../IR/Tenv/index.html#type-t">IR.Tenv.t</a> <span>-></span> <span><a href="../Prop/index.html#type-normal">Prop.normal</a> <a href="../Prop/index.html#type-t">Prop.t</a></span> <span>-></span> <a href="../../IR/Exp/index.html#type-t">IR.Exp.t</a> <span>-></span> bool</code></dt><dd><p>Check whether <code>prop |- allocated(exp)</code>.</p></dd></dl><dl><dt class="spec value" id="val-is_root"><a href="#val-is_root" class="anchor"></a><code><span class="keyword">val</span> is_root : <a href="../../IR/Tenv/index.html#type-t">IR.Tenv.t</a> <span>-></span> <span><a href="../Prop/index.html#type-normal">Prop.normal</a> <a href="../Prop/index.html#type-t">Prop.t</a></span> <span>-></span> <a href="../../IR/Exp/index.html#type-t">IR.Exp.t</a> <span>-></span> <a href="../../IR/Exp/index.html#type-t">IR.Exp.t</a> <span>-></span> <span><span><a href="../Predicates/index.html#type-offset">Predicates.offset</a> list</span> option</span></code></dt><dd><p><code>is_root prop base_exp exp</code> checks whether <code>base_exp = exp.offlist</code> for some list of offsets <code>offlist</code>. If so, it returns <code>Some(offlist)</code>. Otherwise, it returns <code>None</code>. Assumes that <code>base_exp</code> points to the beginning of a structure, not the middle.</p></dd></dl><dl><dt class="spec value" id="val-expand_hpred_pointer"><a href="#val-expand_hpred_pointer" class="anchor"></a><code><span class="keyword">val</span> expand_hpred_pointer : <a href="../../IR/Tenv/index.html#type-t">IR.Tenv.t</a> <span>-></span> bool <span>-></span> <a href="../Predicates/index.html#type-hpred">Predicates.hpred</a> <span>-></span> bool * bool * <a href="../Predicates/index.html#type-hpred">Predicates.hpred</a></code></dt><dd><p><code>expand_hpred_pointer calc_index_frame hpred</code> expands <code>hpred</code> if it is a |-> whose lhs is a Lfield or Lindex or ptr+off. Return <code>(changed, calc_index_frame', hpred')</code> where <code>changed</code> indicates whether the predicate has changed.</p></dd></dl><dl><dt class="spec value" id="val-get_bounds"><a href="#val-get_bounds" class="anchor"></a><code><span class="keyword">val</span> get_bounds : <a href="../../IR/Tenv/index.html#type-t">IR.Tenv.t</a> <span>-></span> <span><a href="../Prop/index.html#type-normal">Prop.normal</a> <a href="../Prop/index.html#type-t">Prop.t</a></span> <span>-></span> <a href="../../IR/Exp/index.html#type-t">IR.Exp.t</a> <span>-></span> <span><a href="../../IR/IntLit/index.html#type-t">IR.IntLit.t</a> option</span> * <span><a href="../../IR/IntLit/index.html#type-t">IR.IntLit.t</a> option</span></code></dt><dd><p>Get upper and lower bounds of an expression, if any</p></dd></dl></section><section><header><h3 id="abduction-prover"><a href="#abduction-prover" class="anchor"></a>Abduction prover</h3></header><dl><dt class="spec value" id="val-check_implication"><a href="#val-check_implication" class="anchor"></a><code><span class="keyword">val</span> check_implication : <span><a href="../BiabductionSummary/index.html#type-t">BiabductionSummary.t</a> <a href="../../Absint/InterproceduralAnalysis/index.html#type-t">Absint.InterproceduralAnalysis.t</a></span> <span>-></span> <span><a href="../Prop/index.html#type-normal">Prop.normal</a> <a href="../Prop/index.html#type-t">Prop.t</a></span> <span>-></span> <span><a href="../Prop/index.html#type-exposed">Prop.exposed</a> <a href="../Prop/index.html#type-t">Prop.t</a></span> <span>-></span> bool</code></dt><dd><p><code>check_implication p1 p2</code> returns true if <code>p1|-p2</code></p></dd></dl><dl><dt class="spec type" id="type-check"><a href="#type-check" class="anchor"></a><code><span class="keyword">type</span> check</code><code> = </code><table class="variant"><tr id="type-check.Bounds_check" class="anchored"><td class="def constructor"><a href="#type-check.Bounds_check" class="anchor"></a><code>| </code><code><span class="constructor">Bounds_check</span></code></td></tr><tr id="type-check.Class_cast_check" class="anchored"><td class="def constructor"><a href="#type-check.Class_cast_check" class="anchor"></a><code>| </code><code><span class="constructor">Class_cast_check</span> <span class="keyword">of</span> <a href="../../IR/Exp/index.html#type-t">IR.Exp.t</a> * <a href="../../IR/Exp/index.html#type-t">IR.Exp.t</a> * <a href="../../IR/Exp/index.html#type-t">IR.Exp.t</a></code></td></tr></table></dt></dl><dl><dt class="spec value" id="val-d_typings"><a href="#val-d_typings" class="anchor"></a><code><span class="keyword">val</span> d_typings : <span><span>(<a href="../../IR/Exp/index.html#type-t">IR.Exp.t</a> * <a href="../../IR/Exp/index.html#type-t">IR.Exp.t</a>)</span> list</span> <span>-></span> unit</code></dt></dl><dl><dt class="spec type" id="type-implication_result"><a href="#type-implication_result" class="anchor"></a><code><span class="keyword">type</span> implication_result</code><code> = </code><table class="variant"><tr id="type-implication_result.ImplOK" class="anchored"><td class="def constructor"><a href="#type-implication_result.ImplOK" class="anchor"></a><code>| </code><code><span class="constructor">ImplOK</span> <span class="keyword">of</span> <span><a href="index.html#type-check">check</a> list</span> * <a href="../Predicates/index.html#type-subst">Predicates.subst</a> * <a href="../Predicates/index.html#type-subst">Predicates.subst</a> * <span><a href="../Predicates/index.html#type-hpred">Predicates.hpred</a> list</span> * <span><a href="../Predicates/index.html#type-atom">Predicates.atom</a> list</span> * <span><a href="../Predicates/index.html#type-hpred">Predicates.hpred</a> list</span> * <span><a href="../Predicates/index.html#type-hpred">Predicates.hpred</a> list</span> * <span><a href="../Predicates/index.html#type-hpred">Predicates.hpred</a> list</span> * <span><span>(<a href="../../IR/Exp/index.html#type-t">IR.Exp.t</a> * <a href="../../IR/Exp/index.html#type-t">IR.Exp.t</a>)</span> list</span> * <span><span>(<a href="../../IR/Exp/index.html#type-t">IR.Exp.t</a> * <a href="../../IR/Exp/index.html#type-t">IR.Exp.t</a>)</span> list</span></code></td></tr><tr id="type-implication_result.ImplFail" class="anchored"><td class="def constructor"><a href="#type-implication_result.ImplFail" class="anchor"></a><code>| </code><code><span class="constructor">ImplFail</span> <span class="keyword">of</span> <span><a href="index.html#type-check">check</a> list</span></code></td></tr></table></dt></dl><dl><dt class="spec value" id="val-check_implication_for_footprint"><a href="#val-check_implication_for_footprint" class="anchor"></a><code><span class="keyword">val</span> check_implication_for_footprint : <span><a href="../BiabductionSummary/index.html#type-t">BiabductionSummary.t</a> <a href="../../Absint/InterproceduralAnalysis/index.html#type-t">Absint.InterproceduralAnalysis.t</a></span> <span>-></span> <span><a href="../Prop/index.html#type-normal">Prop.normal</a> <a href="../Prop/index.html#type-t">Prop.t</a></span> <span>-></span> <span><a href="../Prop/index.html#type-exposed">Prop.exposed</a> <a href="../Prop/index.html#type-t">Prop.t</a></span> <span>-></span> <a href="index.html#type-implication_result">implication_result</a></code></dt><dd><p><code>check_implication_for_footprint p1 p2</code> returns <code>Some(sub, frame, missing)</code> if <code>sub(p1 * missing) |- sub(p2 * frame)</code> where <code>sub</code> is a substitution which instantiates the primed vars of <code>p1</code> and <code>p2</code>, which are assumed to be disjoint.</p></dd></dl></section><section><header><h3 id="cover:-minimum-set-of-pi's-whose-disjunction-is-equivalent-to-true"><a href="#cover:-minimum-set-of-pi's-whose-disjunction-is-equivalent-to-true" class="anchor"></a>Cover: minimum set of pi's whose disjunction is equivalent to true</h3></header><dl><dt class="spec value" id="val-find_minimum_pure_cover"><a href="#val-find_minimum_pure_cover" class="anchor"></a><code><span class="keyword">val</span> find_minimum_pure_cover : <a href="../../IR/Tenv/index.html#type-t">IR.Tenv.t</a> <span>-></span> <span><span>(<span><a href="../Predicates/index.html#type-atom">Predicates.atom</a> list</span> * <span class="type-var">'a</span>)</span> list</span> <span>-></span> <span><span><span>(<span><a href="../Predicates/index.html#type-atom">Predicates.atom</a> list</span> * <span class="type-var">'a</span>)</span> list</span> option</span></code></dt><dd><p>Find minimum set of pi's in <code>cases</code> whose disjunction covers true</p></dd></dl></section></div></body></html> |