[infer] Update website (next version)

Reviewed By: jvillard

Differential Revision: D26751260

fbshipit-source-id: dae846ed8
master
Sungkeun Cho 4 years ago committed by Facebook GitHub Bot
parent e9c02d9c63
commit fc19c55b0a

@ -4,11 +4,11 @@
"doc_entries": [ "doc_entries": [
"all-issue-types", "checker-annotation-reachability", "all-issue-types", "checker-annotation-reachability",
"checker-biabduction", "checker-bufferoverrun", "checker-biabduction", "checker-bufferoverrun",
"checker-config-checks-between-markers", "checker-cost", "checker-config-checks-between-markers",
"checker-eradicate", "checker-fragment-retains-view", "checker-config-impact-analysis", "checker-cost", "checker-eradicate",
"checker-immutable-cast", "checker-impurity", "checker-fragment-retains-view", "checker-immutable-cast",
"checker-inefficient-keyset-iterator", "checker-linters", "checker-impurity", "checker-inefficient-keyset-iterator",
"checker-litho-required-props", "checker-liveness", "checker-linters", "checker-litho-required-props", "checker-liveness",
"checker-loop-hoisting", "checker-printf-args", "checker-pulse", "checker-loop-hoisting", "checker-printf-args", "checker-pulse",
"checker-purity", "checker-quandary", "checker-racerd", "checker-purity", "checker-quandary", "checker-racerd",
"checker-resource-leak-lab", "checker-dotnet-resource-leak", "checker-resource-leak-lab", "checker-dotnet-resource-leak",

@ -297,6 +297,11 @@ A condition expression is **always** evaluated to true.
Reported as "Config Checks Between Markers" by [config-checks-between-markers](/docs/next/checker-config-checks-between-markers). Reported as "Config Checks Between Markers" by [config-checks-between-markers](/docs/next/checker-config-checks-between-markers).
A config checking is done between a marker's start and end A config checking is done between a marker's start and end
## CONFIG_IMPACT
Reported as "Config Impact" by [config-impact-analysis](/docs/next/checker-config-impact-analysis).
A function is called without a config check
## CONSTANT_ADDRESS_DEREFERENCE ## CONSTANT_ADDRESS_DEREFERENCE
Reported as "Constant Address Dereference" by [pulse](/docs/next/checker-pulse). Reported as "Constant Address Dereference" by [pulse](/docs/next/checker-pulse).
@ -936,6 +941,27 @@ class C {
Action: Protect the offending access by acquiring the lock indicated by the `@GuardedBy(...)`. Action: Protect the offending access by acquiring the lock indicated by the `@GuardedBy(...)`.
## GUARDEDBY_VIOLATION_NULLSAFE
Reported as "GuardedBy Violation in `@Nullsafe` Class" by [racerd](/docs/next/checker-racerd).
A field annotated with `@GuardedBy` is being accessed by a call-chain that starts at a non-private method without synchronization.
Example:
```java
class C {
@GuardedBy("this")
String f;
void foo(String s) {
f = s; // unprotected access here
}
}
```
Action: Protect the offending access by acquiring the lock indicated by the `@GuardedBy(...)`.
## IMPURE_FUNCTION ## IMPURE_FUNCTION
Reported as "Impure Function" by [impurity](/docs/next/checker-impurity). Reported as "Impure Function" by [impurity](/docs/next/checker-impurity).
@ -1494,9 +1520,9 @@ created, and not an array `@[@"aaa", str, @"bbb"]` of size 3 as expected.
## PULSE_UNINITIALIZED_VALUE ## PULSE_UNINITIALIZED_VALUE
Reported as "Unitialized Value" by [pulse](/docs/next/checker-pulse). Reported as "Uninitialized Value" by [pulse](/docs/next/checker-pulse).
See [UNITIALIZED_VALUE](#uninitialized_value). Re-implemented using Pulse. See [UNINITIALIZED_VALUE](#uninitialized_value). Re-implemented using Pulse.
## PURE_FUNCTION ## PURE_FUNCTION
Reported as "Pure Function" by [purity](/docs/next/checker-purity). Reported as "Pure Function" by [purity](/docs/next/checker-purity).
@ -2069,6 +2095,102 @@ NB RacerD currently **does not recognize `@WorkerThread`, `@BinderThread` or
These annotations can be found at `com.facebook.infer.annotation.*`. These annotations can be found at `com.facebook.infer.annotation.*`.
- `@Functional` This is a method annotation indicating the method always returns
the same value. When a method `foo` is annotated `@Functional`, RacerD will
ignore any writes of the return value of `foo`. For example, in
`this.x = foo()`, the write to `this.x` is ignored. The reasoning is that if
the method returns the same value whenever it's called, any data race on
`this.x` is benign, if that is the only write.
- `@ThreadConfined` This is a class/method/field annotation which takes a single
parameter which can be `UI`, `ANY` or a user chosen string. It indicates to
RacerD a thread identifier for the class/method/field. Thus,
`@ThreadConfined(UI)` is equivalent to `@UiThread`, and `@ThreadConfined(ANY)`
is equivalent to not having the annotation at all, for classes and methods.
When this annotation is applied to a field it instructs Infer to assume
(without checking) that all accesses to that field are made on the same thread
(and can, therefore, not race by definition). The intention is that RacerD
uses that to detect exclusion between accesses occurring on the same thread.
However, only the UI thread is supported at this time, and any user provided
value is considered equal to `UI`.
- `@VisibleForTesting` A method annotation making Infer consider the method as
effectively `private`. This means it will not be checked for races against
other non-private methods of the class, but only if called by one.
- `@ReturnsOwnership` A method annotation indicating that the method returns a
freshly owned object. Accesses to the returned value will not be considered
for data races, as the object is in-effect unique and not accessible yet from
other threads. The main utility of this annotation is in interfaces, where
Infer cannot look up the implementation and decide for itself.
## THREAD_SAFETY_VIOLATION_NULLSAFE
Reported as "Thread Safety Violation in `@Nullsafe` Class" by [racerd](/docs/next/checker-racerd).
This warning indicates a potential data race in Java. The analyser is called
RacerD and this section gives brief but a mostly complete description of its
features. See the [RacerD page](/docs/next/checker-racerd) for more in-depth information and
examples.
### Thread-safety: What is a data race
Here a data race is a pair of accesses to the same member field such that:
- at least one is a write, and,
- at least one occurs without any lock synchronization, and,
- the two accesses occur on threads (if known) which can run in parallel.
### Thread-safety: Potential fixes
- Synchronizing the accesses (using the `synchronized` keyword, thread-exclusion
such as atomic objects, `volatile` etc).
- Making an offending method private -- this will exclude it from being checked
at the top level, though it will be checked if called by a public method which
may itself, e.g., hold a lock when calling it.
- Putting the two accesses on the same thread, e.g., by using `@MainThread` or
`@ThreadConfined`.
### Thread-safety: Conditions checked before reporting
The class and method are not marked `@ThreadSafe(enableChecks = false)`, and,
- The method is declared `synchronized`, or employs (non-transitively) locking,
or,
- The class is not marked `@NotThreadSafe`, and,
- The class/method is marked `@ThreadSafe,` or one of the configured synonyms
in `.inferconfig`, or,
- A parent class, or an override method are marked with the above annotations.
NB currently RacerD **does not take into account `@GuardedBy`**.
### Thread-safety: Thread annotations recognized by RacerD
These class and method annotations imply the method is on the main thread:
`@MainThread`, `@UiThread`
These method annotations imply the method is on the main thread: `@OnBind`,
`@OnEvent`, `@OnMount`, `@OnUnbind`, `@OnUnmount`
Both classes of annotations work through the inheritance tree (i.e. if a parent
class or method is marked with one of these annotations, so is the child class /
method override).
In addition to these, RacerD recognizes many lifecycle methods as necessarily
running on the main thread, eg `Fragment.onCreate` etc.
Finally, the thread status of being on the main thread propagates backwards
through the call graph (ie if `foo` calls `bar` and `bar` is marked `@UiThtread`
then `foo` is automatically considered on the main thread too). Calling
`assertMainThread`, `assertOnUiThread`, `checkOnMainThread` has the same effect.
NB RacerD currently **does not recognize `@WorkerThread`, `@BinderThread` or
`@AnyThread`**.
### Thread-safety: Other annotations and what they do
These annotations can be found at `com.facebook.infer.annotation.*`.
- `@Functional` This is a method annotation indicating the method always returns - `@Functional` This is a method annotation indicating the method always returns
the same value. When a method `foo` is annotated `@Functional`, RacerD will the same value. When a method `foo` is annotated `@Functional`, RacerD will
ignore any writes of the return value of `foo`. For example, in ignore any writes of the return value of `foo`. For example, in

@ -12,7 +12,7 @@ Supported languages:
- Java: Experimental - Java: Experimental
- C#/.Net: Experimental - C#/.Net: Experimental
This checker is currently only useful for certain Facebook code. This checker collects config checkings in some program regions determined by pairs of marker-starts and marker-ends. The set of config checking functions, marker-start functions, and marker-end functions is hardcoded and empty by default for now, so to use this checker, please modify the code directly in [FbGKInteraction.ml](https://github.com/facebook/infer/tree/master/infer/src/opensource).
## List of Issue Types ## List of Issue Types

@ -70,10 +70,10 @@ where `foo` has a linear cost in its parameter, then Infer automatically detects
Unlike other Infer analyses (which report found issues/bugs when running infer once), cost analysis only reports an issue for differential analysis (i.e. when comparing the analysis results on the original and the modified files). Instead, infer writes the execution cost of the program into `infer-out/costs-report.json` file. For each procedure, `costs-report.json` includes the actual polynomial (for the exection cost) along with the degree of the polynomial, the procedure name, line number etc. Unlike other Infer analyses (which report found issues/bugs when running infer once), cost analysis only reports an issue for differential analysis (i.e. when comparing the analysis results on the original and the modified files). Instead, infer writes the execution cost of the program into `infer-out/costs-report.json` file. For each procedure, `costs-report.json` includes the actual polynomial (for the exection cost) along with the degree of the polynomial, the procedure name, line number etc.
Differential cost analysis in action: Differential cost analysis in action:
- first run infer's cost analysis on `File.java` and rename `costs-report.json` (which is in `/infer-out`) to `previous-costs-report.json` - first run infer's cost analysis on `File.java` and copy `inter-out/costs-report.json` to `previous-costs-report.json` (Note that the file should be copied outside the result directory because the directory will be removed in the second infer run.)
- modify the function as shown above - modify `File.java` as shown above
- re-run infer on `File.java` and rename `costs-report.json` to `current-costs-report.json` - re-run infer on `File.java` and copy `infer-out/costs-report.json` to `current-costs-report.json`
- run `infer reportdiff --costs-current current-costs-report.json --costs-previous current-costs-report`. - run `infer reportdiff --costs-current current-costs-report.json --costs-previous previous-costs-report.json`.
- Inspect `infer-out/differential/introduced.json` to see the newly found complexity increase issue(s). - Inspect `infer-out/differential/introduced.json` to see the newly found complexity increase issue(s).

@ -500,6 +500,8 @@ resource.
The following issue types are reported by this checker: The following issue types are reported by this checker:
- [GUARDEDBY_VIOLATION](/docs/next/all-issue-types#guardedby_violation) - [GUARDEDBY_VIOLATION](/docs/next/all-issue-types#guardedby_violation)
- [GUARDEDBY_VIOLATION_NULLSAFE](/docs/next/all-issue-types#guardedby_violation_nullsafe)
- [INTERFACE_NOT_THREAD_SAFE](/docs/next/all-issue-types#interface_not_thread_safe) - [INTERFACE_NOT_THREAD_SAFE](/docs/next/all-issue-types#interface_not_thread_safe)
- [LOCK_CONSISTENCY_VIOLATION](/docs/next/all-issue-types#lock_consistency_violation) - [LOCK_CONSISTENCY_VIOLATION](/docs/next/all-issue-types#lock_consistency_violation)
- [THREAD_SAFETY_VIOLATION](/docs/next/all-issue-types#thread_safety_violation) - [THREAD_SAFETY_VIOLATION](/docs/next/all-issue-types#thread_safety_violation)
- [THREAD_SAFETY_VIOLATION_NULLSAFE](/docs/next/all-issue-types#thread_safety_violation_nullsafe)

@ -133,6 +133,21 @@ config-checks-between-markers and disable all other checkers
(Conversely: (Conversely:
<b>--no-config-checks-between-markers-only</b>)</p> <b>--no-config-checks-between-markers-only</b>)</p>
<p style="margin-left:11%;"><b>--config-impact-analysis</b></p>
<p style="margin-left:17%;">Activates: checker
config-impact-analysis: [EXPERIMENTAL] Collects function
that are called without config checks. (Conversely:
<b>--no-config-impact-analysis</b>)</p>
<p style="margin-left:11%;"><b>--config-impact-analysis-only</b></p>
<p style="margin-left:17%;">Activates: Enable
config-impact-analysis and disable all other checkers
(Conversely: <b>--no-config-impact-analysis-only</b>)</p>
<p style="margin-left:11%;"><b>--continue-analysis</b></p> <p style="margin-left:11%;"><b>--continue-analysis</b></p>
<p style="margin-left:17%;">Activates: Continue the <p style="margin-left:17%;">Activates: Continue the

@ -508,6 +508,13 @@ frontend tests (also sets <b>--print-types</b>) (Conversely:
header files (Conversely: <b>--no-headers</b>)</p> header files (Conversely: <b>--no-headers</b>)</p>
<p style="margin-left:11%;"><b>--skip-non-capture-clang-commands</b></p>
<p style="margin-left:17%;">Activates: Skip clang commands
that Infer doesn't use to capture data (Conversely:
<b>--no-skip-non-capture-clang-commands</b>)</p>
<p style="margin-left:11%;"><b>--skip-translation-headers</b> <p style="margin-left:11%;"><b>--skip-translation-headers</b>
<i>+path_prefix</i></p> <i>+path_prefix</i></p>

@ -87,6 +87,13 @@ are tested by the regex are relative to the
&lsquo;&lt;reason_string&gt;&lsquo; is a non-empty string &lsquo;&lt;reason_string&gt;&lsquo; is a non-empty string
used to explain why the issue was filtered.</p> used to explain why the issue was filtered.</p>
<p style="margin-left:11%;"><b>--config-impact-data-file</b>
<i>file</i></p>
<p style="margin-left:17%;">[ConfigImpact] Specify the file
containing the config data</p>
<p style="margin-left:11%;"><b>--cost-issues-tests</b> <p style="margin-left:11%;"><b>--cost-issues-tests</b>
<i>file</i></p> <i>file</i></p>
@ -213,6 +220,7 @@ default), <br>
CONDITION_ALWAYS_FALSE (disabled by default), <br> CONDITION_ALWAYS_FALSE (disabled by default), <br>
CONDITION_ALWAYS_TRUE (disabled by default), <br> CONDITION_ALWAYS_TRUE (disabled by default), <br>
CONFIG_CHECKS_BETWEEN_MARKERS (disabled by default), <br> CONFIG_CHECKS_BETWEEN_MARKERS (disabled by default), <br>
CONFIG_IMPACT (disabled by default), <br>
CONSTANT_ADDRESS_DEREFERENCE (disabled by default), <br> CONSTANT_ADDRESS_DEREFERENCE (disabled by default), <br>
CREATE_INTENT_FROM_URI (enabled by default), <br> CREATE_INTENT_FROM_URI (enabled by default), <br>
CROSS_SITE_SCRIPTING (enabled by default), <br> CROSS_SITE_SCRIPTING (enabled by default), <br>
@ -275,6 +283,7 @@ GLOBAL_VARIABLE_INITIALIZED_WITH_FUNCTION_OR_METHOD_CALL
<br> <br>
(disabled by default), <br> (disabled by default), <br>
GUARDEDBY_VIOLATION (enabled by default), <br> GUARDEDBY_VIOLATION (enabled by default), <br>
GUARDEDBY_VIOLATION_NULLSAFE (enabled by default), <br>
IMPURE_FUNCTION (enabled by default), <br> IMPURE_FUNCTION (enabled by default), <br>
INEFFICIENT_KEYSET_ITERATOR (enabled by default), <br> INEFFICIENT_KEYSET_ITERATOR (enabled by default), <br>
INFERBO_ALLOC_IS_BIG (enabled by default), <br> INFERBO_ALLOC_IS_BIG (enabled by default), <br>
@ -338,6 +347,7 @@ STRONG_DELEGATE_WARNING (enabled by default), <br>
STRONG_SELF_NOT_CHECKED (enabled by default), <br> STRONG_SELF_NOT_CHECKED (enabled by default), <br>
Symexec_memory_error (enabled by default), <br> Symexec_memory_error (enabled by default), <br>
THREAD_SAFETY_VIOLATION (enabled by default), <br> THREAD_SAFETY_VIOLATION (enabled by default), <br>
THREAD_SAFETY_VIOLATION_NULLSAFE (enabled by default), <br>
TOPL_BIABD_ERROR (enabled by default), <br> TOPL_BIABD_ERROR (enabled by default), <br>
TOPL_PULSE_ERROR (enabled by default), <br> TOPL_PULSE_ERROR (enabled by default), <br>
UNINITIALIZED_VALUE (enabled by default), <br> UNINITIALIZED_VALUE (enabled by default), <br>

@ -455,6 +455,30 @@ config-checks-between-markers and disable all other checkers
<p style="margin-left:11%;">See also <p style="margin-left:11%;">See also
<b>infer-analyze</b>(1). <b><br> <b>infer-analyze</b>(1). <b><br>
--config-impact-analysis</b></p>
<p style="margin-left:17%;">Activates: checker
config-impact-analysis: [EXPERIMENTAL] Collects function
that are called without config checks. (Conversely:
<b>--no-config-impact-analysis</b>)</p>
<p style="margin-left:11%;">See also
<b>infer-analyze</b>(1). <b><br>
--config-impact-analysis-only</b></p>
<p style="margin-left:17%;">Activates: Enable
config-impact-analysis and disable all other checkers
(Conversely: <b>--no-config-impact-analysis-only</b>)</p>
<p style="margin-left:11%;">See also
<b>infer-analyze</b>(1). <b><br>
--config-impact-data-file</b> <i>file</i></p>
<p style="margin-left:17%;">[ConfigImpact] Specify the file
containing the config data</p>
<p style="margin-left:11%;">See also
<b>infer-report</b>(1). <b><br>
--continue</b></p> --continue</b></p>
<p style="margin-left:17%;">Activates: Continue the capture <p style="margin-left:17%;">Activates: Continue the capture
@ -723,6 +747,7 @@ default), <br>
CONDITION_ALWAYS_FALSE (disabled by default), <br> CONDITION_ALWAYS_FALSE (disabled by default), <br>
CONDITION_ALWAYS_TRUE (disabled by default), <br> CONDITION_ALWAYS_TRUE (disabled by default), <br>
CONFIG_CHECKS_BETWEEN_MARKERS (disabled by default), <br> CONFIG_CHECKS_BETWEEN_MARKERS (disabled by default), <br>
CONFIG_IMPACT (disabled by default), <br>
CONSTANT_ADDRESS_DEREFERENCE (disabled by default), <br> CONSTANT_ADDRESS_DEREFERENCE (disabled by default), <br>
CREATE_INTENT_FROM_URI (enabled by default), <br> CREATE_INTENT_FROM_URI (enabled by default), <br>
CROSS_SITE_SCRIPTING (enabled by default), <br> CROSS_SITE_SCRIPTING (enabled by default), <br>
@ -785,6 +810,7 @@ GLOBAL_VARIABLE_INITIALIZED_WITH_FUNCTION_OR_METHOD_CALL
<br> <br>
(disabled by default), <br> (disabled by default), <br>
GUARDEDBY_VIOLATION (enabled by default), <br> GUARDEDBY_VIOLATION (enabled by default), <br>
GUARDEDBY_VIOLATION_NULLSAFE (enabled by default), <br>
IMPURE_FUNCTION (enabled by default), <br> IMPURE_FUNCTION (enabled by default), <br>
INEFFICIENT_KEYSET_ITERATOR (enabled by default), <br> INEFFICIENT_KEYSET_ITERATOR (enabled by default), <br>
INFERBO_ALLOC_IS_BIG (enabled by default), <br> INFERBO_ALLOC_IS_BIG (enabled by default), <br>
@ -848,6 +874,7 @@ STRONG_DELEGATE_WARNING (enabled by default), <br>
STRONG_SELF_NOT_CHECKED (enabled by default), <br> STRONG_SELF_NOT_CHECKED (enabled by default), <br>
Symexec_memory_error (enabled by default), <br> Symexec_memory_error (enabled by default), <br>
THREAD_SAFETY_VIOLATION (enabled by default), <br> THREAD_SAFETY_VIOLATION (enabled by default), <br>
THREAD_SAFETY_VIOLATION_NULLSAFE (enabled by default), <br>
TOPL_BIABD_ERROR (enabled by default), <br> TOPL_BIABD_ERROR (enabled by default), <br>
TOPL_PULSE_ERROR (enabled by default), <br> TOPL_PULSE_ERROR (enabled by default), <br>
UNINITIALIZED_VALUE (enabled by default), <br> UNINITIALIZED_VALUE (enabled by default), <br>
@ -1952,6 +1979,14 @@ differential reports (Conversely:
<p style="margin-left:11%;">See also <p style="margin-left:11%;">See also
<b>infer-reportdiff</b>(1). <b><br> <b>infer-reportdiff</b>(1). <b><br>
--skip-non-capture-clang-commands</b></p>
<p style="margin-left:17%;">Activates: Skip clang commands
that Infer doesn't use to capture data (Conversely:
<b>--no-skip-non-capture-clang-commands</b>)</p>
<p style="margin-left:11%;">See also
<b>infer-capture</b>(1). <b><br>
--skip-translation-headers</b> <i>+path_prefix</i></p> --skip-translation-headers</b> <i>+path_prefix</i></p>
<p style="margin-left:17%;">Ignore headers whose path <p style="margin-left:17%;">Ignore headers whose path

File diff suppressed because one or more lines are too long

File diff suppressed because one or more lines are too long

File diff suppressed because one or more lines are too long

File diff suppressed because one or more lines are too long

File diff suppressed because one or more lines are too long

File diff suppressed because one or more lines are too long

File diff suppressed because one or more lines are too long

File diff suppressed because one or more lines are too long

@ -1,2 +1,2 @@
<!DOCTYPE html> <!DOCTYPE html>
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>Exe_env (infer.Absint.Exe_env)</title><link rel="stylesheet" href="../../../odoc.css"/><meta charset="utf-8"/><meta name="generator" content="odoc 1.5.2"/><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; Exe_env</nav><h1>Module <code>Absint.Exe_env</code></h1></header><aside><p>Execution environments are a means to get a function's type environment and integer widths and cache those</p></aside><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-mk"><a href="#val-mk" class="anchor"></a><code><span class="keyword">val</span> mk : unit <span>&#45;&gt;</span> <a href="index.html#type-t">t</a></code></dt><dd><p>Create a new cache</p></dd></dl><dl><dt class="spec value" id="val-get_tenv"><a href="#val-get_tenv" class="anchor"></a><code><span class="keyword">val</span> get_tenv : <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> <a href="../../IR/Procname/index.html#type-t">IR.Procname.t</a> <span>&#45;&gt;</span> <a href="../../IR/Tenv/index.html#type-t">IR.Tenv.t</a></code></dt><dd><p>return the type environment associated with the procedure</p></dd></dl><dl><dt class="spec value" id="val-load_java_global_tenv"><a href="#val-load_java_global_tenv" class="anchor"></a><code><span class="keyword">val</span> load_java_global_tenv : <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> <a href="../../IR/Tenv/index.html#type-t">IR.Tenv.t</a></code></dt><dd><p>Load Java type environment (if not done yet), and return it. Useful for accessing type info not related to any concrete function.</p></dd></dl><dl><dt class="spec value" id="val-get_integer_type_widths"><a href="#val-get_integer_type_widths" class="anchor"></a><code><span class="keyword">val</span> get_integer_type_widths : <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> <a href="../../IR/Procname/index.html#type-t">IR.Procname.t</a> <span>&#45;&gt;</span> <a href="../../IR/Typ/IntegerWidths/index.html#type-t">IR.Typ.IntegerWidths.t</a></code></dt><dd><p>return the integer type widths associated with the procedure</p></dd></dl></div></body></html> <html xmlns="http://www.w3.org/1999/xhtml"><head><title>Exe_env (infer.Absint.Exe_env)</title><link rel="stylesheet" href="../../../odoc.css"/><meta charset="utf-8"/><meta name="generator" content="odoc 1.5.2"/><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; Exe_env</nav><h1>Module <code>Absint.Exe_env</code></h1></header><aside><p>Execution environments are a means to get a function's type environment and integer widths and cache those</p></aside><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-mk"><a href="#val-mk" class="anchor"></a><code><span class="keyword">val</span> mk : unit <span>&#45;&gt;</span> <a href="index.html#type-t">t</a></code></dt><dd><p>Create a new cache</p></dd></dl><dl><dt class="spec value" id="val-get_proc_tenv"><a href="#val-get_proc_tenv" class="anchor"></a><code><span class="keyword">val</span> get_proc_tenv : <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> <a href="../../IR/Procname/index.html#type-t">IR.Procname.t</a> <span>&#45;&gt;</span> <a href="../../IR/Tenv/index.html#type-t">IR.Tenv.t</a></code></dt><dd><p>return the type environment associated with the procedure</p></dd></dl><dl><dt class="spec value" id="val-get_sourcefile_tenv"><a href="#val-get_sourcefile_tenv" class="anchor"></a><code><span class="keyword">val</span> get_sourcefile_tenv : <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> <a href="../../IBase/SourceFile/index.html#type-t">IBase.SourceFile.t</a> <span>&#45;&gt;</span> <a href="../../IR/Tenv/index.html#type-t">IR.Tenv.t</a></code></dt><dd><p>return the type environment associated with the source file</p></dd></dl><dl><dt class="spec value" id="val-load_java_global_tenv"><a href="#val-load_java_global_tenv" class="anchor"></a><code><span class="keyword">val</span> load_java_global_tenv : <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> <a href="../../IR/Tenv/index.html#type-t">IR.Tenv.t</a></code></dt><dd><p>Load Java type environment (if not done yet), and return it. Useful for accessing type info not related to any concrete function.</p></dd></dl><dl><dt class="spec value" id="val-get_integer_type_widths"><a href="#val-get_integer_type_widths" class="anchor"></a><code><span class="keyword">val</span> get_integer_type_widths : <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> <a href="../../IR/Procname/index.html#type-t">IR.Procname.t</a> <span>&#45;&gt;</span> <a href="../../IR/Typ/IntegerWidths/index.html#type-t">IR.Typ.IntegerWidths.t</a></code></dt><dd><p>return the integer type widths associated with the procedure</p></dd></dl></div></body></html>

File diff suppressed because one or more lines are too long

@ -1,2 +1,2 @@
<!DOCTYPE html> <!DOCTYPE html>
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>Absint__Exe_env (infer.Absint__Exe_env)</title><link rel="stylesheet" href="../../odoc.css"/><meta charset="utf-8"/><meta name="generator" content="odoc 1.5.2"/><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__Exe_env</nav><h1>Module <code>Absint__Exe_env</code></h1></header><aside><p>Execution environments are a means to get a function's type environment and integer widths and cache those</p></aside><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-mk"><a href="#val-mk" class="anchor"></a><code><span class="keyword">val</span> mk : unit <span>&#45;&gt;</span> <a href="index.html#type-t">t</a></code></dt><dd><p>Create a new cache</p></dd></dl><dl><dt class="spec value" id="val-get_tenv"><a href="#val-get_tenv" class="anchor"></a><code><span class="keyword">val</span> get_tenv : <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> <a href="../IR/Procname/index.html#type-t">IR.Procname.t</a> <span>&#45;&gt;</span> <a href="../IR/Tenv/index.html#type-t">IR.Tenv.t</a></code></dt><dd><p>return the type environment associated with the procedure</p></dd></dl><dl><dt class="spec value" id="val-load_java_global_tenv"><a href="#val-load_java_global_tenv" class="anchor"></a><code><span class="keyword">val</span> load_java_global_tenv : <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> <a href="../IR/Tenv/index.html#type-t">IR.Tenv.t</a></code></dt><dd><p>Load Java type environment (if not done yet), and return it. Useful for accessing type info not related to any concrete function.</p></dd></dl><dl><dt class="spec value" id="val-get_integer_type_widths"><a href="#val-get_integer_type_widths" class="anchor"></a><code><span class="keyword">val</span> get_integer_type_widths : <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> <a href="../IR/Procname/index.html#type-t">IR.Procname.t</a> <span>&#45;&gt;</span> <a href="../IR/Typ/IntegerWidths/index.html#type-t">IR.Typ.IntegerWidths.t</a></code></dt><dd><p>return the integer type widths associated with the procedure</p></dd></dl></div></body></html> <html xmlns="http://www.w3.org/1999/xhtml"><head><title>Absint__Exe_env (infer.Absint__Exe_env)</title><link rel="stylesheet" href="../../odoc.css"/><meta charset="utf-8"/><meta name="generator" content="odoc 1.5.2"/><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__Exe_env</nav><h1>Module <code>Absint__Exe_env</code></h1></header><aside><p>Execution environments are a means to get a function's type environment and integer widths and cache those</p></aside><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-mk"><a href="#val-mk" class="anchor"></a><code><span class="keyword">val</span> mk : unit <span>&#45;&gt;</span> <a href="index.html#type-t">t</a></code></dt><dd><p>Create a new cache</p></dd></dl><dl><dt class="spec value" id="val-get_proc_tenv"><a href="#val-get_proc_tenv" class="anchor"></a><code><span class="keyword">val</span> get_proc_tenv : <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> <a href="../IR/Procname/index.html#type-t">IR.Procname.t</a> <span>&#45;&gt;</span> <a href="../IR/Tenv/index.html#type-t">IR.Tenv.t</a></code></dt><dd><p>return the type environment associated with the procedure</p></dd></dl><dl><dt class="spec value" id="val-get_sourcefile_tenv"><a href="#val-get_sourcefile_tenv" class="anchor"></a><code><span class="keyword">val</span> get_sourcefile_tenv : <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> <a href="../IBase/SourceFile/index.html#type-t">IBase.SourceFile.t</a> <span>&#45;&gt;</span> <a href="../IR/Tenv/index.html#type-t">IR.Tenv.t</a></code></dt><dd><p>return the type environment associated with the source file</p></dd></dl><dl><dt class="spec value" id="val-load_java_global_tenv"><a href="#val-load_java_global_tenv" class="anchor"></a><code><span class="keyword">val</span> load_java_global_tenv : <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> <a href="../IR/Tenv/index.html#type-t">IR.Tenv.t</a></code></dt><dd><p>Load Java type environment (if not done yet), and return it. Useful for accessing type info not related to any concrete function.</p></dd></dl><dl><dt class="spec value" id="val-get_integer_type_widths"><a href="#val-get_integer_type_widths" class="anchor"></a><code><span class="keyword">val</span> get_integer_type_widths : <a href="index.html#type-t">t</a> <span>&#45;&gt;</span> <a href="../IR/Procname/index.html#type-t">IR.Procname.t</a> <span>&#45;&gt;</span> <a href="../IR/Typ/IntegerWidths/index.html#type-t">IR.Typ.IntegerWidths.t</a></code></dt><dd><p>return the integer type widths associated with the procedure</p></dd></dl></div></body></html>

File diff suppressed because one or more lines are too long

File diff suppressed because one or more lines are too long

File diff suppressed because one or more lines are too long

@ -1,2 +1,2 @@
<!DOCTYPE html> <!DOCTYPE html>
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>OnDisk (infer.Backend.Summary.OnDisk)</title><link rel="stylesheet" href="../../../../odoc.css"/><meta charset="utf-8"/><meta name="generator" content="odoc 1.5.2"/><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">Backend</a> &#x00BB; <a href="../index.html">Summary</a> &#x00BB; OnDisk</nav><h1>Module <code>Summary.OnDisk</code></h1></header><dl><dt class="spec value" id="val-clear_cache"><a href="#val-clear_cache" class="anchor"></a><code><span class="keyword">val</span> clear_cache : unit <span>&#45;&gt;</span> unit</code></dt><dd><p>Remove all the elements from the cache of summaries</p></dd></dl><dl><dt class="spec value" id="val-get"><a href="#val-get" class="anchor"></a><code><span class="keyword">val</span> get : <a href="../../../IR/Procname/index.html#type-t">IR.Procname.t</a> <span>&#45;&gt;</span> <span><a href="../index.html#type-t">t</a> option</span></code></dt><dd><p>Return the summary option for the procedure name</p></dd></dl><dl><dt class="spec value" id="val-reset"><a href="#val-reset" class="anchor"></a><code><span class="keyword">val</span> reset : <a href="../../../IR/Procdesc/index.html#type-t">IR.Procdesc.t</a> <span>&#45;&gt;</span> <a href="../index.html#type-t">t</a></code></dt><dd><p>Reset a summary rebuilding the dependents and preserving the proc attributes if present.</p></dd></dl><dl><dt class="spec value" id="val-proc_resolve_attributes"><a href="#val-proc_resolve_attributes" class="anchor"></a><code><span class="keyword">val</span> proc_resolve_attributes : <a href="../../../IR/Procname/index.html#type-t">IR.Procname.t</a> <span>&#45;&gt;</span> <span><a href="../../../IR/ProcAttributes/index.html#type-t">IR.ProcAttributes.t</a> option</span></code></dt><dd><p>Try to find the attributes for a defined proc. First look at specs (to get attributes computed by analysis) then look at the attributes table. If no attributes can be found, return None.</p></dd></dl><dl><dt class="spec value" id="val-store_analyzed"><a href="#val-store_analyzed" class="anchor"></a><code><span class="keyword">val</span> store_analyzed : <a href="../index.html#type-t">t</a> <span>&#45;&gt;</span> unit</code></dt><dd><p>Save summary for the procedure into the spec database</p></dd></dl><dl><dt class="spec value" id="val-reset_all"><a href="#val-reset_all" class="anchor"></a><code><span class="keyword">val</span> reset_all : <span>filter:<a href="../../../IR/Filtering/index.html#type-procedures_filter">IR.Filtering.procedures_filter</a></span> <span>&#45;&gt;</span> unit <span>&#45;&gt;</span> unit</code></dt><dt class="spec value" id="val-delete"><a href="#val-delete" class="anchor"></a><code><span class="keyword">val</span> delete : <a href="../../../IR/Procname/index.html#type-t">IR.Procname.t</a> <span>&#45;&gt;</span> unit</code></dt><dd><p>Delete the .specs file corresponding to the procname and remove its summary from the Summary cache</p></dd></dl><dl><dt class="spec value" id="val-iter_specs"><a href="#val-iter_specs" class="anchor"></a><code><span class="keyword">val</span> iter_specs : <span>f:<span>(<a href="../index.html#type-t">t</a> <span>&#45;&gt;</span> unit)</span></span> <span>&#45;&gt;</span> unit</code></dt><dd><p>Iterates over all stored summaries</p></dd></dl><dl><dt class="spec value" id="val-iter_report_summaries_from_config"><a href="#val-iter_report_summaries_from_config" class="anchor"></a><code><span class="keyword">val</span> iter_report_summaries_from_config : <span>f:<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><a href="../../../Costlib/CostDomain/index.html#type-summary">Costlib.CostDomain.summary</a> option</span> <span>&#45;&gt;</span> <a href="../../../Absint/Errlog/index.html#type-t">Absint.Errlog.t</a> <span>&#45;&gt;</span> unit)</span></span> <span>&#45;&gt;</span> unit</code></dt><dd><p>Iterates over all analysis artefacts listed above, for each procedure</p></dd></dl><dl><dt class="spec value" id="val-pp_specs_from_config"><a href="#val-pp_specs_from_config" class="anchor"></a><code><span class="keyword">val</span> pp_specs_from_config : Stdlib.Format.formatter <span>&#45;&gt;</span> unit</code></dt><dd><p>pretty print all stored summaries</p></dd></dl></div></body></html> <html xmlns="http://www.w3.org/1999/xhtml"><head><title>OnDisk (infer.Backend.Summary.OnDisk)</title><link rel="stylesheet" href="../../../../odoc.css"/><meta charset="utf-8"/><meta name="generator" content="odoc 1.5.2"/><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">Backend</a> &#x00BB; <a href="../index.html">Summary</a> &#x00BB; OnDisk</nav><h1>Module <code>Summary.OnDisk</code></h1></header><dl><dt class="spec value" id="val-clear_cache"><a href="#val-clear_cache" class="anchor"></a><code><span class="keyword">val</span> clear_cache : unit <span>&#45;&gt;</span> unit</code></dt><dd><p>Remove all the elements from the cache of summaries</p></dd></dl><dl><dt class="spec value" id="val-get"><a href="#val-get" class="anchor"></a><code><span class="keyword">val</span> get : <a href="../../../IR/Procname/index.html#type-t">IR.Procname.t</a> <span>&#45;&gt;</span> <span><a href="../index.html#type-t">t</a> option</span></code></dt><dd><p>Return the summary option for the procedure name</p></dd></dl><dl><dt class="spec value" id="val-reset"><a href="#val-reset" class="anchor"></a><code><span class="keyword">val</span> reset : <a href="../../../IR/Procdesc/index.html#type-t">IR.Procdesc.t</a> <span>&#45;&gt;</span> <a href="../index.html#type-t">t</a></code></dt><dd><p>Reset a summary rebuilding the dependents and preserving the proc attributes if present.</p></dd></dl><dl><dt class="spec value" id="val-proc_resolve_attributes"><a href="#val-proc_resolve_attributes" class="anchor"></a><code><span class="keyword">val</span> proc_resolve_attributes : <a href="../../../IR/Procname/index.html#type-t">IR.Procname.t</a> <span>&#45;&gt;</span> <span><a href="../../../IR/ProcAttributes/index.html#type-t">IR.ProcAttributes.t</a> option</span></code></dt><dd><p>Try to find the attributes for a defined proc. First look at specs (to get attributes computed by analysis) then look at the attributes table. If no attributes can be found, return None.</p></dd></dl><dl><dt class="spec value" id="val-store_analyzed"><a href="#val-store_analyzed" class="anchor"></a><code><span class="keyword">val</span> store_analyzed : <a href="../index.html#type-t">t</a> <span>&#45;&gt;</span> unit</code></dt><dd><p>Save summary for the procedure into the spec database</p></dd></dl><dl><dt class="spec value" id="val-reset_all"><a href="#val-reset_all" class="anchor"></a><code><span class="keyword">val</span> reset_all : <span>filter:<a href="../../../IR/Filtering/index.html#type-procedures_filter">IR.Filtering.procedures_filter</a></span> <span>&#45;&gt;</span> unit <span>&#45;&gt;</span> unit</code></dt><dt class="spec value" id="val-delete"><a href="#val-delete" class="anchor"></a><code><span class="keyword">val</span> delete : <a href="../../../IR/Procname/index.html#type-t">IR.Procname.t</a> <span>&#45;&gt;</span> unit</code></dt><dd><p>Delete the .specs file corresponding to the procname and remove its summary from the Summary cache</p></dd></dl><dl><dt class="spec value" id="val-iter_specs"><a href="#val-iter_specs" class="anchor"></a><code><span class="keyword">val</span> iter_specs : <span>f:<span>(<a href="../index.html#type-t">t</a> <span>&#45;&gt;</span> unit)</span></span> <span>&#45;&gt;</span> unit</code></dt><dd><p>Iterates over all stored summaries</p></dd></dl><dl><dt class="spec value" id="val-iter_report_summaries_from_config"><a href="#val-iter_report_summaries_from_config" class="anchor"></a><code><span class="keyword">val</span> iter_report_summaries_from_config : <span>f:<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><a href="../../../Costlib/CostDomain/index.html#type-summary">Costlib.CostDomain.summary</a> option</span> <span>&#45;&gt;</span> <span><a href="../../../Checkers/ConfigImpactAnalysis/Summary/index.html#type-t">Checkers.ConfigImpactAnalysis.Summary.t</a> option</span> <span>&#45;&gt;</span> <a href="../../../Absint/Errlog/index.html#type-t">Absint.Errlog.t</a> <span>&#45;&gt;</span> unit)</span></span> <span>&#45;&gt;</span> unit</code></dt><dd><p>Iterates over all analysis artefacts listed above, for each procedure</p></dd></dl><dl><dt class="spec value" id="val-pp_specs_from_config"><a href="#val-pp_specs_from_config" class="anchor"></a><code><span class="keyword">val</span> pp_specs_from_config : Stdlib.Format.formatter <span>&#45;&gt;</span> unit</code></dt><dd><p>pretty print all stored summaries</p></dd></dl></div></body></html>

File diff suppressed because one or more lines are too long

File diff suppressed because one or more lines are too long

File diff suppressed because one or more lines are too long

@ -1,2 +1,2 @@
<!DOCTYPE html> <!DOCTYPE html>
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>OnDisk (infer.Backend__Summary.OnDisk)</title><link rel="stylesheet" href="../../../odoc.css"/><meta charset="utf-8"/><meta name="generator" content="odoc 1.5.2"/><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">Backend__Summary</a> &#x00BB; OnDisk</nav><h1>Module <code>Backend__Summary.OnDisk</code></h1></header><dl><dt class="spec value" id="val-clear_cache"><a href="#val-clear_cache" class="anchor"></a><code><span class="keyword">val</span> clear_cache : unit <span>&#45;&gt;</span> unit</code></dt><dd><p>Remove all the elements from the cache of summaries</p></dd></dl><dl><dt class="spec value" id="val-get"><a href="#val-get" class="anchor"></a><code><span class="keyword">val</span> get : <a href="../../IR/Procname/index.html#type-t">IR.Procname.t</a> <span>&#45;&gt;</span> <span><a href="../index.html#type-t">t</a> option</span></code></dt><dd><p>Return the summary option for the procedure name</p></dd></dl><dl><dt class="spec value" id="val-reset"><a href="#val-reset" class="anchor"></a><code><span class="keyword">val</span> reset : <a href="../../IR/Procdesc/index.html#type-t">IR.Procdesc.t</a> <span>&#45;&gt;</span> <a href="../index.html#type-t">t</a></code></dt><dd><p>Reset a summary rebuilding the dependents and preserving the proc attributes if present.</p></dd></dl><dl><dt class="spec value" id="val-proc_resolve_attributes"><a href="#val-proc_resolve_attributes" class="anchor"></a><code><span class="keyword">val</span> proc_resolve_attributes : <a href="../../IR/Procname/index.html#type-t">IR.Procname.t</a> <span>&#45;&gt;</span> <span><a href="../../IR/ProcAttributes/index.html#type-t">IR.ProcAttributes.t</a> option</span></code></dt><dd><p>Try to find the attributes for a defined proc. First look at specs (to get attributes computed by analysis) then look at the attributes table. If no attributes can be found, return None.</p></dd></dl><dl><dt class="spec value" id="val-store_analyzed"><a href="#val-store_analyzed" class="anchor"></a><code><span class="keyword">val</span> store_analyzed : <a href="../index.html#type-t">t</a> <span>&#45;&gt;</span> unit</code></dt><dd><p>Save summary for the procedure into the spec database</p></dd></dl><dl><dt class="spec value" id="val-reset_all"><a href="#val-reset_all" class="anchor"></a><code><span class="keyword">val</span> reset_all : <span>filter:<a href="../../IR/Filtering/index.html#type-procedures_filter">IR.Filtering.procedures_filter</a></span> <span>&#45;&gt;</span> unit <span>&#45;&gt;</span> unit</code></dt><dt class="spec value" id="val-delete"><a href="#val-delete" class="anchor"></a><code><span class="keyword">val</span> delete : <a href="../../IR/Procname/index.html#type-t">IR.Procname.t</a> <span>&#45;&gt;</span> unit</code></dt><dd><p>Delete the .specs file corresponding to the procname and remove its summary from the Summary cache</p></dd></dl><dl><dt class="spec value" id="val-iter_specs"><a href="#val-iter_specs" class="anchor"></a><code><span class="keyword">val</span> iter_specs : <span>f:<span>(<a href="../index.html#type-t">t</a> <span>&#45;&gt;</span> unit)</span></span> <span>&#45;&gt;</span> unit</code></dt><dd><p>Iterates over all stored summaries</p></dd></dl><dl><dt class="spec value" id="val-iter_report_summaries_from_config"><a href="#val-iter_report_summaries_from_config" class="anchor"></a><code><span class="keyword">val</span> iter_report_summaries_from_config : <span>f:<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><a href="../../Costlib/CostDomain/index.html#type-summary">Costlib.CostDomain.summary</a> option</span> <span>&#45;&gt;</span> <a href="../../Absint/Errlog/index.html#type-t">Absint.Errlog.t</a> <span>&#45;&gt;</span> unit)</span></span> <span>&#45;&gt;</span> unit</code></dt><dd><p>Iterates over all analysis artefacts listed above, for each procedure</p></dd></dl><dl><dt class="spec value" id="val-pp_specs_from_config"><a href="#val-pp_specs_from_config" class="anchor"></a><code><span class="keyword">val</span> pp_specs_from_config : Stdlib.Format.formatter <span>&#45;&gt;</span> unit</code></dt><dd><p>pretty print all stored summaries</p></dd></dl></div></body></html> <html xmlns="http://www.w3.org/1999/xhtml"><head><title>OnDisk (infer.Backend__Summary.OnDisk)</title><link rel="stylesheet" href="../../../odoc.css"/><meta charset="utf-8"/><meta name="generator" content="odoc 1.5.2"/><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">Backend__Summary</a> &#x00BB; OnDisk</nav><h1>Module <code>Backend__Summary.OnDisk</code></h1></header><dl><dt class="spec value" id="val-clear_cache"><a href="#val-clear_cache" class="anchor"></a><code><span class="keyword">val</span> clear_cache : unit <span>&#45;&gt;</span> unit</code></dt><dd><p>Remove all the elements from the cache of summaries</p></dd></dl><dl><dt class="spec value" id="val-get"><a href="#val-get" class="anchor"></a><code><span class="keyword">val</span> get : <a href="../../IR/Procname/index.html#type-t">IR.Procname.t</a> <span>&#45;&gt;</span> <span><a href="../index.html#type-t">t</a> option</span></code></dt><dd><p>Return the summary option for the procedure name</p></dd></dl><dl><dt class="spec value" id="val-reset"><a href="#val-reset" class="anchor"></a><code><span class="keyword">val</span> reset : <a href="../../IR/Procdesc/index.html#type-t">IR.Procdesc.t</a> <span>&#45;&gt;</span> <a href="../index.html#type-t">t</a></code></dt><dd><p>Reset a summary rebuilding the dependents and preserving the proc attributes if present.</p></dd></dl><dl><dt class="spec value" id="val-proc_resolve_attributes"><a href="#val-proc_resolve_attributes" class="anchor"></a><code><span class="keyword">val</span> proc_resolve_attributes : <a href="../../IR/Procname/index.html#type-t">IR.Procname.t</a> <span>&#45;&gt;</span> <span><a href="../../IR/ProcAttributes/index.html#type-t">IR.ProcAttributes.t</a> option</span></code></dt><dd><p>Try to find the attributes for a defined proc. First look at specs (to get attributes computed by analysis) then look at the attributes table. If no attributes can be found, return None.</p></dd></dl><dl><dt class="spec value" id="val-store_analyzed"><a href="#val-store_analyzed" class="anchor"></a><code><span class="keyword">val</span> store_analyzed : <a href="../index.html#type-t">t</a> <span>&#45;&gt;</span> unit</code></dt><dd><p>Save summary for the procedure into the spec database</p></dd></dl><dl><dt class="spec value" id="val-reset_all"><a href="#val-reset_all" class="anchor"></a><code><span class="keyword">val</span> reset_all : <span>filter:<a href="../../IR/Filtering/index.html#type-procedures_filter">IR.Filtering.procedures_filter</a></span> <span>&#45;&gt;</span> unit <span>&#45;&gt;</span> unit</code></dt><dt class="spec value" id="val-delete"><a href="#val-delete" class="anchor"></a><code><span class="keyword">val</span> delete : <a href="../../IR/Procname/index.html#type-t">IR.Procname.t</a> <span>&#45;&gt;</span> unit</code></dt><dd><p>Delete the .specs file corresponding to the procname and remove its summary from the Summary cache</p></dd></dl><dl><dt class="spec value" id="val-iter_specs"><a href="#val-iter_specs" class="anchor"></a><code><span class="keyword">val</span> iter_specs : <span>f:<span>(<a href="../index.html#type-t">t</a> <span>&#45;&gt;</span> unit)</span></span> <span>&#45;&gt;</span> unit</code></dt><dd><p>Iterates over all stored summaries</p></dd></dl><dl><dt class="spec value" id="val-iter_report_summaries_from_config"><a href="#val-iter_report_summaries_from_config" class="anchor"></a><code><span class="keyword">val</span> iter_report_summaries_from_config : <span>f:<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><a href="../../Costlib/CostDomain/index.html#type-summary">Costlib.CostDomain.summary</a> option</span> <span>&#45;&gt;</span> <span><a href="../../Checkers/ConfigImpactAnalysis/Summary/index.html#type-t">Checkers.ConfigImpactAnalysis.Summary.t</a> option</span> <span>&#45;&gt;</span> <a href="../../Absint/Errlog/index.html#type-t">Absint.Errlog.t</a> <span>&#45;&gt;</span> unit)</span></span> <span>&#45;&gt;</span> unit</code></dt><dd><p>Iterates over all analysis artefacts listed above, for each procedure</p></dd></dl><dl><dt class="spec value" id="val-pp_specs_from_config"><a href="#val-pp_specs_from_config" class="anchor"></a><code><span class="keyword">val</span> pp_specs_from_config : Stdlib.Format.formatter <span>&#45;&gt;</span> unit</code></dt><dd><p>pretty print all stored summaries</p></dd></dl></div></body></html>

File diff suppressed because one or more lines are too long

File diff suppressed because one or more lines are too long

File diff suppressed because one or more lines are too long

File diff suppressed because one or more lines are too long

File diff suppressed because one or more lines are too long

File diff suppressed because one or more lines are too long

File diff suppressed because one or more lines are too long

File diff suppressed because one or more lines are too long

File diff suppressed because one or more lines are too long

File diff suppressed because one or more lines are too long

File diff suppressed because one or more lines are too long

File diff suppressed because one or more lines are too long

File diff suppressed because one or more lines are too long

File diff suppressed because one or more lines are too long

File diff suppressed because one or more lines are too long

File diff suppressed because one or more lines are too long

File diff suppressed because one or more lines are too long

File diff suppressed because one or more lines are too long

File diff suppressed because one or more lines are too long

File diff suppressed because one or more lines are too long

File diff suppressed because one or more lines are too long

File diff suppressed because one or more lines are too long

File diff suppressed because one or more lines are too long

File diff suppressed because one or more lines are too long

File diff suppressed because one or more lines are too long

@ -1,2 +1,2 @@
<!DOCTYPE html> <!DOCTYPE html>
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>JsonReports (infer.Integration.JsonReports)</title><link rel="stylesheet" href="../../../odoc.css"/><meta charset="utf-8"/><meta name="generator" content="odoc 1.5.2"/><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">Integration</a> &#x00BB; JsonReports</nav><h1>Module <code>Integration.JsonReports</code></h1></header><dl><dt class="spec value" id="val-potential_exception_message"><a href="#val-potential_exception_message" class="anchor"></a><code><span class="keyword">val</span> potential_exception_message : string</code></dt><dt class="spec value" id="val-loc_trace_to_jsonbug_record"><a href="#val-loc_trace_to_jsonbug_record" class="anchor"></a><code><span class="keyword">val</span> loc_trace_to_jsonbug_record : <span><a href="../../Absint/Errlog/index.html#type-loc_trace_elem">Absint.Errlog.loc_trace_elem</a> list</span> <span>&#45;&gt;</span> <a href="../../IBase/IssueType/index.html#type-severity">IBase.IssueType.severity</a> <span>&#45;&gt;</span> <span><a href="../../ATDGenerated/Jsonbug_t/index.html#type-json_trace_item">ATDGenerated.Jsonbug_t.json_trace_item</a> list</span></code></dt><dt class="spec value" id="val-censored_reason"><a href="#val-censored_reason" class="anchor"></a><code><span class="keyword">val</span> censored_reason : <a href="../../IBase/IssueType/index.html#type-t">IBase.IssueType.t</a> <span>&#45;&gt;</span> <a href="../../IBase/SourceFile/index.html#type-t">IBase.SourceFile.t</a> <span>&#45;&gt;</span> <span>string option</span></code></dt><dt class="spec value" id="val-write_reports"><a href="#val-write_reports" class="anchor"></a><code><span class="keyword">val</span> write_reports : <span>issues_json:string</span> <span>&#45;&gt;</span> <span>costs_json:string</span> <span>&#45;&gt;</span> unit</code></dt></dl></div></body></html> <html xmlns="http://www.w3.org/1999/xhtml"><head><title>JsonReports (infer.Integration.JsonReports)</title><link rel="stylesheet" href="../../../odoc.css"/><meta charset="utf-8"/><meta name="generator" content="odoc 1.5.2"/><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">Integration</a> &#x00BB; JsonReports</nav><h1>Module <code>Integration.JsonReports</code></h1></header><dl><dt class="spec value" id="val-potential_exception_message"><a href="#val-potential_exception_message" class="anchor"></a><code><span class="keyword">val</span> potential_exception_message : string</code></dt><dt class="spec value" id="val-loc_trace_to_jsonbug_record"><a href="#val-loc_trace_to_jsonbug_record" class="anchor"></a><code><span class="keyword">val</span> loc_trace_to_jsonbug_record : <span><a href="../../Absint/Errlog/index.html#type-loc_trace_elem">Absint.Errlog.loc_trace_elem</a> list</span> <span>&#45;&gt;</span> <a href="../../IBase/IssueType/index.html#type-severity">IBase.IssueType.severity</a> <span>&#45;&gt;</span> <span><a href="../../ATDGenerated/Jsonbug_t/index.html#type-json_trace_item">ATDGenerated.Jsonbug_t.json_trace_item</a> list</span></code></dt><dt class="spec value" id="val-censored_reason"><a href="#val-censored_reason" class="anchor"></a><code><span class="keyword">val</span> censored_reason : <a href="../../IBase/IssueType/index.html#type-t">IBase.IssueType.t</a> <span>&#45;&gt;</span> <a href="../../IBase/SourceFile/index.html#type-t">IBase.SourceFile.t</a> <span>&#45;&gt;</span> <span>string option</span></code></dt><dt class="spec value" id="val-write_reports"><a href="#val-write_reports" class="anchor"></a><code><span class="keyword">val</span> write_reports : <span>issues_json:string</span> <span>&#45;&gt;</span> <span>costs_json:string</span> <span>&#45;&gt;</span> <span>config_impact_json:string</span> <span>&#45;&gt;</span> unit</code></dt></dl></div></body></html>

@ -1,2 +1,2 @@
<!DOCTYPE html> <!DOCTYPE html>
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>Integration__JsonReports (infer.Integration__JsonReports)</title><link rel="stylesheet" href="../../odoc.css"/><meta charset="utf-8"/><meta name="generator" content="odoc 1.5.2"/><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; Integration__JsonReports</nav><h1>Module <code>Integration__JsonReports</code></h1></header><dl><dt class="spec value" id="val-potential_exception_message"><a href="#val-potential_exception_message" class="anchor"></a><code><span class="keyword">val</span> potential_exception_message : string</code></dt><dt class="spec value" id="val-loc_trace_to_jsonbug_record"><a href="#val-loc_trace_to_jsonbug_record" class="anchor"></a><code><span class="keyword">val</span> loc_trace_to_jsonbug_record : <span><a href="../Absint/Errlog/index.html#type-loc_trace_elem">Absint.Errlog.loc_trace_elem</a> list</span> <span>&#45;&gt;</span> <a href="../IBase/IssueType/index.html#type-severity">IBase.IssueType.severity</a> <span>&#45;&gt;</span> <span><a href="../ATDGenerated/Jsonbug_t/index.html#type-json_trace_item">ATDGenerated.Jsonbug_t.json_trace_item</a> list</span></code></dt><dt class="spec value" id="val-censored_reason"><a href="#val-censored_reason" class="anchor"></a><code><span class="keyword">val</span> censored_reason : <a href="../IBase/IssueType/index.html#type-t">IBase.IssueType.t</a> <span>&#45;&gt;</span> <a href="../IBase/SourceFile/index.html#type-t">IBase.SourceFile.t</a> <span>&#45;&gt;</span> <span>string option</span></code></dt><dt class="spec value" id="val-write_reports"><a href="#val-write_reports" class="anchor"></a><code><span class="keyword">val</span> write_reports : <span>issues_json:string</span> <span>&#45;&gt;</span> <span>costs_json:string</span> <span>&#45;&gt;</span> unit</code></dt></dl></div></body></html> <html xmlns="http://www.w3.org/1999/xhtml"><head><title>Integration__JsonReports (infer.Integration__JsonReports)</title><link rel="stylesheet" href="../../odoc.css"/><meta charset="utf-8"/><meta name="generator" content="odoc 1.5.2"/><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; Integration__JsonReports</nav><h1>Module <code>Integration__JsonReports</code></h1></header><dl><dt class="spec value" id="val-potential_exception_message"><a href="#val-potential_exception_message" class="anchor"></a><code><span class="keyword">val</span> potential_exception_message : string</code></dt><dt class="spec value" id="val-loc_trace_to_jsonbug_record"><a href="#val-loc_trace_to_jsonbug_record" class="anchor"></a><code><span class="keyword">val</span> loc_trace_to_jsonbug_record : <span><a href="../Absint/Errlog/index.html#type-loc_trace_elem">Absint.Errlog.loc_trace_elem</a> list</span> <span>&#45;&gt;</span> <a href="../IBase/IssueType/index.html#type-severity">IBase.IssueType.severity</a> <span>&#45;&gt;</span> <span><a href="../ATDGenerated/Jsonbug_t/index.html#type-json_trace_item">ATDGenerated.Jsonbug_t.json_trace_item</a> list</span></code></dt><dt class="spec value" id="val-censored_reason"><a href="#val-censored_reason" class="anchor"></a><code><span class="keyword">val</span> censored_reason : <a href="../IBase/IssueType/index.html#type-t">IBase.IssueType.t</a> <span>&#45;&gt;</span> <a href="../IBase/SourceFile/index.html#type-t">IBase.SourceFile.t</a> <span>&#45;&gt;</span> <span>string option</span></code></dt><dt class="spec value" id="val-write_reports"><a href="#val-write_reports" class="anchor"></a><code><span class="keyword">val</span> write_reports : <span>issues_json:string</span> <span>&#45;&gt;</span> <span>costs_json:string</span> <span>&#45;&gt;</span> <span>config_impact_json:string</span> <span>&#45;&gt;</span> unit</code></dt></dl></div></body></html>

@ -1,2 +1,2 @@
<!DOCTYPE html> <!DOCTYPE html>
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>PostDomain (infer.Pulselib.PulseAbductiveDomain.PostDomain)</title><link rel="stylesheet" href="../../../../odoc.css"/><meta charset="utf-8"/><meta name="generator" content="odoc 1.5.2"/><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; PostDomain</nav><h1>Module <code>PulseAbductiveDomain.PostDomain</code></h1><p>The post abstract state at each program point, or current state.</p></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> = <span class="keyword">private</span> <a href="../../PulseBaseDomain/index.html#type-t">BaseDomain.t</a></code></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-equal"><a href="#val-equal" class="anchor"></a><code><span class="keyword">val</span> equal : <a href="index.html#type-t">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-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-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> Yojson.Safe.t</code></dt><dt class="spec value" id="val-empty"><a href="#val-empty" class="anchor"></a><code><span class="keyword">val</span> empty : <a href="index.html#type-t">t</a></code></dt><dt class="spec value" id="val-update"><a href="#val-update" class="anchor"></a><code><span class="keyword">val</span> update : <span>?&#8288;stack:<a href="../../PulseBaseStack/index.html#type-t">BaseStack.t</a></span> <span>&#45;&gt;</span> <span>?&#8288;heap:<a href="../../PulseBaseMemory/index.html#type-t">BaseMemory.t</a></span> <span>&#45;&gt;</span> <span>?&#8288;attrs:<a href="../../PulseBaseAddressAttributes/index.html#type-t">BaseAddressAttributes.t</a></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-filter_addr"><a href="#val-filter_addr" class="anchor"></a><code><span class="keyword">val</span> filter_addr : <span>f:<span>(<a href="../../PulseAbstractValue/index.html#type-t">PulseBasicInterface.AbstractValue.t</a> <span>&#45;&gt;</span> bool)</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>filter both heap and attrs</p></dd></dl><dl><dt class="spec value" id="val-filter_addr_with_discarded_addrs"><a href="#val-filter_addr_with_discarded_addrs" class="anchor"></a><code><span class="keyword">val</span> filter_addr_with_discarded_addrs : <span>f:<span>(<a href="../../PulseAbstractValue/index.html#type-t">PulseBasicInterface.AbstractValue.t</a> <span>&#45;&gt;</span> bool)</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> * <span><a href="../../PulseAbstractValue/index.html#type-t">PulseBasicInterface.AbstractValue.t</a> list</span></code></dt><dd><p>compute new state containing only reachable addresses in its heap and attributes, as well as the list of discarded unreachable addresses</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> <html xmlns="http://www.w3.org/1999/xhtml"><head><title>PostDomain (infer.Pulselib.PulseAbductiveDomain.PostDomain)</title><link rel="stylesheet" href="../../../../odoc.css"/><meta charset="utf-8"/><meta name="generator" content="odoc 1.5.2"/><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; PostDomain</nav><h1>Module <code>PulseAbductiveDomain.PostDomain</code></h1><p>The post abstract state at each program point, or current state.</p></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> = <span class="keyword">private</span> <a href="../../PulseBaseDomain/index.html#type-t">BaseDomain.t</a></code></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-equal"><a href="#val-equal" class="anchor"></a><code><span class="keyword">val</span> equal : <a href="index.html#type-t">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-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-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> Yojson.Safe.t</code></dt><dt class="spec value" id="val-empty"><a href="#val-empty" class="anchor"></a><code><span class="keyword">val</span> empty : <a href="index.html#type-t">t</a></code></dt><dt class="spec value" id="val-update"><a href="#val-update" class="anchor"></a><code><span class="keyword">val</span> update : <span>?&#8288;stack:<a href="../../PulseBaseStack/index.html#type-t">BaseStack.t</a></span> <span>&#45;&gt;</span> <span>?&#8288;heap:<a href="../../PulseBaseMemory/index.html#type-t">BaseMemory.t</a></span> <span>&#45;&gt;</span> <span>?&#8288;attrs:<a href="../../PulseBaseAddressAttributes/index.html#type-t">BaseAddressAttributes.t</a></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-filter_addr"><a href="#val-filter_addr" class="anchor"></a><code><span class="keyword">val</span> filter_addr : <span>f:<span>(<a href="../../PulseAbstractValue/index.html#type-t">PulseBasicInterface.AbstractValue.t</a> <span>&#45;&gt;</span> bool)</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>filter both heap and attrs</p></dd></dl><dl><dt class="spec value" id="val-filter_addr_with_discarded_addrs"><a href="#val-filter_addr_with_discarded_addrs" class="anchor"></a><code><span class="keyword">val</span> filter_addr_with_discarded_addrs : <span>f:<span>(<a href="../../PulseAbstractValue/index.html#type-t">PulseBasicInterface.AbstractValue.t</a> <span>&#45;&gt;</span> bool)</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> * <span><a href="../../PulseAbstractValue/index.html#type-t">PulseBasicInterface.AbstractValue.t</a> list</span></code></dt><dd><p>compute new state containing only reachable addresses in its heap and attributes, as well as the list of discarded unreachable addresses</p></dd></dl><dl><dt class="spec value" id="val-subst_var"><a href="#val-subst_var" class="anchor"></a><code><span class="keyword">val</span> subst_var : <span>(<a href="../../PulseAbstractValue/index.html#type-t">PulseBasicInterface.AbstractValue.t</a> * <a href="../../PulseAbstractValue/index.html#type-t">PulseBasicInterface.AbstractValue.t</a>)</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="../../PulseSatUnsat/index.html#type-t">PulseBasicInterface.SatUnsat.t</a></span></code></dt><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>

File diff suppressed because one or more lines are too long

File diff suppressed because one or more lines are too long

File diff suppressed because one or more lines are too long

File diff suppressed because one or more lines are too long

File diff suppressed because one or more lines are too long

File diff suppressed because one or more lines are too long

File diff suppressed because one or more lines are too long

File diff suppressed because one or more lines are too long

@ -1,2 +1,2 @@
<!DOCTYPE html> <!DOCTYPE html>
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>PulseReport (infer.Pulselib.PulseReport)</title><link rel="stylesheet" href="../../../odoc.css"/><meta charset="utf-8"/><meta name="generator" content="odoc 1.5.2"/><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; PulseReport</nav><h1>Module <code>Pulselib.PulseReport</code></h1></header><dl><dt class="spec type" id="type-access_result"><a href="#type-access_result" class="anchor"></a><code><span class="keyword">type</span> <span>'a access_result</span></code><code> = <span><span>(<span class="type-var">'a</span>, <a href="../PulseDiagnostic/index.html#type-t">PulseBasicInterface.Diagnostic.t</a> * <a href="../PulseAbductiveDomain/index.html#type-t">PulseDomainInterface.AbductiveDomain.t</a>)</span> <a href="../../IStdlib/index.html#module-IStd">IStdlib.IStd</a>.result</span></code></dt></dl><dl><dt class="spec value" id="val-report_error"><a href="#val-report_error" class="anchor"></a><code><span class="keyword">val</span> report_error : <a href="../../IR/Procdesc/index.html#type-t">IR.Procdesc.t</a> <span>&#45;&gt;</span> <a href="../../IR/Tenv/index.html#type-t">IR.Tenv.t</a> <span>&#45;&gt;</span> <a href="../../Absint/Errlog/index.html#type-t">Absint.Errlog.t</a> <span>&#45;&gt;</span> <span><span class="type-var">'ok</span> <a href="index.html#type-access_result">access_result</a></span> <span>&#45;&gt;</span> <span><span>(<span class="type-var">'ok</span>, <span><span><span class="type-var">_</span> <a href="../PulseExecutionDomain/index.html#type-base_t">PulseDomainInterface.ExecutionDomain.base_t</a></span> <a href="../PulseSatUnsat/index.html#type-t">PulseBasicInterface.SatUnsat.t</a></span>)</span> <a href="../../IStdlib/index.html#module-IStd">IStdlib.IStd</a>.result</span></code></dt></dl></div></body></html> <html xmlns="http://www.w3.org/1999/xhtml"><head><title>PulseReport (infer.Pulselib.PulseReport)</title><link rel="stylesheet" href="../../../odoc.css"/><meta charset="utf-8"/><meta name="generator" content="odoc 1.5.2"/><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; PulseReport</nav><h1>Module <code>Pulselib.PulseReport</code></h1></header><dl><dt class="spec type" id="type-access_result"><a href="#type-access_result" class="anchor"></a><code><span class="keyword">type</span> <span>'a access_result</span></code><code> = <span><span>(<span class="type-var">'a</span>, <a href="../PulseDiagnostic/index.html#type-t">PulseBasicInterface.Diagnostic.t</a> * <a href="../PulseAbductiveDomain/index.html#type-t">PulseDomainInterface.AbductiveDomain.t</a>)</span> <a href="../../IStdlib/index.html#module-IStd">IStdlib.IStd</a>.result</span></code></dt></dl><dl><dt class="spec value" id="val-report_list_result"><a href="#val-report_list_result" class="anchor"></a><code><span class="keyword">val</span> report_list_result : <span><a href="../PulseSummary/index.html#type-t">PulseSummary.t</a> <a href="../../Absint/InterproceduralAnalysis/index.html#type-t">Absint.InterproceduralAnalysis.t</a></span> <span>&#45;&gt;</span> <span><span><a href="../PulseAbductiveDomain/index.html#type-t">PulseDomainInterface.AbductiveDomain.t</a> list</span> <a href="index.html#type-access_result">access_result</a></span> <span>&#45;&gt;</span> <span><a href="../PulseExecutionDomain/index.html#type-t">PulseDomainInterface.ExecutionDomain.t</a> list</span></code></dt><dt class="spec value" id="val-report_results"><a href="#val-report_results" class="anchor"></a><code><span class="keyword">val</span> report_results : <span><a href="../PulseSummary/index.html#type-t">PulseSummary.t</a> <a href="../../Absint/InterproceduralAnalysis/index.html#type-t">Absint.InterproceduralAnalysis.t</a></span> <span>&#45;&gt;</span> <span><span><a href="../PulseExecutionDomain/index.html#type-t">PulseDomainInterface.ExecutionDomain.t</a> <a href="index.html#type-access_result">access_result</a></span> list</span> <span>&#45;&gt;</span> <span><a href="../PulseExecutionDomain/index.html#type-t">PulseDomainInterface.ExecutionDomain.t</a> list</span></code></dt></dl></div></body></html>

File diff suppressed because one or more lines are too long

File diff suppressed because one or more lines are too long

File diff suppressed because one or more lines are too long

File diff suppressed because one or more lines are too long

File diff suppressed because one or more lines are too long

File diff suppressed because one or more lines are too long

File diff suppressed because one or more lines are too long

File diff suppressed because one or more lines are too long

File diff suppressed because one or more lines are too long

File diff suppressed because one or more lines are too long

File diff suppressed because one or more lines are too long

File diff suppressed because one or more lines are too long

@ -1,2 +1,2 @@
<!DOCTYPE html> <!DOCTYPE html>
<html xmlns="http://www.w3.org/1999/xhtml"><head><title>Pulselib__PulseReport (infer.Pulselib__PulseReport)</title><link rel="stylesheet" href="../../odoc.css"/><meta charset="utf-8"/><meta name="generator" content="odoc 1.5.2"/><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__PulseReport</nav><h1>Module <code>Pulselib__PulseReport</code></h1></header><dl><dt class="spec type" id="type-access_result"><a href="#type-access_result" class="anchor"></a><code><span class="keyword">type</span> <span>'a access_result</span></code><code> = <span><span>(<span class="type-var">'a</span>, <a href="../Pulselib/PulseDiagnostic/index.html#type-t">Pulselib.PulseBasicInterface.Diagnostic.t</a> * <a href="../Pulselib/PulseAbductiveDomain/index.html#type-t">Pulselib.PulseDomainInterface.AbductiveDomain.t</a>)</span> <a href="../IStdlib/index.html#module-IStd">IStdlib.IStd</a>.result</span></code></dt></dl><dl><dt class="spec value" id="val-report_error"><a href="#val-report_error" class="anchor"></a><code><span class="keyword">val</span> report_error : <a href="../IR/Procdesc/index.html#type-t">IR.Procdesc.t</a> <span>&#45;&gt;</span> <a href="../IR/Tenv/index.html#type-t">IR.Tenv.t</a> <span>&#45;&gt;</span> <a href="../Absint/Errlog/index.html#type-t">Absint.Errlog.t</a> <span>&#45;&gt;</span> <span><span class="type-var">'ok</span> <a href="index.html#type-access_result">access_result</a></span> <span>&#45;&gt;</span> <span><span>(<span class="type-var">'ok</span>, <span><span><span class="type-var">_</span> <a href="../Pulselib/PulseExecutionDomain/index.html#type-base_t">Pulselib.PulseDomainInterface.ExecutionDomain.base_t</a></span> <a href="../Pulselib/PulseSatUnsat/index.html#type-t">Pulselib.PulseBasicInterface.SatUnsat.t</a></span>)</span> <a href="../IStdlib/index.html#module-IStd">IStdlib.IStd</a>.result</span></code></dt></dl></div></body></html> <html xmlns="http://www.w3.org/1999/xhtml"><head><title>Pulselib__PulseReport (infer.Pulselib__PulseReport)</title><link rel="stylesheet" href="../../odoc.css"/><meta charset="utf-8"/><meta name="generator" content="odoc 1.5.2"/><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__PulseReport</nav><h1>Module <code>Pulselib__PulseReport</code></h1></header><dl><dt class="spec type" id="type-access_result"><a href="#type-access_result" class="anchor"></a><code><span class="keyword">type</span> <span>'a access_result</span></code><code> = <span><span>(<span class="type-var">'a</span>, <a href="../Pulselib/PulseDiagnostic/index.html#type-t">Pulselib.PulseBasicInterface.Diagnostic.t</a> * <a href="../Pulselib/PulseAbductiveDomain/index.html#type-t">Pulselib.PulseDomainInterface.AbductiveDomain.t</a>)</span> <a href="../IStdlib/index.html#module-IStd">IStdlib.IStd</a>.result</span></code></dt></dl><dl><dt class="spec value" id="val-report_list_result"><a href="#val-report_list_result" class="anchor"></a><code><span class="keyword">val</span> report_list_result : <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> <span>&#45;&gt;</span> <span><span><a href="../Pulselib/PulseAbductiveDomain/index.html#type-t">Pulselib.PulseDomainInterface.AbductiveDomain.t</a> list</span> <a href="index.html#type-access_result">access_result</a></span> <span>&#45;&gt;</span> <span><a href="../Pulselib/PulseExecutionDomain/index.html#type-t">Pulselib.PulseDomainInterface.ExecutionDomain.t</a> list</span></code></dt><dt class="spec value" id="val-report_results"><a href="#val-report_results" class="anchor"></a><code><span class="keyword">val</span> report_results : <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> <span>&#45;&gt;</span> <span><span><a href="../Pulselib/PulseExecutionDomain/index.html#type-t">Pulselib.PulseDomainInterface.ExecutionDomain.t</a> <a href="index.html#type-access_result">access_result</a></span> list</span> <span>&#45;&gt;</span> <span><a href="../Pulselib/PulseExecutionDomain/index.html#type-t">Pulselib.PulseDomainInterface.ExecutionDomain.t</a> list</span></code></dt></dl></div></body></html>

File diff suppressed because one or more lines are too long

File diff suppressed because one or more lines are too long
Loading…
Cancel
Save