[website] Add documentation for Nil Messaging of non-POD return type issue

Reviewed By: jvillard

Differential Revision: D28964438

fbshipit-source-id: 1579cc7d2

infer/documentation/issues/NIL_MESSAGING_TO_NON_POD.md

@@ -0,0 +1,24 @@
+In Objective-C, calling a method on `nil` (or in Objective-C terms, sending a message to `nil`) does not crash,
+it simply returns a falsy value (nil/0/false). However, sending a message that returns
+a non-POD C++ type (POD being ["Plain Old Data"](https://en.cppreference.com/w/cpp/named_req/PODType), essentially
+anything that cannot be compiled as a C-style struct) to `nil` causes undefined behaviour.
+
+```objectivec
+std::shared_ptr<int> callMethodReturnsnonPOD() {
+  SomeObject* obj = getObjectOrNil();
+  std::shared_ptr<int> d = [obj returnsnonPOD]; // UB
+  return d;
+}
+```
+
+To fix the above issue, we need to check if `obj` is
+not `nil` before calling the `returnsnonPOD` method:
+
+```objectivec
+std::shared_ptr<int> callMethodReturnsnonPOD(bool b) {
+  SomeObject* obj = getObjectOrNil(b);
+  if (obj == nil) { return std::make_shared<int>(0); }
+  std::shared_ptr<int> d = [obj returnsnonPOD];
+  return d;
+}
+```

infer/src/base/IssueType.ml

@@ -801,9 +801,7 @@ let nil_insertion_into_collection =
 
 let nil_messaging_to_non_pod =
   register ~id:"NIL_MESSAGING_TO_NON_POD" Error Pulse
-    ~user_documentation:
-      "Calling a method that returns a C++ non-POD object on the nil object is undefined behavior \
-       in Objective-C++."
+    ~user_documentation:[%blob "../../documentation/issues/NIL_MESSAGING_TO_NON_POD.md"]
 
 
 let null_dereference =

website/docs/all-issue-types.md

@@ -1315,7 +1315,31 @@ Inserting nil into a collection is an error in Objective-C.
 
 Reported as "Nil Messaging To Non Pod" by [pulse](/docs/next/checker-pulse).
 
-Calling a method that returns a C++ non-POD object on the nil object is undefined behavior in Objective-C++.
+In Objective-C, calling a method on `nil` (or in Objective-C terms, sending a message to `nil`) does not crash,
+it simply returns a falsy value (nil/0/false). However, sending a message that returns
+a non-POD C++ type (POD being ["Plain Old Data"](https://en.cppreference.com/w/cpp/named_req/PODType), essentially
+anything that cannot be compiled as a C-style struct) to `nil` causes undefined behaviour.
+
+```objectivec
+std::shared_ptr<int> callMethodReturnsnonPOD() {
+  SomeObject* obj = getObjectOrNil();
+  std::shared_ptr<int> d = [obj returnsnonPOD]; // UB
+  return d;
+}
+```
+
+To fix the above issue, we need to check if `obj` is
+not `nil` before calling the `returnsnonPOD` method:
+
+```objectivec
+std::shared_ptr<int> callMethodReturnsnonPOD(bool b) {
+  SomeObject* obj = getObjectOrNil(b);
+  if (obj == nil) { return std::make_shared<int>(0); }
+  std::shared_ptr<int> d = [obj returnsnonPOD];
+  return d;
+}
+```
+
 ## NULLPTR_DEREFERENCE
 
 Reported as "Nullptr Dereference" by [pulse](/docs/next/checker-pulse).

website/docs/checker-uninit.md

@@ -5,6 +5,8 @@ description: "Warns when values are used before having been initialized."
 
 Warns when values are used before having been initialized.
 
+**\*\*\*DEPRECATED\*\*\*** Uninitialized value checking has moved to Pulse.
+
 Activate with `--uninit`.
 
 Supported languages:

website/static/man/next/infer-analyze.1.html

@@ -250,8 +250,8 @@ reporting. (Conversely: <b>--deduplicate</b>)</p>
 <b>--inefficient-keyset-iterator</b>, <b>--linters</b>,
 <b>--liveness</b>, <b>--racerd</b>,
 <b>--dotnet-resource-leak</b>, <b>--siof</b>,
-<b>--self-in-block</b>, <b>--starvation</b>, <b>--uninit</b>
-(Conversely: <b>--default-checkers</b>)</p>
+<b>--self-in-block</b>, <b>--starvation</b> (Conversely:
+<b>--default-checkers</b>)</p>
 
 <p style="margin-left:11%;"><b>--eradicate</b></p>
 
@@ -597,8 +597,8 @@ disable all other checkers (Conversely:
 on program paths that contain calls to unknown methods
 (those without implementation) are not reported unless all
 the unknown method names match this pattern. If the empty
-list is provided or
---pulse_report_ignore_unknown_java_methods_patterns-reset,
+list is provided with
+<b>--pulse-report-ignore-unknown-java-methods-patterns-reset</b>,
 all issues will be reported regardless the presence of
 unknown code</p>
 
@@ -763,11 +763,11 @@ temporal properties over multiple objects. (Conversely:
 disable all other checkers (Conversely:
 <b>--no-topl-only</b>)</p>
 
-<p style="margin-left:11%;"><b>--no-uninit</b></p>
+<p style="margin-left:11%;"><b>--uninit</b></p>
 
-<p style="margin-left:17%;">Deactivates: checker uninit:
+<p style="margin-left:17%;">Activates: checker uninit:
 Warns when values are used before having been initialized.
-(Conversely: <b>--uninit</b>)</p>
+(Conversely: <b>--no-uninit</b>)</p>
 
 <p style="margin-left:11%;"><b>--uninit-only</b></p>
 

website/static/man/next/infer-report.1.html

@@ -350,7 +350,7 @@ PRECONDITION_NOT_FOUND (enabled by default), <br>
 PRECONDITION_NOT_MET (enabled by default), <br>
 PREMATURE_NIL_TERMINATION_ARGUMENT (enabled by default),
 <br>
-PULSE_UNINITIALIZED_VALUE (disabled by default), <br>
+PULSE_UNINITIALIZED_VALUE (enabled by default), <br>
 PURE_FUNCTION (enabled by default), <br>
 QUANDARY_TAINT_ERROR (enabled by default), <br>
 RESOURCE_LEAK (enabled by default), <br>

website/static/man/next/infer.1.html

@@ -709,8 +709,8 @@ infer-reportdiff</b>(1). <b><br>
 <b>--inefficient-keyset-iterator</b>, <b>--linters</b>,
 <b>--liveness</b>, <b>--racerd</b>,
 <b>--dotnet-resource-leak</b>, <b>--siof</b>,
-<b>--self-in-block</b>, <b>--starvation</b>, <b>--uninit</b>
-(Conversely: <b>--default-checkers</b>)</p>
+<b>--self-in-block</b>, <b>--starvation</b> (Conversely:
+<b>--default-checkers</b>)</p>
 
 <p style="margin-left:11%;">See also
 <b>infer-analyze</b>(1). <b><br>
@@ -906,7 +906,7 @@ PRECONDITION_NOT_FOUND (enabled by default), <br>
 PRECONDITION_NOT_MET (enabled by default), <br>
 PREMATURE_NIL_TERMINATION_ARGUMENT (enabled by default),
 <br>
-PULSE_UNINITIALIZED_VALUE (disabled by default), <br>
+PULSE_UNINITIALIZED_VALUE (enabled by default), <br>
 PURE_FUNCTION (enabled by default), <br>
 QUANDARY_TAINT_ERROR (enabled by default), <br>
 RESOURCE_LEAK (enabled by default), <br>
@@ -1786,8 +1786,8 @@ disable all other checkers (Conversely:
 on program paths that contain calls to unknown methods
 (those without implementation) are not reported unless all
 the unknown method names match this pattern. If the empty
-list is provided or
---pulse_report_ignore_unknown_java_methods_patterns-reset,
+list is provided with
+<b>--pulse-report-ignore-unknown-java-methods-patterns-reset</b>,
 all issues will be reported regardless the presence of
 unknown code</p>
 
@@ -2244,11 +2244,11 @@ disable all other checkers (Conversely:
 
 <p style="margin-left:11%;">See also
 <b>infer-analyze</b>(1). <b><br>
---no-uninit</b></p>
+--uninit</b></p>
 
-<p style="margin-left:17%;">Deactivates: checker uninit:
+<p style="margin-left:17%;">Activates: checker uninit:
 Warns when values are used before having been initialized.
-(Conversely: <b>--uninit</b>)</p>
+(Conversely: <b>--no-uninit</b>)</p>
 
 <p style="margin-left:11%;">See also
 <b>infer-analyze</b>(1). <b><br>
@@ -2421,6 +2421,9 @@ without their leading &quot;--&quot;, and values depend on
 the type of the option: <br>
 - for switches options, the value is a JSON boolean (true or
 false, without quotes) <br>
+- for non-switches options with no arguments (for instance
+the undefined option associated with a list option), the
+value is null <br>
 - for integers, the value is a JSON integer (without quotes)
 <br>
 - string options have string values <br>

website/static/odoc/next/infer/Absint/AbstractDomain/PairNoJoin/argument-1-Domain1/index.html

@@ -0,0 +1,2 @@
+<!DOCTYPE html>
+<html xmlns="http://www.w3.org/1999/xhtml"><head><title>1-Domain1 (infer.Absint.AbstractDomain.PairNoJoin.1-Domain1)</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> &#x00BB; <a href="../../../index.html">Absint</a> &#x00BB; <a href="../../index.html">AbstractDomain</a> &#x00BB; <a href="../index.html">PairNoJoin</a> &#x00BB; 1-Domain1</nav><h1>Parameter <code>PairNoJoin.1-Domain1</code></h1></header><div><div class="spec include"><div class="doc"><details open="open"><summary><span class="def"><code><span class="keyword">include</span> <a href="../../../../IStdlib/PrettyPrintable/index.html#module-type-PrintableType">IStdlib.PrettyPrintable.PrintableType</a></code></span></summary><dl><dt class="spec type" id="type-t"><a href="#type-t" class="anchor"></a><code><span class="keyword">type</span> t</code></dt></dl><dl><dt class="spec value" id="val-pp"><a href="#val-pp" class="anchor"></a><code><span class="keyword">val</span> pp : <a href="../../../../IStdlib/PrettyPrintable/index.html#module-F">IStdlib.PrettyPrintable.F</a>.formatter <span>&#45;&gt;</span> <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> unit</code></dt></dl></details></div></div></div><dl><dt class="spec value" id="val-leq"><a href="#val-leq" class="anchor"></a><code><span class="keyword">val</span> leq : <span>lhs:<a href="index.html#type-t">t</a></span> <span>&#45;&gt;</span> <span>rhs:<a href="index.html#type-t">t</a></span> <span>&#45;&gt;</span> bool</code></dt><dd><p>the implication relation: <code>lhs &lt;= rhs</code> means <code>lhs |- rhs</code></p></dd></dl></div></body></html>

website/static/odoc/next/infer/Absint/AbstractDomain/PairNoJoin/argument-2-Domain2/index.html

@@ -0,0 +1,2 @@
+<!DOCTYPE html>
+<html xmlns="http://www.w3.org/1999/xhtml"><head><title>2-Domain2 (infer.Absint.AbstractDomain.PairNoJoin.2-Domain2)</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> &#x00BB; <a href="../../../index.html">Absint</a> &#x00BB; <a href="../../index.html">AbstractDomain</a> &#x00BB; <a href="../index.html">PairNoJoin</a> &#x00BB; 2-Domain2</nav><h1>Parameter <code>PairNoJoin.2-Domain2</code></h1></header><div><div class="spec include"><div class="doc"><details open="open"><summary><span class="def"><code><span class="keyword">include</span> <a href="../../../../IStdlib/PrettyPrintable/index.html#module-type-PrintableType">IStdlib.PrettyPrintable.PrintableType</a></code></span></summary><dl><dt class="spec type" id="type-t"><a href="#type-t" class="anchor"></a><code><span class="keyword">type</span> t</code></dt></dl><dl><dt class="spec value" id="val-pp"><a href="#val-pp" class="anchor"></a><code><span class="keyword">val</span> pp : <a href="../../../../IStdlib/PrettyPrintable/index.html#module-F">IStdlib.PrettyPrintable.F</a>.formatter <span>&#45;&gt;</span> <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> unit</code></dt></dl></details></div></div></div><dl><dt class="spec value" id="val-leq"><a href="#val-leq" class="anchor"></a><code><span class="keyword">val</span> leq : <span>lhs:<a href="index.html#type-t">t</a></span> <span>&#45;&gt;</span> <span>rhs:<a href="index.html#type-t">t</a></span> <span>&#45;&gt;</span> bool</code></dt><dd><p>the implication relation: <code>lhs &lt;= rhs</code> means <code>lhs |- rhs</code></p></dd></dl></div></body></html>

website/static/odoc/next/infer/Absint/AbstractDomain/PairNoJoin/index.html

@@ -0,0 +1,2 @@
+<!DOCTYPE html>
+<html xmlns="http://www.w3.org/1999/xhtml"><head><title>PairNoJoin (infer.Absint.AbstractDomain.PairNoJoin)</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> &#x00BB; <a href="../../index.html">Absint</a> &#x00BB; <a href="../index.html">AbstractDomain</a> &#x00BB; PairNoJoin</nav><h1>Module <code>AbstractDomain.PairNoJoin</code></h1></header><h3 class="heading">Parameters</h3><ul><li><code><a href="argument-1-Domain1/index.html">Domain1</a> : <a href="../index.html#module-type-NoJoin">NoJoin</a></code></li><li><code><a href="argument-2-Domain2/index.html">Domain2</a> : <a href="../index.html#module-type-NoJoin">NoJoin</a></code></li></ul><h3 class="heading">Signature</h3><div><div class="spec include"><div class="doc"><details open="open"><summary><span class="def"><code><span class="keyword">include</span> <a href="../../../IStdlib/PrettyPrintable/index.html#module-type-PrintableType">IStdlib.PrettyPrintable.PrintableType</a></code></span></summary><dl><dt class="spec type" id="type-t"><a href="#type-t" class="anchor"></a><code><span class="keyword">type</span> t</code></dt></dl><dl><dt class="spec value" id="val-pp"><a href="#val-pp" class="anchor"></a><code><span class="keyword">val</span> pp : <a href="../../../IStdlib/PrettyPrintable/index.html#module-F">IStdlib.PrettyPrintable.F</a>.formatter <span>&#45;&gt;</span> <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> unit</code></dt></dl></details></div></div></div><dl><dt class="spec value" id="val-leq"><a href="#val-leq" class="anchor"></a><code><span class="keyword">val</span> leq : <span>lhs:<a href="index.html#type-t">t</a></span> <span>&#45;&gt;</span> <span>rhs:<a href="index.html#type-t">t</a></span> <span>&#45;&gt;</span> bool</code></dt><dd><p>the implication relation: <code>lhs &lt;= rhs</code> means <code>lhs |- rhs</code></p></dd></dl></div></body></html>

website/static/odoc/next/infer/Absint/TaskSchedulerTypes/index.html

@@ -1,2 +1,2 @@
 <!DOCTYPE html>
-<html xmlns="http://www.w3.org/1999/xhtml"><head><title>TaskSchedulerTypes (infer.Absint.TaskSchedulerTypes)</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> &#x00BB; <a href="../index.html">Absint</a> &#x00BB; TaskSchedulerTypes</nav><h1>Module <code>Absint.TaskSchedulerTypes</code></h1></header><dl><dt class="spec exception" id="exception-ProcnameAlreadyLocked"><a href="#exception-ProcnameAlreadyLocked" class="anchor"></a><code><span class="keyword">exception</span> </code><code><span class="exception">ProcnameAlreadyLocked</span> <span class="keyword">of</span> </code><code>{</code><table class="record"><tr id=".dependency_filename" class="anchored"><td class="def field"><a href="#.dependency_filename" class="anchor"></a><code>dependency_filename : string;</code></td></tr></table><code>}</code></dt><dd><p>for the Restart scheduler: raise when a worker tries to analyze a procedure already being analyzed by another process</p></dd></dl><dl><dt class="spec type" id="type-target"><a href="#type-target" class="anchor"></a><code><span class="keyword">type</span> target</code><code> = </code><table class="variant"><tr id="type-target.Procname" class="anchored"><td class="def constructor"><a href="#type-target.Procname" class="anchor"></a><code>| </code><code><span class="constructor">Procname</span> <span class="keyword">of</span> <a href="../../IR/Procname/index.html#type-t">IR.Procname.t</a></code></td></tr><tr id="type-target.File" class="anchored"><td class="def constructor"><a href="#type-target.File" class="anchor"></a><code>| </code><code><span class="constructor">File</span> <span class="keyword">of</span> <a href="../../IBase/SourceFile/index.html#type-t">IBase.SourceFile.t</a></code></td></tr><tr id="type-target.ProcUID" class="anchored"><td class="def constructor"><a href="#type-target.ProcUID" class="anchor"></a><code>| </code><code><span class="constructor">ProcUID</span> <span class="keyword">of</span> string</code></td><td class="doc"><p>matches primary key of <code>procedures</code> and <code>specs</code> tables; see <code>ResultsDatabase.ml</code></p></td></tr></table></dt></dl></div></body></html>
+<html xmlns="http://www.w3.org/1999/xhtml"><head><title>TaskSchedulerTypes (infer.Absint.TaskSchedulerTypes)</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> &#x00BB; <a href="../index.html">Absint</a> &#x00BB; TaskSchedulerTypes</nav><h1>Module <code>Absint.TaskSchedulerTypes</code></h1></header><dl><dt class="spec type" id="type-target"><a href="#type-target" class="anchor"></a><code><span class="keyword">type</span> target</code><code> = </code><table class="variant"><tr id="type-target.Procname" class="anchored"><td class="def constructor"><a href="#type-target.Procname" class="anchor"></a><code>| </code><code><span class="constructor">Procname</span> <span class="keyword">of</span> <a href="../../IR/Procname/index.html#type-t">IR.Procname.t</a></code></td></tr><tr id="type-target.File" class="anchored"><td class="def constructor"><a href="#type-target.File" class="anchor"></a><code>| </code><code><span class="constructor">File</span> <span class="keyword">of</span> <a href="../../IBase/SourceFile/index.html#type-t">IBase.SourceFile.t</a></code></td></tr><tr id="type-target.ProcUID" class="anchored"><td class="def constructor"><a href="#type-target.ProcUID" class="anchor"></a><code>| </code><code><span class="constructor">ProcUID</span> <span class="keyword">of</span> string</code></td><td class="doc"><p>matches primary key of <code>procedures</code> and <code>specs</code> tables; see <code>ResultsDatabase.ml</code></p></td></tr></table></dt></dl></div></body></html>

website/static/odoc/next/infer/Absint__AbstractDomain/PairNoJoin/argument-1-Domain1/index.html

@@ -0,0 +1,2 @@
+<!DOCTYPE html>
+<html xmlns="http://www.w3.org/1999/xhtml"><head><title>1-Domain1 (infer.Absint__AbstractDomain.PairNoJoin.1-Domain1)</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> &#x00BB; <a href="../../index.html">Absint__AbstractDomain</a> &#x00BB; <a href="../index.html">PairNoJoin</a> &#x00BB; 1-Domain1</nav><h1>Parameter <code>PairNoJoin.1-Domain1</code></h1></header><div><div class="spec include"><div class="doc"><details open="open"><summary><span class="def"><code><span class="keyword">include</span> <a href="../../../IStdlib/PrettyPrintable/index.html#module-type-PrintableType">IStdlib.PrettyPrintable.PrintableType</a></code></span></summary><dl><dt class="spec type" id="type-t"><a href="#type-t" class="anchor"></a><code><span class="keyword">type</span> t</code></dt></dl><dl><dt class="spec value" id="val-pp"><a href="#val-pp" class="anchor"></a><code><span class="keyword">val</span> pp : <a href="../../../IStdlib/PrettyPrintable/index.html#module-F">IStdlib.PrettyPrintable.F</a>.formatter <span>&#45;&gt;</span> <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> unit</code></dt></dl></details></div></div></div><dl><dt class="spec value" id="val-leq"><a href="#val-leq" class="anchor"></a><code><span class="keyword">val</span> leq : <span>lhs:<a href="index.html#type-t">t</a></span> <span>&#45;&gt;</span> <span>rhs:<a href="index.html#type-t">t</a></span> <span>&#45;&gt;</span> bool</code></dt><dd><p>the implication relation: <code>lhs &lt;= rhs</code> means <code>lhs |- rhs</code></p></dd></dl></div></body></html>

website/static/odoc/next/infer/Absint__AbstractDomain/PairNoJoin/argument-2-Domain2/index.html

@@ -0,0 +1,2 @@
+<!DOCTYPE html>
+<html xmlns="http://www.w3.org/1999/xhtml"><head><title>2-Domain2 (infer.Absint__AbstractDomain.PairNoJoin.2-Domain2)</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> &#x00BB; <a href="../../index.html">Absint__AbstractDomain</a> &#x00BB; <a href="../index.html">PairNoJoin</a> &#x00BB; 2-Domain2</nav><h1>Parameter <code>PairNoJoin.2-Domain2</code></h1></header><div><div class="spec include"><div class="doc"><details open="open"><summary><span class="def"><code><span class="keyword">include</span> <a href="../../../IStdlib/PrettyPrintable/index.html#module-type-PrintableType">IStdlib.PrettyPrintable.PrintableType</a></code></span></summary><dl><dt class="spec type" id="type-t"><a href="#type-t" class="anchor"></a><code><span class="keyword">type</span> t</code></dt></dl><dl><dt class="spec value" id="val-pp"><a href="#val-pp" class="anchor"></a><code><span class="keyword">val</span> pp : <a href="../../../IStdlib/PrettyPrintable/index.html#module-F">IStdlib.PrettyPrintable.F</a>.formatter <span>&#45;&gt;</span> <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> unit</code></dt></dl></details></div></div></div><dl><dt class="spec value" id="val-leq"><a href="#val-leq" class="anchor"></a><code><span class="keyword">val</span> leq : <span>lhs:<a href="index.html#type-t">t</a></span> <span>&#45;&gt;</span> <span>rhs:<a href="index.html#type-t">t</a></span> <span>&#45;&gt;</span> bool</code></dt><dd><p>the implication relation: <code>lhs &lt;= rhs</code> means <code>lhs |- rhs</code></p></dd></dl></div></body></html>

website/static/odoc/next/infer/Absint__AbstractDomain/PairNoJoin/index.html

@@ -0,0 +1,2 @@
+<!DOCTYPE html>
+<html xmlns="http://www.w3.org/1999/xhtml"><head><title>PairNoJoin (infer.Absint__AbstractDomain.PairNoJoin)</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> &#x00BB; <a href="../index.html">Absint__AbstractDomain</a> &#x00BB; PairNoJoin</nav><h1>Module <code>Absint__AbstractDomain.PairNoJoin</code></h1></header><h3 class="heading">Parameters</h3><ul><li><code><a href="argument-1-Domain1/index.html">Domain1</a> : <a href="../index.html#module-type-NoJoin">NoJoin</a></code></li><li><code><a href="argument-2-Domain2/index.html">Domain2</a> : <a href="../index.html#module-type-NoJoin">NoJoin</a></code></li></ul><h3 class="heading">Signature</h3><div><div class="spec include"><div class="doc"><details open="open"><summary><span class="def"><code><span class="keyword">include</span> <a href="../../IStdlib/PrettyPrintable/index.html#module-type-PrintableType">IStdlib.PrettyPrintable.PrintableType</a></code></span></summary><dl><dt class="spec type" id="type-t"><a href="#type-t" class="anchor"></a><code><span class="keyword">type</span> t</code></dt></dl><dl><dt class="spec value" id="val-pp"><a href="#val-pp" class="anchor"></a><code><span class="keyword">val</span> pp : <a href="../../IStdlib/PrettyPrintable/index.html#module-F">IStdlib.PrettyPrintable.F</a>.formatter <span>&#45;&gt;</span> <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> unit</code></dt></dl></details></div></div></div><dl><dt class="spec value" id="val-leq"><a href="#val-leq" class="anchor"></a><code><span class="keyword">val</span> leq : <span>lhs:<a href="index.html#type-t">t</a></span> <span>&#45;&gt;</span> <span>rhs:<a href="index.html#type-t">t</a></span> <span>&#45;&gt;</span> bool</code></dt><dd><p>the implication relation: <code>lhs &lt;= rhs</code> means <code>lhs |- rhs</code></p></dd></dl></div></body></html>

website/static/odoc/next/infer/Absint__TaskSchedulerTypes/index.html

@@ -1,2 +1,2 @@
 <!DOCTYPE html>
-<html xmlns="http://www.w3.org/1999/xhtml"><head><title>Absint__TaskSchedulerTypes (infer.Absint__TaskSchedulerTypes)</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> &#x00BB; Absint__TaskSchedulerTypes</nav><h1>Module <code>Absint__TaskSchedulerTypes</code></h1></header><dl><dt class="spec exception" id="exception-ProcnameAlreadyLocked"><a href="#exception-ProcnameAlreadyLocked" class="anchor"></a><code><span class="keyword">exception</span> </code><code><span class="exception">ProcnameAlreadyLocked</span> <span class="keyword">of</span> </code><code>{</code><table class="record"><tr id=".dependency_filename" class="anchored"><td class="def field"><a href="#.dependency_filename" class="anchor"></a><code>dependency_filename : string;</code></td></tr></table><code>}</code></dt><dd><p>for the Restart scheduler: raise when a worker tries to analyze a procedure already being analyzed by another process</p></dd></dl><dl><dt class="spec type" id="type-target"><a href="#type-target" class="anchor"></a><code><span class="keyword">type</span> target</code><code> = </code><table class="variant"><tr id="type-target.Procname" class="anchored"><td class="def constructor"><a href="#type-target.Procname" class="anchor"></a><code>| </code><code><span class="constructor">Procname</span> <span class="keyword">of</span> <a href="../IR/Procname/index.html#type-t">IR.Procname.t</a></code></td></tr><tr id="type-target.File" class="anchored"><td class="def constructor"><a href="#type-target.File" class="anchor"></a><code>| </code><code><span class="constructor">File</span> <span class="keyword">of</span> <a href="../IBase/SourceFile/index.html#type-t">IBase.SourceFile.t</a></code></td></tr><tr id="type-target.ProcUID" class="anchored"><td class="def constructor"><a href="#type-target.ProcUID" class="anchor"></a><code>| </code><code><span class="constructor">ProcUID</span> <span class="keyword">of</span> string</code></td><td class="doc"><p>matches primary key of <code>procedures</code> and <code>specs</code> tables; see <code>ResultsDatabase.ml</code></p></td></tr></table></dt></dl></div></body></html>
+<html xmlns="http://www.w3.org/1999/xhtml"><head><title>Absint__TaskSchedulerTypes (infer.Absint__TaskSchedulerTypes)</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> &#x00BB; Absint__TaskSchedulerTypes</nav><h1>Module <code>Absint__TaskSchedulerTypes</code></h1></header><dl><dt class="spec type" id="type-target"><a href="#type-target" class="anchor"></a><code><span class="keyword">type</span> target</code><code> = </code><table class="variant"><tr id="type-target.Procname" class="anchored"><td class="def constructor"><a href="#type-target.Procname" class="anchor"></a><code>| </code><code><span class="constructor">Procname</span> <span class="keyword">of</span> <a href="../IR/Procname/index.html#type-t">IR.Procname.t</a></code></td></tr><tr id="type-target.File" class="anchored"><td class="def constructor"><a href="#type-target.File" class="anchor"></a><code>| </code><code><span class="constructor">File</span> <span class="keyword">of</span> <a href="../IBase/SourceFile/index.html#type-t">IBase.SourceFile.t</a></code></td></tr><tr id="type-target.ProcUID" class="anchored"><td class="def constructor"><a href="#type-target.ProcUID" class="anchor"></a><code>| </code><code><span class="constructor">ProcUID</span> <span class="keyword">of</span> string</code></td><td class="doc"><p>matches primary key of <code>procedures</code> and <code>specs</code> tables; see <code>ResultsDatabase.ml</code></p></td></tr></table></dt></dl></div></body></html>

website/static/odoc/next/infer/ErlangFrontend/ErlangTranslator/index.html

@@ -1,2 +1,2 @@
 <!DOCTYPE html>
-<html xmlns="http://www.w3.org/1999/xhtml"><head><title>ErlangTranslator (infer.ErlangFrontend.ErlangTranslator)</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> &#x00BB; <a href="../index.html">ErlangFrontend</a> &#x00BB; ErlangTranslator</nav><h1>Module <code>ErlangFrontend.ErlangTranslator</code></h1></header><dl><dt class="spec value" id="val-to_source_and_cfg"><a href="#val-to_source_and_cfg" class="anchor"></a><code><span class="keyword">val</span> to_source_and_cfg : <a href="../ErlangAst/index.html#type-module_">ErlangAst.module_</a> <span>&#45;&gt;</span> <a href="../../IBase/SourceFile/index.html#type-t">IBase.SourceFile.t</a> * <a href="../../IR/Cfg/index.html#type-t">IR.Cfg.t</a></code></dt></dl></div></body></html>
+<html xmlns="http://www.w3.org/1999/xhtml"><head><title>ErlangTranslator (infer.ErlangFrontend.ErlangTranslator)</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> &#x00BB; <a href="../index.html">ErlangFrontend</a> &#x00BB; ErlangTranslator</nav><h1>Module <code>ErlangFrontend.ErlangTranslator</code></h1></header><dl><dt class="spec value" id="val-translate_module"><a href="#val-translate_module" class="anchor"></a><code><span class="keyword">val</span> translate_module : <a href="../ErlangAst/index.html#type-module_">ErlangAst.module_</a> <span>&#45;&gt;</span> unit</code></dt></dl></div></body></html>

website/static/odoc/next/infer/ErlangFrontend__ErlangTranslator/index.html

@@ -1,2 +1,2 @@
 <!DOCTYPE html>
-<html xmlns="http://www.w3.org/1999/xhtml"><head><title>ErlangFrontend__ErlangTranslator (infer.ErlangFrontend__ErlangTranslator)</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> &#x00BB; ErlangFrontend__ErlangTranslator</nav><h1>Module <code>ErlangFrontend__ErlangTranslator</code></h1></header><dl><dt class="spec value" id="val-to_source_and_cfg"><a href="#val-to_source_and_cfg" class="anchor"></a><code><span class="keyword">val</span> to_source_and_cfg : <a href="../ErlangFrontend/ErlangAst/index.html#type-module_">ErlangFrontend.ErlangAst.module_</a> <span>&#45;&gt;</span> <a href="../IBase/SourceFile/index.html#type-t">IBase.SourceFile.t</a> * <a href="../IR/Cfg/index.html#type-t">IR.Cfg.t</a></code></dt></dl></div></body></html>
+<html xmlns="http://www.w3.org/1999/xhtml"><head><title>ErlangFrontend__ErlangTranslator (infer.ErlangFrontend__ErlangTranslator)</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> &#x00BB; ErlangFrontend__ErlangTranslator</nav><h1>Module <code>ErlangFrontend__ErlangTranslator</code></h1></header><dl><dt class="spec value" id="val-translate_module"><a href="#val-translate_module" class="anchor"></a><code><span class="keyword">val</span> translate_module : <a href="../ErlangFrontend/ErlangAst/index.html#type-module_">ErlangFrontend.ErlangAst.module_</a> <span>&#45;&gt;</span> unit</code></dt></dl></div></body></html>

website/static/odoc/next/infer/IBase/RestartSchedulerException/index.html

@@ -0,0 +1,2 @@
+<!DOCTYPE html>
+<html xmlns="http://www.w3.org/1999/xhtml"><head><title>RestartSchedulerException (infer.IBase.RestartSchedulerException)</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> &#x00BB; <a href="../index.html">IBase</a> &#x00BB; RestartSchedulerException</nav><h1>Module <code>IBase.RestartSchedulerException</code></h1></header><dl><dt class="spec exception" id="exception-ProcnameAlreadyLocked"><a href="#exception-ProcnameAlreadyLocked" class="anchor"></a><code><span class="keyword">exception</span> </code><code><span class="exception">ProcnameAlreadyLocked</span> <span class="keyword">of</span> </code><code>{</code><table class="record"><tr id=".dependency_filename" class="anchored"><td class="def field"><a href="#.dependency_filename" class="anchor"></a><code>dependency_filename : string;</code></td></tr></table><code>}</code></dt><dd><p>for the Restart scheduler: raise when a worker tries to analyze a procedure already being analyzed by another process</p></dd></dl><dl><dt class="spec value" id="val-is_not_restart_exception"><a href="#val-is_not_restart_exception" class="anchor"></a><code><span class="keyword">val</span> is_not_restart_exception : exn <span>&#45;&gt;</span> bool</code></dt><dd><p>check if the exception passed is the one defined above</p></dd></dl></div></body></html>

website/static/odoc/next/infer/IBase__RestartSchedulerException/index.html

@@ -0,0 +1,2 @@
+<!DOCTYPE html>
+<html xmlns="http://www.w3.org/1999/xhtml"><head><title>IBase__RestartSchedulerException (infer.IBase__RestartSchedulerException)</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> &#x00BB; IBase__RestartSchedulerException</nav><h1>Module <code>IBase__RestartSchedulerException</code></h1></header><dl><dt class="spec exception" id="exception-ProcnameAlreadyLocked"><a href="#exception-ProcnameAlreadyLocked" class="anchor"></a><code><span class="keyword">exception</span> </code><code><span class="exception">ProcnameAlreadyLocked</span> <span class="keyword">of</span> </code><code>{</code><table class="record"><tr id=".dependency_filename" class="anchored"><td class="def field"><a href="#.dependency_filename" class="anchor"></a><code>dependency_filename : string;</code></td></tr></table><code>}</code></dt><dd><p>for the Restart scheduler: raise when a worker tries to analyze a procedure already being analyzed by another process</p></dd></dl><dl><dt class="spec value" id="val-is_not_restart_exception"><a href="#val-is_not_restart_exception" class="anchor"></a><code><span class="keyword">val</span> is_not_restart_exception : exn <span>&#45;&gt;</span> bool</code></dt><dd><p>check if the exception passed is the one defined above</p></dd></dl></div></body></html>

website/static/odoc/next/infer/IR/ErlangTypeName/index.html

@@ -0,0 +1,2 @@
+<!DOCTYPE html>
+<html xmlns="http://www.w3.org/1999/xhtml"><head><title>ErlangTypeName (infer.IR.ErlangTypeName)</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> &#x00BB; <a href="../index.html">IR</a> &#x00BB; ErlangTypeName</nav><h1>Module <code>IR.ErlangTypeName</code></h1></header><dl><dt class="spec type" id="type-t"><a href="#type-t" class="anchor"></a><code><span class="keyword">type</span> t</code><code> = </code><table class="variant"><tr id="type-t.Any" class="anchored"><td class="def constructor"><a href="#type-t.Any" class="anchor"></a><code>| </code><code><span class="constructor">Any</span></code></td></tr></table></dt></dl><div><div class="spec include"><div class="doc"><dl><dt class="spec value" id="val-compare"><a href="#val-compare" class="anchor"></a><code><span class="keyword">val</span> compare : <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> int</code></dt><dt class="spec value" id="val-yojson_of_t"><a href="#val-yojson_of_t" class="anchor"></a><code><span class="keyword">val</span> yojson_of_t : <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> Ppx_yojson_conv_lib.Yojson.Safe.t</code></dt></dl></div></div></div><dl><dt class="spec value" id="val-pp"><a href="#val-pp" class="anchor"></a><code><span class="keyword">val</span> pp : Stdlib.Format.formatter <span>&#45;&gt;</span> <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> unit</code></dt><dt class="spec value" id="val-to_string"><a href="#val-to_string" class="anchor"></a><code><span class="keyword">val</span> to_string : <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> string</code></dt></dl></div></body></html>

website/static/odoc/next/infer/IR__ErlangTypeName/index.html

@@ -0,0 +1,2 @@
+<!DOCTYPE html>
+<html xmlns="http://www.w3.org/1999/xhtml"><head><title>IR__ErlangTypeName (infer.IR__ErlangTypeName)</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> &#x00BB; IR__ErlangTypeName</nav><h1>Module <code>IR__ErlangTypeName</code></h1></header><dl><dt class="spec type" id="type-t"><a href="#type-t" class="anchor"></a><code><span class="keyword">type</span> t</code><code> = </code><table class="variant"><tr id="type-t.Any" class="anchored"><td class="def constructor"><a href="#type-t.Any" class="anchor"></a><code>| </code><code><span class="constructor">Any</span></code></td></tr></table></dt></dl><div><div class="spec include"><div class="doc"><dl><dt class="spec value" id="val-compare"><a href="#val-compare" class="anchor"></a><code><span class="keyword">val</span> compare : <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> int</code></dt><dt class="spec value" id="val-yojson_of_t"><a href="#val-yojson_of_t" class="anchor"></a><code><span class="keyword">val</span> yojson_of_t : <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> Ppx_yojson_conv_lib.Yojson.Safe.t</code></dt></dl></div></div></div><dl><dt class="spec value" id="val-pp"><a href="#val-pp" class="anchor"></a><code><span class="keyword">val</span> pp : Stdlib.Format.formatter <span>&#45;&gt;</span> <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> unit</code></dt><dt class="spec value" id="val-to_string"><a href="#val-to_string" class="anchor"></a><code><span class="keyword">val</span> to_string : <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> string</code></dt></dl></div></body></html>

website/static/odoc/next/infer/OpenSource/FbThreadSafety/index.html

@@ -1,2 +1,2 @@
 <!DOCTYPE html>
-<html xmlns="http://www.w3.org/1999/xhtml"><head><title>FbThreadSafety (infer.OpenSource.FbThreadSafety)</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> &#x00BB; <a href="../index.html">OpenSource</a> &#x00BB; FbThreadSafety</nav><h1>Module <code>OpenSource.FbThreadSafety</code></h1></header><dl><dt class="spec value" id="val-is_custom_init"><a href="#val-is_custom_init" class="anchor"></a><code><span class="keyword">val</span> is_custom_init : <span class="type-var">'tenv_t</span> <span>&#45;&gt;</span> <span class="type-var">'procname_t</span> <span>&#45;&gt;</span> bool</code></dt><dt class="spec value" id="val-is_logging_method"><a href="#val-is_logging_method" class="anchor"></a><code><span class="keyword">val</span> is_logging_method : <span class="type-var">'procname_t</span> <span>&#45;&gt;</span> bool</code></dt><dt class="spec value" id="val-get_fbthreadsafe_class_annot"><a href="#val-get_fbthreadsafe_class_annot" class="anchor"></a><code><span class="keyword">val</span> get_fbthreadsafe_class_annot : <span class="type-var">'procname_t</span> <span>&#45;&gt;</span> <span class="type-var">'tenv_t</span> <span>&#45;&gt;</span> <span><span>(string * string)</span> option</span></code></dt><dt class="spec value" id="val-message_fbthreadsafe_class"><a href="#val-message_fbthreadsafe_class" class="anchor"></a><code><span class="keyword">val</span> message_fbthreadsafe_class : string <span>&#45;&gt;</span> string <span>&#45;&gt;</span> string</code></dt></dl></div></body></html>
+<html xmlns="http://www.w3.org/1999/xhtml"><head><title>FbThreadSafety (infer.OpenSource.FbThreadSafety)</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> &#x00BB; <a href="../index.html">OpenSource</a> &#x00BB; FbThreadSafety</nav><h1>Module <code>OpenSource.FbThreadSafety</code></h1></header><dl><dt class="spec value" id="val-is_custom_init"><a href="#val-is_custom_init" class="anchor"></a><code><span class="keyword">val</span> is_custom_init : <span class="type-var">'tenv_t</span> <span>&#45;&gt;</span> <span class="type-var">'procname_t</span> <span>&#45;&gt;</span> bool</code></dt><dt class="spec value" id="val-is_logging_method"><a href="#val-is_logging_method" class="anchor"></a><code><span class="keyword">val</span> is_logging_method : <span class="type-var">'procname_t</span> <span>&#45;&gt;</span> bool</code></dt></dl></div></body></html>

website/static/odoc/next/infer/OpenSource__FbThreadSafety/index.html

@@ -1,2 +1,2 @@
 <!DOCTYPE html>
-<html xmlns="http://www.w3.org/1999/xhtml"><head><title>OpenSource__FbThreadSafety (infer.OpenSource__FbThreadSafety)</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> &#x00BB; OpenSource__FbThreadSafety</nav><h1>Module <code>OpenSource__FbThreadSafety</code></h1></header><dl><dt class="spec value" id="val-is_custom_init"><a href="#val-is_custom_init" class="anchor"></a><code><span class="keyword">val</span> is_custom_init : <span class="type-var">'tenv_t</span> <span>&#45;&gt;</span> <span class="type-var">'procname_t</span> <span>&#45;&gt;</span> bool</code></dt><dt class="spec value" id="val-is_logging_method"><a href="#val-is_logging_method" class="anchor"></a><code><span class="keyword">val</span> is_logging_method : <span class="type-var">'procname_t</span> <span>&#45;&gt;</span> bool</code></dt><dt class="spec value" id="val-get_fbthreadsafe_class_annot"><a href="#val-get_fbthreadsafe_class_annot" class="anchor"></a><code><span class="keyword">val</span> get_fbthreadsafe_class_annot : <span class="type-var">'procname_t</span> <span>&#45;&gt;</span> <span class="type-var">'tenv_t</span> <span>&#45;&gt;</span> <span><span>(string * string)</span> option</span></code></dt><dt class="spec value" id="val-message_fbthreadsafe_class"><a href="#val-message_fbthreadsafe_class" class="anchor"></a><code><span class="keyword">val</span> message_fbthreadsafe_class : string <span>&#45;&gt;</span> string <span>&#45;&gt;</span> string</code></dt></dl></div></body></html>
+<html xmlns="http://www.w3.org/1999/xhtml"><head><title>OpenSource__FbThreadSafety (infer.OpenSource__FbThreadSafety)</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> &#x00BB; OpenSource__FbThreadSafety</nav><h1>Module <code>OpenSource__FbThreadSafety</code></h1></header><dl><dt class="spec value" id="val-is_custom_init"><a href="#val-is_custom_init" class="anchor"></a><code><span class="keyword">val</span> is_custom_init : <span class="type-var">'tenv_t</span> <span>&#45;&gt;</span> <span class="type-var">'procname_t</span> <span>&#45;&gt;</span> bool</code></dt><dt class="spec value" id="val-is_logging_method"><a href="#val-is_logging_method" class="anchor"></a><code><span class="keyword">val</span> is_logging_method : <span class="type-var">'procname_t</span> <span>&#45;&gt;</span> bool</code></dt></dl></div></body></html>

website/static/odoc/next/infer/Pulselib/PulseAbductiveDomain/Stack/index.html

@@ -1,2 +1,2 @@
 <!DOCTYPE html>
-<html xmlns="http://www.w3.org/1999/xhtml"><head><title>Stack (infer.Pulselib.PulseAbductiveDomain.Stack)</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> &#x00BB; <a href="../../index.html">Pulselib</a> &#x00BB; <a href="../index.html">PulseAbductiveDomain</a> &#x00BB; Stack</nav><h1>Module <code>PulseAbductiveDomain.Stack</code></h1><p>stack operations like <a href="../BaseStack/index.html"><code>BaseStack</code></a> but that also take care of propagating facts to the precondition</p></header><dl><dt class="spec value" id="val-add"><a href="#val-add" class="anchor"></a><code><span class="keyword">val</span> add : <a href="../../../IR/Var/index.html#type-t">IR.Var.t</a> <span>&#45;&gt;</span> <a href="../../PulseBaseStack/index.html#type-value">BaseStack.value</a> <span>&#45;&gt;</span> <a href="../index.html#type-t">t</a> <span>&#45;&gt;</span> <a href="../index.html#type-t">t</a></code></dt><dt class="spec value" id="val-remove_vars"><a href="#val-remove_vars" class="anchor"></a><code><span class="keyword">val</span> remove_vars : <span><a href="../../../IR/Var/index.html#type-t">IR.Var.t</a> list</span> <span>&#45;&gt;</span> <a href="../index.html#type-t">t</a> <span>&#45;&gt;</span> <a href="../index.html#type-t">t</a></code></dt><dt class="spec value" id="val-fold"><a href="#val-fold" class="anchor"></a><code><span class="keyword">val</span> fold : <span>(<a href="../../../IR/Var/index.html#type-t">IR.Var.t</a> <span>&#45;&gt;</span> <a href="../../PulseBaseStack/index.html#type-value">BaseStack.value</a> <span>&#45;&gt;</span> <span class="type-var">'a</span> <span>&#45;&gt;</span> <span class="type-var">'a</span>)</span> <span>&#45;&gt;</span> <a href="../index.html#type-t">t</a> <span>&#45;&gt;</span> <span class="type-var">'a</span> <span>&#45;&gt;</span> <span class="type-var">'a</span></code></dt><dt class="spec value" id="val-find_opt"><a href="#val-find_opt" class="anchor"></a><code><span class="keyword">val</span> find_opt : <a href="../../../IR/Var/index.html#type-t">IR.Var.t</a> <span>&#45;&gt;</span> <a href="../index.html#type-t">t</a> <span>&#45;&gt;</span> <span><a href="../../PulseBaseStack/index.html#type-value">BaseStack.value</a> option</span></code></dt><dt class="spec value" id="val-eval"><a href="#val-eval" class="anchor"></a><code><span class="keyword">val</span> eval : <a href="../../../IBase/Location/index.html#type-t">IBase.Location.t</a> <span>&#45;&gt;</span> <a href="../../PulseValueHistory/index.html#type-t">PulseBasicInterface.ValueHistory.t</a> <span>&#45;&gt;</span> <a href="../../../IR/Var/index.html#type-t">IR.Var.t</a> <span>&#45;&gt;</span> <a href="../index.html#type-t">t</a> <span>&#45;&gt;</span> <a href="../index.html#type-t">t</a> * <span>(<a href="../../PulseAbstractValue/index.html#type-t">PulseBasicInterface.AbstractValue.t</a> * <a href="../../PulseValueHistory/index.html#type-t">PulseBasicInterface.ValueHistory.t</a>)</span></code></dt><dd><p>return the value of the variable in the stack or create a fresh one if needed</p></dd></dl><dl><dt class="spec value" id="val-mem"><a href="#val-mem" class="anchor"></a><code><span class="keyword">val</span> mem : <a href="../../../IR/Var/index.html#type-t">IR.Var.t</a> <span>&#45;&gt;</span> <a href="../index.html#type-t">t</a> <span>&#45;&gt;</span> bool</code></dt><dt class="spec value" id="val-exists"><a href="#val-exists" class="anchor"></a><code><span class="keyword">val</span> exists : <span>(<a href="../../../IR/Var/index.html#type-t">IR.Var.t</a> <span>&#45;&gt;</span> <a href="../../PulseBaseStack/index.html#type-value">BaseStack.value</a> <span>&#45;&gt;</span> bool)</span> <span>&#45;&gt;</span> <a href="../index.html#type-t">t</a> <span>&#45;&gt;</span> bool</code></dt><dt class="spec value" id="val-keys"><a href="#val-keys" class="anchor"></a><code><span class="keyword">val</span> keys : <a href="../index.html#type-t">t</a> <span>&#45;&gt;</span> <span><a href="../../../IR/Var/index.html#type-t">IR.Var.t</a> list</span></code></dt></dl></div></body></html>
+<html xmlns="http://www.w3.org/1999/xhtml"><head><title>Stack (infer.Pulselib.PulseAbductiveDomain.Stack)</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> &#x00BB; <a href="../../index.html">Pulselib</a> &#x00BB; <a href="../index.html">PulseAbductiveDomain</a> &#x00BB; Stack</nav><h1>Module <code>PulseAbductiveDomain.Stack</code></h1><p>stack operations like <a href="../BaseStack/index.html"><code>BaseStack</code></a> but that also take care of propagating facts to the precondition</p></header><dl><dt class="spec value" id="val-add"><a href="#val-add" class="anchor"></a><code><span class="keyword">val</span> add : <a href="../../../IR/Var/index.html#type-t">IR.Var.t</a> <span>&#45;&gt;</span> <a href="../../PulseBaseStack/index.html#type-value">BaseStack.value</a> <span>&#45;&gt;</span> <a href="../index.html#type-t">t</a> <span>&#45;&gt;</span> <a href="../index.html#type-t">t</a></code></dt><dt class="spec value" id="val-remove_vars"><a href="#val-remove_vars" class="anchor"></a><code><span class="keyword">val</span> remove_vars : <span><a href="../../../IR/Var/index.html#type-t">IR.Var.t</a> list</span> <span>&#45;&gt;</span> <a href="../index.html#type-t">t</a> <span>&#45;&gt;</span> <a href="../index.html#type-t">t</a></code></dt><dt class="spec value" id="val-fold"><a href="#val-fold" class="anchor"></a><code><span class="keyword">val</span> fold : <span>(<a href="../../../IR/Var/index.html#type-t">IR.Var.t</a> <span>&#45;&gt;</span> <a href="../../PulseBaseStack/index.html#type-value">BaseStack.value</a> <span>&#45;&gt;</span> <span class="type-var">'a</span> <span>&#45;&gt;</span> <span class="type-var">'a</span>)</span> <span>&#45;&gt;</span> <a href="../index.html#type-t">t</a> <span>&#45;&gt;</span> <span class="type-var">'a</span> <span>&#45;&gt;</span> <span class="type-var">'a</span></code></dt><dt class="spec value" id="val-find_opt"><a href="#val-find_opt" class="anchor"></a><code><span class="keyword">val</span> find_opt : <a href="../../../IR/Var/index.html#type-t">IR.Var.t</a> <span>&#45;&gt;</span> <a href="../index.html#type-t">t</a> <span>&#45;&gt;</span> <span><a href="../../PulseBaseStack/index.html#type-value">BaseStack.value</a> option</span></code></dt><dt class="spec value" id="val-eval"><a href="#val-eval" class="anchor"></a><code><span class="keyword">val</span> eval : <a href="../../PulsePathContext/index.html#type-t">PulseBasicInterface.PathContext.t</a> <span>&#45;&gt;</span> <a href="../../../IBase/Location/index.html#type-t">IBase.Location.t</a> <span>&#45;&gt;</span> <a href="../../PulseValueHistory/index.html#type-t">PulseBasicInterface.ValueHistory.t</a> <span>&#45;&gt;</span> <a href="../../../IR/Var/index.html#type-t">IR.Var.t</a> <span>&#45;&gt;</span> <a href="../index.html#type-t">t</a> <span>&#45;&gt;</span> <a href="../index.html#type-t">t</a> * <span>(<a href="../../PulseAbstractValue/index.html#type-t">PulseBasicInterface.AbstractValue.t</a> * <a href="../../PulseValueHistory/index.html#type-t">PulseBasicInterface.ValueHistory.t</a>)</span></code></dt><dd><p>return the value of the variable in the stack or create a fresh one if needed</p></dd></dl><dl><dt class="spec value" id="val-mem"><a href="#val-mem" class="anchor"></a><code><span class="keyword">val</span> mem : <a href="../../../IR/Var/index.html#type-t">IR.Var.t</a> <span>&#45;&gt;</span> <a href="../index.html#type-t">t</a> <span>&#45;&gt;</span> bool</code></dt><dt class="spec value" id="val-exists"><a href="#val-exists" class="anchor"></a><code><span class="keyword">val</span> exists : <span>(<a href="../../../IR/Var/index.html#type-t">IR.Var.t</a> <span>&#45;&gt;</span> <a href="../../PulseBaseStack/index.html#type-value">BaseStack.value</a> <span>&#45;&gt;</span> bool)</span> <span>&#45;&gt;</span> <a href="../index.html#type-t">t</a> <span>&#45;&gt;</span> bool</code></dt><dt class="spec value" id="val-keys"><a href="#val-keys" class="anchor"></a><code><span class="keyword">val</span> keys : <a href="../index.html#type-t">t</a> <span>&#45;&gt;</span> <span><a href="../../../IR/Var/index.html#type-t">IR.Var.t</a> list</span></code></dt></dl></div></body></html>

website/static/odoc/next/infer/Pulselib/PulseCallOperations/index.html

@@ -1,2 +1,2 @@
 <!DOCTYPE html>
-<html xmlns="http://www.w3.org/1999/xhtml"><head><title>PulseCallOperations (infer.Pulselib.PulseCallOperations)</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> &#x00BB; <a href="../index.html">Pulselib</a> &#x00BB; PulseCallOperations</nav><h1>Module <code>Pulselib.PulseCallOperations</code></h1></header><dl><dt class="spec type" id="type-t"><a href="#type-t" class="anchor"></a><code><span class="keyword">type</span> t</code><code> = <a href="../PulseAbductiveDomain/index.html#type-t">PulseDomainInterface.AbductiveDomain.t</a></code></dt></dl><dl><dt class="spec value" id="val-call"><a href="#val-call" class="anchor"></a><code><span class="keyword">val</span> call : <a href="../../IR/Tenv/index.html#type-t">IR.Tenv.t</a> <span>&#45;&gt;</span> <span>caller_proc_desc:<a href="../../IR/Procdesc/index.html#type-t">IR.Procdesc.t</a></span> <span>&#45;&gt;</span> <span>callee_data:<span><span>(<a href="../../IR/Procdesc/index.html#type-t">IR.Procdesc.t</a> * <a href="../PulseSummary/index.html#type-t">PulseSummary.t</a>)</span> option</span></span> <span>&#45;&gt;</span> <a href="../../IBase/Location/index.html#type-t">IBase.Location.t</a> <span>&#45;&gt;</span> <a href="../../IR/Procname/index.html#type-t">IR.Procname.t</a> <span>&#45;&gt;</span> <span>ret:<span>(<a href="../../IR/Ident/index.html#type-t">IR.Ident.t</a> * <a href="../../IR/Typ/index.html#type-t">IR.Typ.t</a>)</span></span> <span>&#45;&gt;</span> <span>actuals:<span><span>(<span>(<a href="../PulseAbstractValue/index.html#type-t">PulseBasicInterface.AbstractValue.t</a> * <a href="../PulseValueHistory/index.html#type-t">PulseBasicInterface.ValueHistory.t</a>)</span> * <a href="../../IR/Typ/index.html#type-t">IR.Typ.t</a>)</span> list</span></span> <span>&#45;&gt;</span> <span>formals_opt:<span><span><span>(<a href="../../IR/Pvar/index.html#type-t">IR.Pvar.t</a> * <a href="../../IR/Typ/index.html#type-t">IR.Typ.t</a>)</span> list</span> option</span></span> <span>&#45;&gt;</span> <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> <span><span><a href="../PulseExecutionDomain/index.html#type-t">PulseDomainInterface.ExecutionDomain.t</a> <a href="../PulseAccessResult/index.html#type-t">PulseDomainInterface.AccessResult.t</a></span> list</span></code></dt><dd><p>perform an interprocedural call: apply the summary for the call proc name passed as argument if it exists</p></dd></dl><dl><dt class="spec value" id="val-unknown_call"><a href="#val-unknown_call" class="anchor"></a><code><span class="keyword">val</span> unknown_call : <a href="../../IR/Tenv/index.html#type-t">IR.Tenv.t</a> <span>&#45;&gt;</span> <a href="../../IBase/Location/index.html#type-t">IBase.Location.t</a> <span>&#45;&gt;</span> <a href="../PulseCallEvent/index.html#type-t">PulseBasicInterface.CallEvent.t</a> <span>&#45;&gt;</span> <span>ret:<span>(<a href="../../IR/Ident/index.html#type-t">IR.Ident.t</a> * <a href="../../IR/Typ/index.html#type-t">IR.Typ.t</a>)</span></span> <span>&#45;&gt;</span> <span>actuals:<span><span>(<span>(<a href="../PulseAbstractValue/index.html#type-t">PulseBasicInterface.AbstractValue.t</a> * <a href="../PulseValueHistory/index.html#type-t">PulseBasicInterface.ValueHistory.t</a>)</span> * <a href="../../IR/Typ/index.html#type-t">IR.Typ.t</a>)</span> list</span></span> <span>&#45;&gt;</span> <span>formals_opt:<span><span><span>(<a href="../../IR/Pvar/index.html#type-t">IR.Pvar.t</a> * <a href="../../IR/Typ/index.html#type-t">IR.Typ.t</a>)</span> list</span> option</span></span> <span>&#45;&gt;</span> <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> <a href="index.html#type-t">t</a></code></dt><dd><p>performs a call to a function with no summary by optimistically havoc'ing the by-ref actuals and the return value as appropriate</p></dd></dl><dl><dt class="spec value" id="val-conservatively_initialize_args"><a href="#val-conservatively_initialize_args" class="anchor"></a><code><span class="keyword">val</span> conservatively_initialize_args : <span><a href="../PulseAbstractValue/index.html#type-t">PulseBasicInterface.AbstractValue.t</a> list</span> <span>&#45;&gt;</span> <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> <a href="index.html#type-t">t</a></code></dt></dl></div></body></html>
+<html xmlns="http://www.w3.org/1999/xhtml"><head><title>PulseCallOperations (infer.Pulselib.PulseCallOperations)</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> &#x00BB; <a href="../index.html">Pulselib</a> &#x00BB; PulseCallOperations</nav><h1>Module <code>Pulselib.PulseCallOperations</code></h1></header><dl><dt class="spec type" id="type-t"><a href="#type-t" class="anchor"></a><code><span class="keyword">type</span> t</code><code> = <a href="../PulseAbductiveDomain/index.html#type-t">PulseDomainInterface.AbductiveDomain.t</a></code></dt></dl><dl><dt class="spec value" id="val-call"><a href="#val-call" class="anchor"></a><code><span class="keyword">val</span> call : <a href="../../IR/Tenv/index.html#type-t">IR.Tenv.t</a> <span>&#45;&gt;</span> <a href="../PulsePathContext/index.html#type-t">PulseBasicInterface.PathContext.t</a> <span>&#45;&gt;</span> <span>caller_proc_desc:<a href="../../IR/Procdesc/index.html#type-t">IR.Procdesc.t</a></span> <span>&#45;&gt;</span> <span>callee_data:<span><span>(<a href="../../IR/Procdesc/index.html#type-t">IR.Procdesc.t</a> * <a href="../PulseSummary/index.html#type-t">PulseSummary.t</a>)</span> option</span></span> <span>&#45;&gt;</span> <a href="../../IBase/Location/index.html#type-t">IBase.Location.t</a> <span>&#45;&gt;</span> <a href="../../IR/Procname/index.html#type-t">IR.Procname.t</a> <span>&#45;&gt;</span> <span>ret:<span>(<a href="../../IR/Ident/index.html#type-t">IR.Ident.t</a> * <a href="../../IR/Typ/index.html#type-t">IR.Typ.t</a>)</span></span> <span>&#45;&gt;</span> <span>actuals:<span><span>(<span>(<a href="../PulseAbstractValue/index.html#type-t">PulseBasicInterface.AbstractValue.t</a> * <a href="../PulseValueHistory/index.html#type-t">PulseBasicInterface.ValueHistory.t</a>)</span> * <a href="../../IR/Typ/index.html#type-t">IR.Typ.t</a>)</span> list</span></span> <span>&#45;&gt;</span> <span>formals_opt:<span><span><span>(<a href="../../IR/Pvar/index.html#type-t">IR.Pvar.t</a> * <a href="../../IR/Typ/index.html#type-t">IR.Typ.t</a>)</span> list</span> option</span></span> <span>&#45;&gt;</span> <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> <span><span><a href="../PulseExecutionDomain/index.html#type-t">PulseDomainInterface.ExecutionDomain.t</a> <a href="../PulseAccessResult/index.html#type-t">PulseDomainInterface.AccessResult.t</a></span> list</span></code></dt><dd><p>perform an interprocedural call: apply the summary for the call proc name passed as argument if it exists</p></dd></dl><dl><dt class="spec value" id="val-unknown_call"><a href="#val-unknown_call" class="anchor"></a><code><span class="keyword">val</span> unknown_call : <a href="../../IR/Tenv/index.html#type-t">IR.Tenv.t</a> <span>&#45;&gt;</span> <a href="../PulsePathContext/index.html#type-t">PulseBasicInterface.PathContext.t</a> <span>&#45;&gt;</span> <a href="../../IBase/Location/index.html#type-t">IBase.Location.t</a> <span>&#45;&gt;</span> <a href="../PulseCallEvent/index.html#type-t">PulseBasicInterface.CallEvent.t</a> <span>&#45;&gt;</span> <span>ret:<span>(<a href="../../IR/Ident/index.html#type-t">IR.Ident.t</a> * <a href="../../IR/Typ/index.html#type-t">IR.Typ.t</a>)</span></span> <span>&#45;&gt;</span> <span>actuals:<span><span>(<span>(<a href="../PulseAbstractValue/index.html#type-t">PulseBasicInterface.AbstractValue.t</a> * <a href="../PulseValueHistory/index.html#type-t">PulseBasicInterface.ValueHistory.t</a>)</span> * <a href="../../IR/Typ/index.html#type-t">IR.Typ.t</a>)</span> list</span></span> <span>&#45;&gt;</span> <span>formals_opt:<span><span><span>(<a href="../../IR/Pvar/index.html#type-t">IR.Pvar.t</a> * <a href="../../IR/Typ/index.html#type-t">IR.Typ.t</a>)</span> list</span> option</span></span> <span>&#45;&gt;</span> <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> <span><a href="index.html#type-t">t</a> <a href="../PulseAccessResult/index.html#type-t">PulseDomainInterface.AccessResult.t</a></span></code></dt><dd><p>performs a call to a function with no summary by optimistically havoc'ing the by-ref actuals and the return value as appropriate</p></dd></dl><dl><dt class="spec value" id="val-conservatively_initialize_args"><a href="#val-conservatively_initialize_args" class="anchor"></a><code><span class="keyword">val</span> conservatively_initialize_args : <span><a href="../PulseAbstractValue/index.html#type-t">PulseBasicInterface.AbstractValue.t</a> list</span> <span>&#45;&gt;</span> <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> <a href="index.html#type-t">t</a></code></dt></dl></div></body></html>

website/static/odoc/next/infer/Pulselib/PulseInterproc/index.html

@@ -1,2 +1,2 @@
 <!DOCTYPE html>
-<html xmlns="http://www.w3.org/1999/xhtml"><head><title>PulseInterproc (infer.Pulselib.PulseInterproc)</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> &#x00BB; <a href="../index.html">Pulselib</a> &#x00BB; PulseInterproc</nav><h1>Module <code>Pulselib.PulseInterproc</code></h1></header><dl><dt class="spec value" id="val-apply_prepost"><a href="#val-apply_prepost" class="anchor"></a><code><span class="keyword">val</span> apply_prepost : <span>is_isl_error_prepost:bool</span> <span>&#45;&gt;</span> <a href="../../IR/Procname/index.html#type-t">IR.Procname.t</a> <span>&#45;&gt;</span> <a href="../../IBase/Location/index.html#type-t">IBase.Location.t</a> <span>&#45;&gt;</span> <span>callee_prepost:<a href="../PulseAbductiveDomain/index.html#type-t">PulseDomainInterface.AbductiveDomain.t</a></span> <span>&#45;&gt;</span> <span>captured_vars_with_actuals:<span><span>(<a href="../../IR/Var/index.html#type-t">IR.Var.t</a> * <span>(<span>(<a href="../PulseAbstractValue/index.html#type-t">PulseBasicInterface.AbstractValue.t</a> * <a href="../PulseValueHistory/index.html#type-t">PulseBasicInterface.ValueHistory.t</a>)</span> * <a href="../../IR/Typ/index.html#type-t">IR.Typ.t</a>)</span>)</span> list</span></span> <span>&#45;&gt;</span> <span>formals:<span><a href="../../IR/Var/index.html#type-t">IR.Var.t</a> list</span></span> <span>&#45;&gt;</span> <span>actuals:<span><span>(<span>(<a href="../PulseAbstractValue/index.html#type-t">PulseBasicInterface.AbstractValue.t</a> * <a href="../PulseValueHistory/index.html#type-t">PulseBasicInterface.ValueHistory.t</a>)</span> * <a href="../../IR/Typ/index.html#type-t">IR.Typ.t</a>)</span> list</span></span> <span>&#45;&gt;</span> <a href="../PulseAbductiveDomain/index.html#type-t">PulseDomainInterface.AbductiveDomain.t</a> <span>&#45;&gt;</span> <span><span><span>(<a href="../PulseAbductiveDomain/index.html#type-t">PulseDomainInterface.AbductiveDomain.t</a> * <span><span>(<a href="../PulseAbstractValue/index.html#type-t">PulseBasicInterface.AbstractValue.t</a> * <a href="../PulseValueHistory/index.html#type-t">PulseBasicInterface.ValueHistory.t</a>)</span> option</span> * <span><span>(<a href="../PulseAbstractValue/index.html#type-t">PulseBasicInterface.AbstractValue.t</a> * <a href="../PulseValueHistory/index.html#type-t">PulseBasicInterface.ValueHistory.t</a>)</span> <a href="../../Pulselib__PulseAbstractValue/index.html#module-Map">Pulselib.PulseBasicInterface.AbstractValue.Map</a>.t</span>)</span> <a href="../PulseAccessResult/index.html#type-t">PulseDomainInterface.AccessResult.t</a></span> <a href="../PulseSatUnsat/index.html#type-t">PulseBasicInterface.SatUnsat.t</a></span></code></dt><dd><p>result of applying one pre/post pair of a callee's summary:</p><ul><li><span class="xref-unresolved" title="unresolved reference to &quot;SatUnsat.Unsat&quot;"><code>SatUnsat</code>.Unsat</span> if that path in the callee is infeasible</li><li>otherwise, there can be an error detected</li><li>otherwise, the result is a new abstract state, an optional return value, and a substitution <code>callee_abstract_value -&gt; caller_abstract_value</code> mapping callee's abstract values to what they became in the new (caller) state</li></ul></dd></dl></div></body></html>
+<html xmlns="http://www.w3.org/1999/xhtml"><head><title>PulseInterproc (infer.Pulselib.PulseInterproc)</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> &#x00BB; <a href="../index.html">Pulselib</a> &#x00BB; PulseInterproc</nav><h1>Module <code>Pulselib.PulseInterproc</code></h1></header><dl><dt class="spec value" id="val-apply_prepost"><a href="#val-apply_prepost" class="anchor"></a><code><span class="keyword">val</span> apply_prepost : <a href="../PulsePathContext/index.html#type-t">PulseBasicInterface.PathContext.t</a> <span>&#45;&gt;</span> <span>is_isl_error_prepost:bool</span> <span>&#45;&gt;</span> <a href="../../IR/Procname/index.html#type-t">IR.Procname.t</a> <span>&#45;&gt;</span> <a href="../../IBase/Location/index.html#type-t">IBase.Location.t</a> <span>&#45;&gt;</span> <span>callee_prepost:<a href="../PulseAbductiveDomain/index.html#type-t">PulseDomainInterface.AbductiveDomain.t</a></span> <span>&#45;&gt;</span> <span>captured_vars_with_actuals:<span><span>(<a href="../../IR/Var/index.html#type-t">IR.Var.t</a> * <span>(<span>(<a href="../PulseAbstractValue/index.html#type-t">PulseBasicInterface.AbstractValue.t</a> * <a href="../PulseValueHistory/index.html#type-t">PulseBasicInterface.ValueHistory.t</a>)</span> * <a href="../../IR/Typ/index.html#type-t">IR.Typ.t</a>)</span>)</span> list</span></span> <span>&#45;&gt;</span> <span>formals:<span><a href="../../IR/Var/index.html#type-t">IR.Var.t</a> list</span></span> <span>&#45;&gt;</span> <span>actuals:<span><span>(<span>(<a href="../PulseAbstractValue/index.html#type-t">PulseBasicInterface.AbstractValue.t</a> * <a href="../PulseValueHistory/index.html#type-t">PulseBasicInterface.ValueHistory.t</a>)</span> * <a href="../../IR/Typ/index.html#type-t">IR.Typ.t</a>)</span> list</span></span> <span>&#45;&gt;</span> <a href="../PulseAbductiveDomain/index.html#type-t">PulseDomainInterface.AbductiveDomain.t</a> <span>&#45;&gt;</span> <span><span><span>(<a href="../PulseAbductiveDomain/index.html#type-t">PulseDomainInterface.AbductiveDomain.t</a> * <span><span>(<a href="../PulseAbstractValue/index.html#type-t">PulseBasicInterface.AbstractValue.t</a> * <a href="../PulseValueHistory/index.html#type-t">PulseBasicInterface.ValueHistory.t</a>)</span> option</span> * <span><span>(<a href="../PulseAbstractValue/index.html#type-t">PulseBasicInterface.AbstractValue.t</a> * <a href="../PulseValueHistory/index.html#type-t">PulseBasicInterface.ValueHistory.t</a>)</span> <a href="../../Pulselib__PulseAbstractValue/index.html#module-Map">Pulselib.PulseBasicInterface.AbstractValue.Map</a>.t</span>)</span> <a href="../PulseAccessResult/index.html#type-t">PulseDomainInterface.AccessResult.t</a></span> <a href="../PulseSatUnsat/index.html#type-t">PulseBasicInterface.SatUnsat.t</a></span></code></dt><dd><p>result of applying one pre/post pair of a callee's summary:</p><ul><li><span class="xref-unresolved" title="unresolved reference to &quot;SatUnsat.Unsat&quot;"><code>SatUnsat</code>.Unsat</span> if that path in the callee is infeasible</li><li>otherwise, there can be an error detected</li><li>otherwise, the result is a new abstract state, an optional return value, and a substitution <code>callee_abstract_value -&gt; caller_abstract_value</code> mapping callee's abstract values to what they became in the new (caller) state</li></ul></dd></dl></div></body></html>

website/static/odoc/next/infer/Pulselib/PulseModels/index.html

@@ -1,2 +1,2 @@
 <!DOCTYPE html>
-<html xmlns="http://www.w3.org/1999/xhtml"><head><title>PulseModels (infer.Pulselib.PulseModels)</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> &#x00BB; <a href="../index.html">Pulselib</a> &#x00BB; PulseModels</nav><h1>Module <code>Pulselib.PulseModels</code></h1></header><dl><dt class="spec type" id="type-model_data"><a href="#type-model_data" class="anchor"></a><code><span class="keyword">type</span> model_data</code><code> = </code><code>{</code><table class="record"><tr id="type-model_data.analysis_data" class="anchored"><td class="def field"><a href="#type-model_data.analysis_data" class="anchor"></a><code>analysis_data : <span><a href="../PulseSummary/index.html#type-t">PulseSummary.t</a> <a href="../../Absint/InterproceduralAnalysis/index.html#type-t">Absint.InterproceduralAnalysis.t</a></span>;</code></td></tr><tr id="type-model_data.callee_procname" class="anchored"><td class="def field"><a href="#type-model_data.callee_procname" class="anchor"></a><code>callee_procname : <a href="../../IR/Procname/index.html#type-t">IR.Procname.t</a>;</code></td></tr><tr id="type-model_data.location" class="anchored"><td class="def field"><a href="#type-model_data.location" class="anchor"></a><code>location : <a href="../../IBase/Location/index.html#type-t">IBase.Location.t</a>;</code></td></tr><tr id="type-model_data.ret" class="anchored"><td class="def field"><a href="#type-model_data.ret" class="anchor"></a><code>ret : <a href="../../IR/Ident/index.html#type-t">IR.Ident.t</a> * <a href="../../IR/Typ/index.html#type-t">IR.Typ.t</a>;</code></td></tr></table><code>}</code></dt><dt class="spec type" id="type-model"><a href="#type-model" class="anchor"></a><code><span class="keyword">type</span> model</code><code> = <a href="index.html#type-model_data">model_data</a> <span>&#45;&gt;</span> <a href="../PulseAbductiveDomain/index.html#type-t">PulseDomainInterface.AbductiveDomain.t</a> <span>&#45;&gt;</span> <span><span><a href="../PulseExecutionDomain/index.html#type-t">PulseDomainInterface.ExecutionDomain.t</a> <a href="../PulseAccessResult/index.html#type-t">PulseDomainInterface.AccessResult.t</a></span> list</span></code></dt></dl><dl><dt class="spec value" id="val-dispatch"><a href="#val-dispatch" class="anchor"></a><code><span class="keyword">val</span> dispatch : <a href="../../IR/Tenv/index.html#type-t">IR.Tenv.t</a> <span>&#45;&gt;</span> <a href="../../IR/Procname/index.html#type-t">IR.Procname.t</a> <span>&#45;&gt;</span> <span><span><span>(<a href="../PulseAbstractValue/index.html#type-t">PulseBasicInterface.AbstractValue.t</a> * <a href="../PulseValueHistory/index.html#type-t">PulseBasicInterface.ValueHistory.t</a>)</span> <a href="../../Absint/ProcnameDispatcher/Call/FuncArg/index.html#type-t">Absint.ProcnameDispatcher.Call.FuncArg.t</a></span> list</span> <span>&#45;&gt;</span> <span><a href="index.html#type-model">model</a> option</span></code></dt></dl></div></body></html>
+<html xmlns="http://www.w3.org/1999/xhtml"><head><title>PulseModels (infer.Pulselib.PulseModels)</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> &#x00BB; <a href="../index.html">Pulselib</a> &#x00BB; PulseModels</nav><h1>Module <code>Pulselib.PulseModels</code></h1></header><dl><dt class="spec type" id="type-model_data"><a href="#type-model_data" class="anchor"></a><code><span class="keyword">type</span> model_data</code><code> = </code><code>{</code><table class="record"><tr id="type-model_data.analysis_data" class="anchored"><td class="def field"><a href="#type-model_data.analysis_data" class="anchor"></a><code>analysis_data : <span><a href="../PulseSummary/index.html#type-t">PulseSummary.t</a> <a href="../../Absint/InterproceduralAnalysis/index.html#type-t">Absint.InterproceduralAnalysis.t</a></span>;</code></td></tr><tr id="type-model_data.path" class="anchored"><td class="def field"><a href="#type-model_data.path" class="anchor"></a><code>path : <a href="../PulsePathContext/index.html#type-t">PulseBasicInterface.PathContext.t</a>;</code></td></tr><tr id="type-model_data.callee_procname" class="anchored"><td class="def field"><a href="#type-model_data.callee_procname" class="anchor"></a><code>callee_procname : <a href="../../IR/Procname/index.html#type-t">IR.Procname.t</a>;</code></td></tr><tr id="type-model_data.location" class="anchored"><td class="def field"><a href="#type-model_data.location" class="anchor"></a><code>location : <a href="../../IBase/Location/index.html#type-t">IBase.Location.t</a>;</code></td></tr><tr id="type-model_data.ret" class="anchored"><td class="def field"><a href="#type-model_data.ret" class="anchor"></a><code>ret : <a href="../../IR/Ident/index.html#type-t">IR.Ident.t</a> * <a href="../../IR/Typ/index.html#type-t">IR.Typ.t</a>;</code></td></tr></table><code>}</code></dt><dt class="spec type" id="type-model"><a href="#type-model" class="anchor"></a><code><span class="keyword">type</span> model</code><code> = <a href="index.html#type-model_data">model_data</a> <span>&#45;&gt;</span> <a href="../PulseAbductiveDomain/index.html#type-t">PulseDomainInterface.AbductiveDomain.t</a> <span>&#45;&gt;</span> <span><span><a href="../PulseExecutionDomain/index.html#type-t">PulseDomainInterface.ExecutionDomain.t</a> <a href="../PulseAccessResult/index.html#type-t">PulseDomainInterface.AccessResult.t</a></span> list</span></code></dt></dl><dl><dt class="spec value" id="val-dispatch"><a href="#val-dispatch" class="anchor"></a><code><span class="keyword">val</span> dispatch : <a href="../../IR/Tenv/index.html#type-t">IR.Tenv.t</a> <span>&#45;&gt;</span> <a href="../../IR/Procname/index.html#type-t">IR.Procname.t</a> <span>&#45;&gt;</span> <span><span><span>(<a href="../PulseAbstractValue/index.html#type-t">PulseBasicInterface.AbstractValue.t</a> * <a href="../PulseValueHistory/index.html#type-t">PulseBasicInterface.ValueHistory.t</a>)</span> <a href="../../Absint/ProcnameDispatcher/Call/FuncArg/index.html#type-t">Absint.ProcnameDispatcher.Call.FuncArg.t</a></span> list</span> <span>&#45;&gt;</span> <span><a href="index.html#type-model">model</a> option</span></code></dt></dl></div></body></html>

website/static/odoc/next/infer/Pulselib/PulseOperations/Closures/index.html

@@ -1,2 +1,2 @@
 <!DOCTYPE html>
-<html xmlns="http://www.w3.org/1999/xhtml"><head><title>Closures (infer.Pulselib.PulseOperations.Closures)</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> &#x00BB; <a href="../../index.html">Pulselib</a> &#x00BB; <a href="../index.html">PulseOperations</a> &#x00BB; Closures</nav><h1>Module <code>PulseOperations.Closures</code></h1></header><dl><dt class="spec value" id="val-check_captured_addresses"><a href="#val-check_captured_addresses" class="anchor"></a><code><span class="keyword">val</span> check_captured_addresses : <a href="../../../IBase/Location/index.html#type-t">IBase.Location.t</a> <span>&#45;&gt;</span> <a href="../../PulseAbstractValue/index.html#type-t">PulseBasicInterface.AbstractValue.t</a> <span>&#45;&gt;</span> <a href="../index.html#type-t">t</a> <span>&#45;&gt;</span> <span><a href="../index.html#type-t">t</a> <a href="../../PulseAccessResult/index.html#type-t">PulseDomainInterface.AccessResult.t</a></span></code></dt><dd><p>assert the validity of the addresses captured by the lambda</p></dd></dl></div></body></html>
+<html xmlns="http://www.w3.org/1999/xhtml"><head><title>Closures (infer.Pulselib.PulseOperations.Closures)</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> &#x00BB; <a href="../../index.html">Pulselib</a> &#x00BB; <a href="../index.html">PulseOperations</a> &#x00BB; Closures</nav><h1>Module <code>PulseOperations.Closures</code></h1></header><dl><dt class="spec value" id="val-check_captured_addresses"><a href="#val-check_captured_addresses" class="anchor"></a><code><span class="keyword">val</span> check_captured_addresses : <a href="../../PulsePathContext/index.html#type-t">PulseBasicInterface.PathContext.t</a> <span>&#45;&gt;</span> <a href="../../../IBase/Location/index.html#type-t">IBase.Location.t</a> <span>&#45;&gt;</span> <a href="../../PulseAbstractValue/index.html#type-t">PulseBasicInterface.AbstractValue.t</a> <span>&#45;&gt;</span> <a href="../index.html#type-t">t</a> <span>&#45;&gt;</span> <span><a href="../index.html#type-t">t</a> <a href="../../PulseAccessResult/index.html#type-t">PulseDomainInterface.AccessResult.t</a></span></code></dt><dd><p>assert the validity of the addresses captured by the lambda</p></dd></dl></div></body></html>

website/static/odoc/next/infer/Pulselib/PulsePathContext/index.html

@@ -0,0 +1,2 @@
+<!DOCTYPE html>
+<html xmlns="http://www.w3.org/1999/xhtml"><head><title>PulsePathContext (infer.Pulselib.PulsePathContext)</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> &#x00BB; <a href="../index.html">Pulselib</a> &#x00BB; PulsePathContext</nav><h1>Module <code>Pulselib.PulsePathContext</code></h1></header><div class="spec module" id="module-F"><a href="#module-F" class="anchor"></a><code><span class="keyword">module</span> F = Stdlib.Format</code></div><dl><dt class="spec type" id="type-timestamp"><a href="#type-timestamp" class="anchor"></a><code><span class="keyword">type</span> timestamp</code><code> = <span class="keyword">private</span> int</code></dt></dl><div><div class="spec include"><div class="doc"><dl><dt class="spec value" id="val-compare_timestamp"><a href="#val-compare_timestamp" class="anchor"></a><code><span class="keyword">val</span> compare_timestamp : <a href="index.html#type-timestamp">timestamp</a> <span>&#45;&gt;</span> <a href="index.html#type-timestamp">timestamp</a> <span>&#45;&gt;</span> int</code></dt></dl></div></div></div><dl><dt class="spec value" id="val-t0"><a href="#val-t0" class="anchor"></a><code><span class="keyword">val</span> t0 : <a href="index.html#type-timestamp">timestamp</a></code></dt></dl><dl><dt class="spec type" id="type-t"><a href="#type-t" class="anchor"></a><code><span class="keyword">type</span> t</code><code> = </code><code>{</code><table class="record"><tr id="type-t.timestamp" class="anchored"><td class="def field"><a href="#type-t.timestamp" class="anchor"></a><code>timestamp : <a href="index.html#type-timestamp">timestamp</a>;</code></td><td class="doc"><p>step number</p></td></tr></table><code>}</code></dt></dl><dl><dt class="spec value" id="val-leq"><a href="#val-leq" class="anchor"></a><code><span class="keyword">val</span> leq : <span>lhs:<a href="index.html#type-t">t</a></span> <span>&#45;&gt;</span> <span>rhs:<a href="index.html#type-t">t</a></span> <span>&#45;&gt;</span> bool</code></dt><dt class="spec value" id="val-initial"><a href="#val-initial" class="anchor"></a><code><span class="keyword">val</span> initial : <a href="index.html#type-t">t</a></code></dt><dt class="spec value" id="val-post_exec_instr"><a href="#val-post_exec_instr" class="anchor"></a><code><span class="keyword">val</span> post_exec_instr : <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> <a href="index.html#type-t">t</a></code></dt><dd><p>call this after each step of the symbolic execution to update the path information</p></dd></dl><dl><dt class="spec value" id="val-pp"><a href="#val-pp" class="anchor"></a><code><span class="keyword">val</span> pp : <a href="index.html#module-F">F</a>.formatter <span>&#45;&gt;</span> <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> unit</code></dt></dl></div></body></html>

website/static/odoc/next/infer/Pulselib__PulseAbductiveDomain/Stack/index.html

@@ -1,2 +1,2 @@
 <!DOCTYPE html>
-<html xmlns="http://www.w3.org/1999/xhtml"><head><title>Stack (infer.Pulselib__PulseAbductiveDomain.Stack)</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> &#x00BB; <a href="../index.html">Pulselib__PulseAbductiveDomain</a> &#x00BB; Stack</nav><h1>Module <code>Pulselib__PulseAbductiveDomain.Stack</code></h1><p>stack operations like <a href="../BaseStack/index.html"><code>BaseStack</code></a> but that also take care of propagating facts to the precondition</p></header><dl><dt class="spec value" id="val-add"><a href="#val-add" class="anchor"></a><code><span class="keyword">val</span> add : <a href="../../IR/Var/index.html#type-t">IR.Var.t</a> <span>&#45;&gt;</span> <a href="../../Pulselib/PulseBaseStack/index.html#type-value">BaseStack.value</a> <span>&#45;&gt;</span> <a href="../index.html#type-t">t</a> <span>&#45;&gt;</span> <a href="../index.html#type-t">t</a></code></dt><dt class="spec value" id="val-remove_vars"><a href="#val-remove_vars" class="anchor"></a><code><span class="keyword">val</span> remove_vars : <span><a href="../../IR/Var/index.html#type-t">IR.Var.t</a> list</span> <span>&#45;&gt;</span> <a href="../index.html#type-t">t</a> <span>&#45;&gt;</span> <a href="../index.html#type-t">t</a></code></dt><dt class="spec value" id="val-fold"><a href="#val-fold" class="anchor"></a><code><span class="keyword">val</span> fold : <span>(<a href="../../IR/Var/index.html#type-t">IR.Var.t</a> <span>&#45;&gt;</span> <a href="../../Pulselib/PulseBaseStack/index.html#type-value">BaseStack.value</a> <span>&#45;&gt;</span> <span class="type-var">'a</span> <span>&#45;&gt;</span> <span class="type-var">'a</span>)</span> <span>&#45;&gt;</span> <a href="../index.html#type-t">t</a> <span>&#45;&gt;</span> <span class="type-var">'a</span> <span>&#45;&gt;</span> <span class="type-var">'a</span></code></dt><dt class="spec value" id="val-find_opt"><a href="#val-find_opt" class="anchor"></a><code><span class="keyword">val</span> find_opt : <a href="../../IR/Var/index.html#type-t">IR.Var.t</a> <span>&#45;&gt;</span> <a href="../index.html#type-t">t</a> <span>&#45;&gt;</span> <span><a href="../../Pulselib/PulseBaseStack/index.html#type-value">BaseStack.value</a> option</span></code></dt><dt class="spec value" id="val-eval"><a href="#val-eval" class="anchor"></a><code><span class="keyword">val</span> eval : <a href="../../IBase/Location/index.html#type-t">IBase.Location.t</a> <span>&#45;&gt;</span> <a href="../../Pulselib/PulseValueHistory/index.html#type-t">Pulselib.PulseBasicInterface.ValueHistory.t</a> <span>&#45;&gt;</span> <a href="../../IR/Var/index.html#type-t">IR.Var.t</a> <span>&#45;&gt;</span> <a href="../index.html#type-t">t</a> <span>&#45;&gt;</span> <a href="../index.html#type-t">t</a> * <span>(<a href="../../Pulselib/PulseAbstractValue/index.html#type-t">Pulselib.PulseBasicInterface.AbstractValue.t</a> * <a href="../../Pulselib/PulseValueHistory/index.html#type-t">Pulselib.PulseBasicInterface.ValueHistory.t</a>)</span></code></dt><dd><p>return the value of the variable in the stack or create a fresh one if needed</p></dd></dl><dl><dt class="spec value" id="val-mem"><a href="#val-mem" class="anchor"></a><code><span class="keyword">val</span> mem : <a href="../../IR/Var/index.html#type-t">IR.Var.t</a> <span>&#45;&gt;</span> <a href="../index.html#type-t">t</a> <span>&#45;&gt;</span> bool</code></dt><dt class="spec value" id="val-exists"><a href="#val-exists" class="anchor"></a><code><span class="keyword">val</span> exists : <span>(<a href="../../IR/Var/index.html#type-t">IR.Var.t</a> <span>&#45;&gt;</span> <a href="../../Pulselib/PulseBaseStack/index.html#type-value">BaseStack.value</a> <span>&#45;&gt;</span> bool)</span> <span>&#45;&gt;</span> <a href="../index.html#type-t">t</a> <span>&#45;&gt;</span> bool</code></dt><dt class="spec value" id="val-keys"><a href="#val-keys" class="anchor"></a><code><span class="keyword">val</span> keys : <a href="../index.html#type-t">t</a> <span>&#45;&gt;</span> <span><a href="../../IR/Var/index.html#type-t">IR.Var.t</a> list</span></code></dt></dl></div></body></html>
+<html xmlns="http://www.w3.org/1999/xhtml"><head><title>Stack (infer.Pulselib__PulseAbductiveDomain.Stack)</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> &#x00BB; <a href="../index.html">Pulselib__PulseAbductiveDomain</a> &#x00BB; Stack</nav><h1>Module <code>Pulselib__PulseAbductiveDomain.Stack</code></h1><p>stack operations like <a href="../BaseStack/index.html"><code>BaseStack</code></a> but that also take care of propagating facts to the precondition</p></header><dl><dt class="spec value" id="val-add"><a href="#val-add" class="anchor"></a><code><span class="keyword">val</span> add : <a href="../../IR/Var/index.html#type-t">IR.Var.t</a> <span>&#45;&gt;</span> <a href="../../Pulselib/PulseBaseStack/index.html#type-value">BaseStack.value</a> <span>&#45;&gt;</span> <a href="../index.html#type-t">t</a> <span>&#45;&gt;</span> <a href="../index.html#type-t">t</a></code></dt><dt class="spec value" id="val-remove_vars"><a href="#val-remove_vars" class="anchor"></a><code><span class="keyword">val</span> remove_vars : <span><a href="../../IR/Var/index.html#type-t">IR.Var.t</a> list</span> <span>&#45;&gt;</span> <a href="../index.html#type-t">t</a> <span>&#45;&gt;</span> <a href="../index.html#type-t">t</a></code></dt><dt class="spec value" id="val-fold"><a href="#val-fold" class="anchor"></a><code><span class="keyword">val</span> fold : <span>(<a href="../../IR/Var/index.html#type-t">IR.Var.t</a> <span>&#45;&gt;</span> <a href="../../Pulselib/PulseBaseStack/index.html#type-value">BaseStack.value</a> <span>&#45;&gt;</span> <span class="type-var">'a</span> <span>&#45;&gt;</span> <span class="type-var">'a</span>)</span> <span>&#45;&gt;</span> <a href="../index.html#type-t">t</a> <span>&#45;&gt;</span> <span class="type-var">'a</span> <span>&#45;&gt;</span> <span class="type-var">'a</span></code></dt><dt class="spec value" id="val-find_opt"><a href="#val-find_opt" class="anchor"></a><code><span class="keyword">val</span> find_opt : <a href="../../IR/Var/index.html#type-t">IR.Var.t</a> <span>&#45;&gt;</span> <a href="../index.html#type-t">t</a> <span>&#45;&gt;</span> <span><a href="../../Pulselib/PulseBaseStack/index.html#type-value">BaseStack.value</a> option</span></code></dt><dt class="spec value" id="val-eval"><a href="#val-eval" class="anchor"></a><code><span class="keyword">val</span> eval : <a href="../../Pulselib/PulsePathContext/index.html#type-t">Pulselib.PulseBasicInterface.PathContext.t</a> <span>&#45;&gt;</span> <a href="../../IBase/Location/index.html#type-t">IBase.Location.t</a> <span>&#45;&gt;</span> <a href="../../Pulselib/PulseValueHistory/index.html#type-t">Pulselib.PulseBasicInterface.ValueHistory.t</a> <span>&#45;&gt;</span> <a href="../../IR/Var/index.html#type-t">IR.Var.t</a> <span>&#45;&gt;</span> <a href="../index.html#type-t">t</a> <span>&#45;&gt;</span> <a href="../index.html#type-t">t</a> * <span>(<a href="../../Pulselib/PulseAbstractValue/index.html#type-t">Pulselib.PulseBasicInterface.AbstractValue.t</a> * <a href="../../Pulselib/PulseValueHistory/index.html#type-t">Pulselib.PulseBasicInterface.ValueHistory.t</a>)</span></code></dt><dd><p>return the value of the variable in the stack or create a fresh one if needed</p></dd></dl><dl><dt class="spec value" id="val-mem"><a href="#val-mem" class="anchor"></a><code><span class="keyword">val</span> mem : <a href="../../IR/Var/index.html#type-t">IR.Var.t</a> <span>&#45;&gt;</span> <a href="../index.html#type-t">t</a> <span>&#45;&gt;</span> bool</code></dt><dt class="spec value" id="val-exists"><a href="#val-exists" class="anchor"></a><code><span class="keyword">val</span> exists : <span>(<a href="../../IR/Var/index.html#type-t">IR.Var.t</a> <span>&#45;&gt;</span> <a href="../../Pulselib/PulseBaseStack/index.html#type-value">BaseStack.value</a> <span>&#45;&gt;</span> bool)</span> <span>&#45;&gt;</span> <a href="../index.html#type-t">t</a> <span>&#45;&gt;</span> bool</code></dt><dt class="spec value" id="val-keys"><a href="#val-keys" class="anchor"></a><code><span class="keyword">val</span> keys : <a href="../index.html#type-t">t</a> <span>&#45;&gt;</span> <span><a href="../../IR/Var/index.html#type-t">IR.Var.t</a> list</span></code></dt></dl></div></body></html>

website/static/odoc/next/infer/Pulselib__PulseInterproc/index.html

@@ -1,2 +1,2 @@
 <!DOCTYPE html>
-<html xmlns="http://www.w3.org/1999/xhtml"><head><title>Pulselib__PulseInterproc (infer.Pulselib__PulseInterproc)</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> &#x00BB; Pulselib__PulseInterproc</nav><h1>Module <code>Pulselib__PulseInterproc</code></h1></header><dl><dt class="spec value" id="val-apply_prepost"><a href="#val-apply_prepost" class="anchor"></a><code><span class="keyword">val</span> apply_prepost : <span>is_isl_error_prepost:bool</span> <span>&#45;&gt;</span> <a href="../IR/Procname/index.html#type-t">IR.Procname.t</a> <span>&#45;&gt;</span> <a href="../IBase/Location/index.html#type-t">IBase.Location.t</a> <span>&#45;&gt;</span> <span>callee_prepost:<a href="../Pulselib/PulseAbductiveDomain/index.html#type-t">Pulselib.PulseDomainInterface.AbductiveDomain.t</a></span> <span>&#45;&gt;</span> <span>captured_vars_with_actuals:<span><span>(<a href="../IR/Var/index.html#type-t">IR.Var.t</a> * <span>(<span>(<a href="../Pulselib/PulseAbstractValue/index.html#type-t">Pulselib.PulseBasicInterface.AbstractValue.t</a> * <a href="../Pulselib/PulseValueHistory/index.html#type-t">Pulselib.PulseBasicInterface.ValueHistory.t</a>)</span> * <a href="../IR/Typ/index.html#type-t">IR.Typ.t</a>)</span>)</span> list</span></span> <span>&#45;&gt;</span> <span>formals:<span><a href="../IR/Var/index.html#type-t">IR.Var.t</a> list</span></span> <span>&#45;&gt;</span> <span>actuals:<span><span>(<span>(<a href="../Pulselib/PulseAbstractValue/index.html#type-t">Pulselib.PulseBasicInterface.AbstractValue.t</a> * <a href="../Pulselib/PulseValueHistory/index.html#type-t">Pulselib.PulseBasicInterface.ValueHistory.t</a>)</span> * <a href="../IR/Typ/index.html#type-t">IR.Typ.t</a>)</span> list</span></span> <span>&#45;&gt;</span> <a href="../Pulselib/PulseAbductiveDomain/index.html#type-t">Pulselib.PulseDomainInterface.AbductiveDomain.t</a> <span>&#45;&gt;</span> <span><span><span>(<a href="../Pulselib/PulseAbductiveDomain/index.html#type-t">Pulselib.PulseDomainInterface.AbductiveDomain.t</a> * <span><span>(<a href="../Pulselib/PulseAbstractValue/index.html#type-t">Pulselib.PulseBasicInterface.AbstractValue.t</a> * <a href="../Pulselib/PulseValueHistory/index.html#type-t">Pulselib.PulseBasicInterface.ValueHistory.t</a>)</span> option</span> * <span><span>(<a href="../Pulselib/PulseAbstractValue/index.html#type-t">Pulselib.PulseBasicInterface.AbstractValue.t</a> * <a href="../Pulselib/PulseValueHistory/index.html#type-t">Pulselib.PulseBasicInterface.ValueHistory.t</a>)</span> <a href="../Pulselib__PulseAbstractValue/index.html#module-Map">Pulselib.PulseBasicInterface.AbstractValue.Map</a>.t</span>)</span> <a href="../Pulselib/PulseAccessResult/index.html#type-t">Pulselib.PulseDomainInterface.AccessResult.t</a></span> <a href="../Pulselib/PulseSatUnsat/index.html#type-t">Pulselib.PulseBasicInterface.SatUnsat.t</a></span></code></dt><dd><p>result of applying one pre/post pair of a callee's summary:</p><ul><li><span class="xref-unresolved" title="unresolved reference to &quot;SatUnsat.Unsat&quot;"><code>SatUnsat</code>.Unsat</span> if that path in the callee is infeasible</li><li>otherwise, there can be an error detected</li><li>otherwise, the result is a new abstract state, an optional return value, and a substitution <code>callee_abstract_value -&gt; caller_abstract_value</code> mapping callee's abstract values to what they became in the new (caller) state</li></ul></dd></dl></div></body></html>
+<html xmlns="http://www.w3.org/1999/xhtml"><head><title>Pulselib__PulseInterproc (infer.Pulselib__PulseInterproc)</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> &#x00BB; Pulselib__PulseInterproc</nav><h1>Module <code>Pulselib__PulseInterproc</code></h1></header><dl><dt class="spec value" id="val-apply_prepost"><a href="#val-apply_prepost" class="anchor"></a><code><span class="keyword">val</span> apply_prepost : <a href="../Pulselib/PulsePathContext/index.html#type-t">Pulselib.PulseBasicInterface.PathContext.t</a> <span>&#45;&gt;</span> <span>is_isl_error_prepost:bool</span> <span>&#45;&gt;</span> <a href="../IR/Procname/index.html#type-t">IR.Procname.t</a> <span>&#45;&gt;</span> <a href="../IBase/Location/index.html#type-t">IBase.Location.t</a> <span>&#45;&gt;</span> <span>callee_prepost:<a href="../Pulselib/PulseAbductiveDomain/index.html#type-t">Pulselib.PulseDomainInterface.AbductiveDomain.t</a></span> <span>&#45;&gt;</span> <span>captured_vars_with_actuals:<span><span>(<a href="../IR/Var/index.html#type-t">IR.Var.t</a> * <span>(<span>(<a href="../Pulselib/PulseAbstractValue/index.html#type-t">Pulselib.PulseBasicInterface.AbstractValue.t</a> * <a href="../Pulselib/PulseValueHistory/index.html#type-t">Pulselib.PulseBasicInterface.ValueHistory.t</a>)</span> * <a href="../IR/Typ/index.html#type-t">IR.Typ.t</a>)</span>)</span> list</span></span> <span>&#45;&gt;</span> <span>formals:<span><a href="../IR/Var/index.html#type-t">IR.Var.t</a> list</span></span> <span>&#45;&gt;</span> <span>actuals:<span><span>(<span>(<a href="../Pulselib/PulseAbstractValue/index.html#type-t">Pulselib.PulseBasicInterface.AbstractValue.t</a> * <a href="../Pulselib/PulseValueHistory/index.html#type-t">Pulselib.PulseBasicInterface.ValueHistory.t</a>)</span> * <a href="../IR/Typ/index.html#type-t">IR.Typ.t</a>)</span> list</span></span> <span>&#45;&gt;</span> <a href="../Pulselib/PulseAbductiveDomain/index.html#type-t">Pulselib.PulseDomainInterface.AbductiveDomain.t</a> <span>&#45;&gt;</span> <span><span><span>(<a href="../Pulselib/PulseAbductiveDomain/index.html#type-t">Pulselib.PulseDomainInterface.AbductiveDomain.t</a> * <span><span>(<a href="../Pulselib/PulseAbstractValue/index.html#type-t">Pulselib.PulseBasicInterface.AbstractValue.t</a> * <a href="../Pulselib/PulseValueHistory/index.html#type-t">Pulselib.PulseBasicInterface.ValueHistory.t</a>)</span> option</span> * <span><span>(<a href="../Pulselib/PulseAbstractValue/index.html#type-t">Pulselib.PulseBasicInterface.AbstractValue.t</a> * <a href="../Pulselib/PulseValueHistory/index.html#type-t">Pulselib.PulseBasicInterface.ValueHistory.t</a>)</span> <a href="../Pulselib__PulseAbstractValue/index.html#module-Map">Pulselib.PulseBasicInterface.AbstractValue.Map</a>.t</span>)</span> <a href="../Pulselib/PulseAccessResult/index.html#type-t">Pulselib.PulseDomainInterface.AccessResult.t</a></span> <a href="../Pulselib/PulseSatUnsat/index.html#type-t">Pulselib.PulseBasicInterface.SatUnsat.t</a></span></code></dt><dd><p>result of applying one pre/post pair of a callee's summary:</p><ul><li><span class="xref-unresolved" title="unresolved reference to &quot;SatUnsat.Unsat&quot;"><code>SatUnsat</code>.Unsat</span> if that path in the callee is infeasible</li><li>otherwise, there can be an error detected</li><li>otherwise, the result is a new abstract state, an optional return value, and a substitution <code>callee_abstract_value -&gt; caller_abstract_value</code> mapping callee's abstract values to what they became in the new (caller) state</li></ul></dd></dl></div></body></html>

website/static/odoc/next/infer/Pulselib__PulseModels/index.html

@@ -1,2 +1,2 @@
 <!DOCTYPE html>
-<html xmlns="http://www.w3.org/1999/xhtml"><head><title>Pulselib__PulseModels (infer.Pulselib__PulseModels)</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> &#x00BB; Pulselib__PulseModels</nav><h1>Module <code>Pulselib__PulseModels</code></h1></header><dl><dt class="spec type" id="type-model_data"><a href="#type-model_data" class="anchor"></a><code><span class="keyword">type</span> model_data</code><code> = </code><code>{</code><table class="record"><tr id="type-model_data.analysis_data" class="anchored"><td class="def field"><a href="#type-model_data.analysis_data" class="anchor"></a><code>analysis_data : <span><a href="../Pulselib/PulseSummary/index.html#type-t">Pulselib.PulseSummary.t</a> <a href="../Absint/InterproceduralAnalysis/index.html#type-t">Absint.InterproceduralAnalysis.t</a></span>;</code></td></tr><tr id="type-model_data.callee_procname" class="anchored"><td class="def field"><a href="#type-model_data.callee_procname" class="anchor"></a><code>callee_procname : <a href="../IR/Procname/index.html#type-t">IR.Procname.t</a>;</code></td></tr><tr id="type-model_data.location" class="anchored"><td class="def field"><a href="#type-model_data.location" class="anchor"></a><code>location : <a href="../IBase/Location/index.html#type-t">IBase.Location.t</a>;</code></td></tr><tr id="type-model_data.ret" class="anchored"><td class="def field"><a href="#type-model_data.ret" class="anchor"></a><code>ret : <a href="../IR/Ident/index.html#type-t">IR.Ident.t</a> * <a href="../IR/Typ/index.html#type-t">IR.Typ.t</a>;</code></td></tr></table><code>}</code></dt><dt class="spec type" id="type-model"><a href="#type-model" class="anchor"></a><code><span class="keyword">type</span> model</code><code> = <a href="index.html#type-model_data">model_data</a> <span>&#45;&gt;</span> <a href="../Pulselib/PulseAbductiveDomain/index.html#type-t">Pulselib.PulseDomainInterface.AbductiveDomain.t</a> <span>&#45;&gt;</span> <span><span><a href="../Pulselib/PulseExecutionDomain/index.html#type-t">Pulselib.PulseDomainInterface.ExecutionDomain.t</a> <a href="../Pulselib/PulseAccessResult/index.html#type-t">Pulselib.PulseDomainInterface.AccessResult.t</a></span> list</span></code></dt></dl><dl><dt class="spec value" id="val-dispatch"><a href="#val-dispatch" class="anchor"></a><code><span class="keyword">val</span> dispatch : <a href="../IR/Tenv/index.html#type-t">IR.Tenv.t</a> <span>&#45;&gt;</span> <a href="../IR/Procname/index.html#type-t">IR.Procname.t</a> <span>&#45;&gt;</span> <span><span><span>(<a href="../Pulselib/PulseAbstractValue/index.html#type-t">Pulselib.PulseBasicInterface.AbstractValue.t</a> * <a href="../Pulselib/PulseValueHistory/index.html#type-t">Pulselib.PulseBasicInterface.ValueHistory.t</a>)</span> <a href="../Absint/ProcnameDispatcher/Call/FuncArg/index.html#type-t">Absint.ProcnameDispatcher.Call.FuncArg.t</a></span> list</span> <span>&#45;&gt;</span> <span><a href="index.html#type-model">model</a> option</span></code></dt></dl></div></body></html>
+<html xmlns="http://www.w3.org/1999/xhtml"><head><title>Pulselib__PulseModels (infer.Pulselib__PulseModels)</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> &#x00BB; Pulselib__PulseModels</nav><h1>Module <code>Pulselib__PulseModels</code></h1></header><dl><dt class="spec type" id="type-model_data"><a href="#type-model_data" class="anchor"></a><code><span class="keyword">type</span> model_data</code><code> = </code><code>{</code><table class="record"><tr id="type-model_data.analysis_data" class="anchored"><td class="def field"><a href="#type-model_data.analysis_data" class="anchor"></a><code>analysis_data : <span><a href="../Pulselib/PulseSummary/index.html#type-t">Pulselib.PulseSummary.t</a> <a href="../Absint/InterproceduralAnalysis/index.html#type-t">Absint.InterproceduralAnalysis.t</a></span>;</code></td></tr><tr id="type-model_data.path" class="anchored"><td class="def field"><a href="#type-model_data.path" class="anchor"></a><code>path : <a href="../Pulselib/PulsePathContext/index.html#type-t">Pulselib.PulseBasicInterface.PathContext.t</a>;</code></td></tr><tr id="type-model_data.callee_procname" class="anchored"><td class="def field"><a href="#type-model_data.callee_procname" class="anchor"></a><code>callee_procname : <a href="../IR/Procname/index.html#type-t">IR.Procname.t</a>;</code></td></tr><tr id="type-model_data.location" class="anchored"><td class="def field"><a href="#type-model_data.location" class="anchor"></a><code>location : <a href="../IBase/Location/index.html#type-t">IBase.Location.t</a>;</code></td></tr><tr id="type-model_data.ret" class="anchored"><td class="def field"><a href="#type-model_data.ret" class="anchor"></a><code>ret : <a href="../IR/Ident/index.html#type-t">IR.Ident.t</a> * <a href="../IR/Typ/index.html#type-t">IR.Typ.t</a>;</code></td></tr></table><code>}</code></dt><dt class="spec type" id="type-model"><a href="#type-model" class="anchor"></a><code><span class="keyword">type</span> model</code><code> = <a href="index.html#type-model_data">model_data</a> <span>&#45;&gt;</span> <a href="../Pulselib/PulseAbductiveDomain/index.html#type-t">Pulselib.PulseDomainInterface.AbductiveDomain.t</a> <span>&#45;&gt;</span> <span><span><a href="../Pulselib/PulseExecutionDomain/index.html#type-t">Pulselib.PulseDomainInterface.ExecutionDomain.t</a> <a href="../Pulselib/PulseAccessResult/index.html#type-t">Pulselib.PulseDomainInterface.AccessResult.t</a></span> list</span></code></dt></dl><dl><dt class="spec value" id="val-dispatch"><a href="#val-dispatch" class="anchor"></a><code><span class="keyword">val</span> dispatch : <a href="../IR/Tenv/index.html#type-t">IR.Tenv.t</a> <span>&#45;&gt;</span> <a href="../IR/Procname/index.html#type-t">IR.Procname.t</a> <span>&#45;&gt;</span> <span><span><span>(<a href="../Pulselib/PulseAbstractValue/index.html#type-t">Pulselib.PulseBasicInterface.AbstractValue.t</a> * <a href="../Pulselib/PulseValueHistory/index.html#type-t">Pulselib.PulseBasicInterface.ValueHistory.t</a>)</span> <a href="../Absint/ProcnameDispatcher/Call/FuncArg/index.html#type-t">Absint.ProcnameDispatcher.Call.FuncArg.t</a></span> list</span> <span>&#45;&gt;</span> <span><a href="index.html#type-model">model</a> option</span></code></dt></dl></div></body></html>

website/static/odoc/next/infer/Pulselib__PulseOperations/Closures/index.html

@@ -1,2 +1,2 @@
 <!DOCTYPE html>
-<html xmlns="http://www.w3.org/1999/xhtml"><head><title>Closures (infer.Pulselib__PulseOperations.Closures)</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> &#x00BB; <a href="../index.html">Pulselib__PulseOperations</a> &#x00BB; Closures</nav><h1>Module <code>Pulselib__PulseOperations.Closures</code></h1></header><dl><dt class="spec value" id="val-check_captured_addresses"><a href="#val-check_captured_addresses" class="anchor"></a><code><span class="keyword">val</span> check_captured_addresses : <a href="../../IBase/Location/index.html#type-t">IBase.Location.t</a> <span>&#45;&gt;</span> <a href="../../Pulselib/PulseAbstractValue/index.html#type-t">Pulselib.PulseBasicInterface.AbstractValue.t</a> <span>&#45;&gt;</span> <a href="../index.html#type-t">t</a> <span>&#45;&gt;</span> <span><a href="../index.html#type-t">t</a> <a href="../../Pulselib/PulseAccessResult/index.html#type-t">Pulselib.PulseDomainInterface.AccessResult.t</a></span></code></dt><dd><p>assert the validity of the addresses captured by the lambda</p></dd></dl></div></body></html>
+<html xmlns="http://www.w3.org/1999/xhtml"><head><title>Closures (infer.Pulselib__PulseOperations.Closures)</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> &#x00BB; <a href="../index.html">Pulselib__PulseOperations</a> &#x00BB; Closures</nav><h1>Module <code>Pulselib__PulseOperations.Closures</code></h1></header><dl><dt class="spec value" id="val-check_captured_addresses"><a href="#val-check_captured_addresses" class="anchor"></a><code><span class="keyword">val</span> check_captured_addresses : <a href="../../Pulselib/PulsePathContext/index.html#type-t">Pulselib.PulseBasicInterface.PathContext.t</a> <span>&#45;&gt;</span> <a href="../../IBase/Location/index.html#type-t">IBase.Location.t</a> <span>&#45;&gt;</span> <a href="../../Pulselib/PulseAbstractValue/index.html#type-t">Pulselib.PulseBasicInterface.AbstractValue.t</a> <span>&#45;&gt;</span> <a href="../index.html#type-t">t</a> <span>&#45;&gt;</span> <span><a href="../index.html#type-t">t</a> <a href="../../Pulselib/PulseAccessResult/index.html#type-t">Pulselib.PulseDomainInterface.AccessResult.t</a></span></code></dt><dd><p>assert the validity of the addresses captured by the lambda</p></dd></dl></div></body></html>

website/static/odoc/next/infer/Pulselib__PulsePathContext/index.html

@@ -0,0 +1,2 @@
+<!DOCTYPE html>
+<html xmlns="http://www.w3.org/1999/xhtml"><head><title>Pulselib__PulsePathContext (infer.Pulselib__PulsePathContext)</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> &#x00BB; Pulselib__PulsePathContext</nav><h1>Module <code>Pulselib__PulsePathContext</code></h1></header><div class="spec module" id="module-F"><a href="#module-F" class="anchor"></a><code><span class="keyword">module</span> F = Stdlib.Format</code></div><dl><dt class="spec type" id="type-timestamp"><a href="#type-timestamp" class="anchor"></a><code><span class="keyword">type</span> timestamp</code><code> = <span class="keyword">private</span> int</code></dt></dl><div><div class="spec include"><div class="doc"><dl><dt class="spec value" id="val-compare_timestamp"><a href="#val-compare_timestamp" class="anchor"></a><code><span class="keyword">val</span> compare_timestamp : <a href="index.html#type-timestamp">timestamp</a> <span>&#45;&gt;</span> <a href="index.html#type-timestamp">timestamp</a> <span>&#45;&gt;</span> int</code></dt></dl></div></div></div><dl><dt class="spec value" id="val-t0"><a href="#val-t0" class="anchor"></a><code><span class="keyword">val</span> t0 : <a href="index.html#type-timestamp">timestamp</a></code></dt></dl><dl><dt class="spec type" id="type-t"><a href="#type-t" class="anchor"></a><code><span class="keyword">type</span> t</code><code> = </code><code>{</code><table class="record"><tr id="type-t.timestamp" class="anchored"><td class="def field"><a href="#type-t.timestamp" class="anchor"></a><code>timestamp : <a href="index.html#type-timestamp">timestamp</a>;</code></td><td class="doc"><p>step number</p></td></tr></table><code>}</code></dt></dl><dl><dt class="spec value" id="val-leq"><a href="#val-leq" class="anchor"></a><code><span class="keyword">val</span> leq : <span>lhs:<a href="index.html#type-t">t</a></span> <span>&#45;&gt;</span> <span>rhs:<a href="index.html#type-t">t</a></span> <span>&#45;&gt;</span> bool</code></dt><dt class="spec value" id="val-initial"><a href="#val-initial" class="anchor"></a><code><span class="keyword">val</span> initial : <a href="index.html#type-t">t</a></code></dt><dt class="spec value" id="val-post_exec_instr"><a href="#val-post_exec_instr" class="anchor"></a><code><span class="keyword">val</span> post_exec_instr : <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> <a href="index.html#type-t">t</a></code></dt><dd><p>call this after each step of the symbolic execution to update the path information</p></dd></dl><dl><dt class="spec value" id="val-pp"><a href="#val-pp" class="anchor"></a><code><span class="keyword">val</span> pp : <a href="index.html#module-F">F</a>.formatter <span>&#45;&gt;</span> <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> unit</code></dt></dl></div></body></html>