pghs975uc
/
infer_clone
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity
infer_clone/website/static/odoc/0.17.0/infer/InferModules/Prover/index.html

4 lines
16 KiB
Raw Blame History Escape

This file contains ambiguous Unicode characters!

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>
<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> &#x00BB; <a href="../index.html">InferModules</a> &#x00BB; 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>&#45;&gt;</span> <a href="../../../InferIR/InferIR/Sil/index.html#type-atom">InferIR.Sil.atom</a> <span>&#45;&gt;</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>&#45;&gt;</span> <a href="../../../InferIR/InferIR/Exp/index.html#type-t">InferIR.Exp.t</a> <span>&#45;&gt;</span> bool</code></dt><dd><p>Check <code> |- e=0</code>. Result <code>false</code> means &quot;don't know&quot;.</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>&#45;&gt;</span> <span><a href="../Prop/index.html#type-normal">Prop.normal</a> <a href="../Prop/index.html#type-t">Prop.t</a></span> <span>&#45;&gt;</span> <a href="../../../InferIR/InferIR/Exp/index.html#type-t">InferIR.Exp.t</a> <span>&#45;&gt;</span> <a href="../../../InferIR/InferIR/Exp/index.html#type-t">InferIR.Exp.t</a> <span>&#45;&gt;</span> bool</code></dt><dd><p>Check <code>prop |- exp1=exp2</code>. Result <code>false</code> means &quot;don't know&quot;.</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>&#45;&gt;</span> <span><a href="../Prop/index.html#type-normal">Prop.normal</a> <a href="../Prop/index.html#type-t">Prop.t</a></span> <span>&#45;&gt;</span> <a href="../../../InferIR/InferIR/Exp/index.html#type-t">InferIR.Exp.t</a> <span>&#45;&gt;</span> <a href="../../../InferIR/InferIR/Exp/index.html#type-t">InferIR.Exp.t</a> <span>&#45;&gt;</span> bool</code></dt><dd><p>Check whether <code>prop |- exp1!=exp2</code>. Result <code>false</code> means &quot;don't know&quot;.</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>&#45;&gt;</span> <a href="../../../InferIR/InferIR/Typ/index.html#type-t">InferIR.Typ.t</a> <span>&#45;&gt;</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-check_type_size_leq"><a href="#val-check_type_size_leq" class="anchor"></a><code><span class="keyword">val</span> check_type_size_leq : <a href="../../../InferIR/InferIR/Typ/index.html#type-t">InferIR.Typ.t</a> <span>&#45;&gt;</span> <a href="../../../InferIR/InferIR/Typ/index.html#type-t">InferIR.Typ.t</a> <span>&#45;&gt;</span> bool</code></dt><dd><p>Check &lt;= on the size of comparable types</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="../../../InferIR/InferIR/Tenv/index.html#type-t">InferIR.Tenv.t</a> <span>&#45;&gt;</span> <span><a href="../Prop/index.html#type-normal">Prop.normal</a> <a href="../Prop/index.html#type-t">Prop.t</a></span> <span>&#45;&gt;</span> <a href="../../../InferIR/InferIR/Sil/index.html#type-atom">InferIR.Sil.atom</a> <span>&#45;&gt;</span> bool</code></dt><dd><p>Check whether <code>prop |- a</code>. Result <code>false</code> means &quot;don't know&quot;.</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="../../../InferIR/InferIR/Tenv/index.html#type-t">InferIR.Tenv.t</a> <span>&#45;&gt;</span> <span><a href="../Prop/index.html#type-normal">Prop.normal</a> <a href="../Prop/index.html#type-t">Prop.t</a></span> <span>&#45;&gt;</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="../../../InferIR/InferIR/Tenv/index.html#type-t">InferIR.Tenv.t</a> <span>&#45;&gt;</span> <span><a href="../Prop/index.html#type-normal">Prop.normal</a> <a href="../Prop/index.html#type-t">Prop.t</a></span> <span>&#45;&gt;</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="../../../InferIR/InferIR/Tenv/index.html#type-t">InferIR.Tenv.t</a> <span>&#45;&gt;</span> <span><a href="../Prop/index.html#type-normal">Prop.normal</a> <a href="../Prop/index.html#type-t">Prop.t</a></span> <span>&#45;&gt;</span> <a href="../../../InferIR/InferIR/Exp/index.html#type-t">InferIR.Exp.t</a> <span>&#45;&gt;</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="../../../InferIR/InferIR/Tenv/index.html#type-t">InferIR.Tenv.t</a> <span>&#45;&gt;</span> <span><a href="../Prop/index.html#type-normal">Prop.normal</a> <a href="../Prop/index.html#type-t">Prop.t</a></span> <span>&#45;&gt;</span> <a href="../../../InferIR/InferIR/Exp/index.html#type-t">InferIR.Exp.t</a> <span>&#45;&gt;</span> <a href="../../../InferIR/InferIR/Exp/index.html#type-t">InferIR.Exp.t</a> <span>&#45;&gt;</span> <span><span><a href="../../../InferIR/InferIR/Sil/index.html#type-offset">InferIR.Sil.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="../../../InferIR/InferIR/Tenv/index.html#type-t">InferIR.Tenv.t</a> <span>&#45;&gt;</span> bool <span>&#45;&gt;</span> <a href="../../../InferIR/InferIR/Sil/index.html#type-hpred">InferIR.Sil.hpred</a> <span>&#45;&gt;</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 |-&gt; 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>&#45;&gt;</span> <span><a href="../Prop/index.html#type-normal">Prop.normal</a> <a href="../Prop/index.html#type-t">Prop.t</a></span> <span>&#45;&gt;</span> <a href="../../../InferIR/InferIR/Exp/index.html#type-t">InferIR.Exp.t</a> <span>&#45;&gt;</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>&#45;&gt;</span> <a href="../../../InferIR/InferIR/Tenv/index.html#type-t">InferIR.Tenv.t</a> <span>&#45;&gt;</span> <span><a href="../Prop/index.html#type-normal">Prop.normal</a> <a href="../Prop/index.html#type-t">Prop.t</a></span> <span>&#45;&gt;</span> <span><a href="../Prop/index.html#type-exposed">Prop.exposed</a> <a href="../Prop/index.html#type-t">Prop.t</a></span> <span>&#45;&gt;</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>&#45;&gt;</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="../../../InferIR/InferIR/Sil/index.html#type-subst">InferIR.Sil.subst</a> * <a href="../../../InferIR/InferIR/Sil/index.html#type-subst">InferIR.Sil.subst</a> * <span><a href="../../../InferIR/InferIR/Sil/index.html#type-hpred">InferIR.Sil.hpred</a> list</span> * <span><a href="../../../InferIR/InferIR/Sil/index.html#type-atom">InferIR.Sil.atom</a> list</span> * <span><a href="../../../InferIR/InferIR/Sil/index.html#type-hpred">InferIR.Sil.hpred</a> list</span> * <span><a href="../../../InferIR/InferIR/Sil/index.html#type-hpred">InferIR.Sil.hpred</a> list</span> * <span><a href="../../../InferIR/InferIR/Sil/index.html#type-hpred">InferIR.Sil.hpred</a> list</span> * <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>(<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></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 : <a href="../../../InferIR/InferIR/Typ/Procname/index.html#type-t">InferIR.Typ.Procname.t</a> <span>&#45;&gt;</span> <a href="../../../InferIR/InferIR/Tenv/index.html#type-t">InferIR.Tenv.t</a> <span>&#45;&gt;</span> <span><a href="../Prop/index.html#type-normal">Prop.normal</a> <a href="../Prop/index.html#type-t">Prop.t</a></span> <span>&#45;&gt;</span> <span><a href="../Prop/index.html#type-exposed">Prop.exposed</a> <a href="../Prop/index.html#type-t">Prop.t</a></span> <span>&#45;&gt;</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="../../../InferIR/InferIR/Tenv/index.html#type-t">InferIR.Tenv.t</a> <span>&#45;&gt;</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>&#45;&gt;</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>
Reference in new issue View Git Blame Copy Permalink