You can not select more than 25 topics
Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.
|
|
|
|
|
<!DOCTYPE html>
|
|
|
|
|
|
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>Prover (infer.InferModules.Prover)</title><link rel="stylesheet" href="../../../odoc.css"/><meta charset="utf-8"/><meta name="generator" content="odoc %%VERSION%%"/><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">InferModules</a> » Prover</nav><h1>Module <code>InferModules.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><li><a href="#subtype-checking">Subtype checking</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="../../../InferIR/InferIR/Tenv/index.html#type-t">InferIR.Tenv.t</a> <span>-></span> <a href="../../../InferIR/InferIR/Sil/index.html#type-atom">InferIR.Sil.atom</a> <span>-></span> <a href="../../../InferIR/InferIR/Sil/index.html#type-atom">InferIR.Sil.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="../../../InferIR/InferIR/Tenv/index.html#type-t">InferIR.Tenv.t</a> <span>-></span> <a href="../../../InferIR/InferIR/Exp/index.html#type-t">InferIR.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="../../../InferIR/InferIR/Tenv/index.html#type-t">InferIR.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="../../../InferIR/InferIR/Exp/index.html#type-t">InferIR.Exp.t</a> <span>-></span> <a href="../../../InferIR/InferIR/Exp/index.html#type-t">InferIR.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="../../../InferIR/InferIR/Tenv/index.html#type-t">InferIR.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="../../../InferIR/InferIR/Exp/index.html#type-t">InferIR.Exp.t</a> <span>-></span> <a href="../../../InferIR/InferIR/Exp/index.html#type-t">InferIR.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-type_size_comparable"><a href="#val-type_size_comparable" class="anchor"></a><code><span class="keyword">val</span> type_size_comparable : <a href="../../../InferIR/InferIR/Typ/index.html#type-t">InferIR.Typ.t</a> <span>-></span> <a href="../../../InferIR/InferIR/Typ/index.html#type-t">InferIR.Typ.t</a> <span>-></span> bool</code></dt><dd><p>Return true if the two types have sizes which can be compared</p></dd></dl><dl><dt class="spec value" id="val-ch
|
|
|
|
|
|
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="../../../InferIR/InferIR/Tenv/index.html#type-t">InferIR.Tenv.t</a> <span>-></span> bool <span>-></span> <a href="../../../InferIR/InferIR/Sil/index.html#type-hpred">InferIR.Sil.hpred</a> <span>-></span> bool * bool * <a href="../../../InferIR/InferIR/Sil/index.html#type-hpred">InferIR.Sil.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="../../../InferIR/InferIR/Tenv/index.html#type-t">InferIR.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="../../../InferIR/InferIR/Exp/index.html#type-t">InferIR.Exp.t</a> <span>-></span> <span><a href="../../../InferIR/InferIR/IntLit/index.html#type-t">InferIR.IntLit.t</a> option</span> * <span><a href="../../../InferIR/InferIR/IntLit/index.html#type-t">InferIR.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 : <a href="../../../InferIR/InferIR/Typ/Procname/index.html#type-t">InferIR.Typ.Procname.t</a> <span>-></span> <a href="../../../InferIR/InferIR/Tenv/index.html#type-t">InferIR.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> <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="../../../InferIR/InferIR/Exp/index.html#type-t">InferIR.Exp.t</a> * <a href="../../../InferIR/InferIR/Exp/index.html#type-t">InferIR.Exp.t</a> * <a href="../../../InferIR/InferIR/Exp/index.html#type-t">InferIR.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="../../../InferIR/InferIR/Exp/index.html#type-t">InferIR.Exp.t</a> * <a href="../../../InferIR/InferIR/Exp/index.html#type-t">InferIR.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_resul
|
|
|
|
|
|
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="../../../InferIR/InferIR/Tenv/index.html#type-t">InferIR.Tenv.t</a> <span>-></span> <span><span>(<span><a href="../../../InferIR/InferIR/Sil/index.html#type-atom">InferIR.Sil.atom</a> list</span> * <span class="type-var">'a</span>)</span> list</span> <span>-></span> <span><span><span>(<span><a href="../../../InferIR/InferIR/Sil/index.html#type-atom">InferIR.Sil.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><section><header><h3 id="subtype-checking"><a href="#subtype-checking" class="anchor"></a>Subtype checking</h3></header><div class="spec module" id="module-Subtyping_check"><a href="#module-Subtyping_check" class="anchor"></a><code><span class="keyword">module</span> <a href="Subtyping_check/index.html">Subtyping_check</a> : <span class="keyword">sig</span> ... <span class="keyword">end</span></code></div></section></div></body></html>
|
