From d65df3457f2ed84ff0e960ffb22237237bedb225 Mon Sep 17 00:00:00 2001
From: Jules Villard
Date: Wed, 24 Mar 2021 07:52:37 -0700
Subject: [PATCH] [website] make doc-publish
Summary: Reflect TOPL and command-line changes.
Reviewed By: skcho
Differential Revision: D27291246
fbshipit-source-id: cd5d30d0e
---
website/checkers.json | 2 +-
website/docs/all-issue-types.md | 9 +-
website/docs/checker-topl-pulse.md | 20 ---
...{checker-topl-biabd.md => checker-topl.md} | 4 +-
website/static/man/next/infer-analyze.1.html | 96 ++++++++------
website/static/man/next/infer-capture.1.html | 4 +-
website/static/man/next/infer-compile.1.html | 4 +-
website/static/man/next/infer-explore.1.html | 4 +-
website/static/man/next/infer-report.1.html | 14 +--
.../static/man/next/infer-reportdiff.1.html | 4 +-
website/static/man/next/infer-run.1.html | 11 +-
website/static/man/next/infer.1.html | 117 ++++++++++--------
.../infer/Absint/PatternMatch/Java/index.html | 2 +-
.../Absint__PatternMatch/Java/index.html | 2 +-
.../infer/Biabduction/Predicates/index.html | 2 +-
.../infer/Biabduction__Predicates/index.html | 2 +-
.../odoc/next/infer/IBase/Checker/index.html | 2 +-
.../odoc/next/infer/IBase/Config/index.html | 2 +-
.../next/infer/IBase/IssueType/index.html | 2 +-
.../odoc/next/infer/IBase__Checker/index.html | 2 +-
.../odoc/next/infer/IBase__Config/index.html | 2 +-
.../next/infer/IBase__IssueType/index.html | 2 +-
.../static/odoc/next/infer/IR/Exp/index.html | 2 +-
.../odoc/next/infer/IR/Mangled/index.html | 2 +-
.../odoc/next/infer/IR/Procdesc/index.html | 2 +-
.../static/odoc/next/infer/IR/Pvar/index.html | 2 +-
.../static/odoc/next/infer/IR__Exp/index.html | 2 +-
.../odoc/next/infer/IR__Mangled/index.html | 2 +-
.../odoc/next/infer/IR__Procdesc/index.html | 2 +-
.../odoc/next/infer/IR__Pvar/index.html | 2 +-
.../next/infer/Pulselib/PulseCItv/index.html | 2 +-
.../infer/Pulselib/PulseFormula/index.html | 2 +-
.../Pulselib/PulsePathCondition/index.html | 2 +-
.../Pulselib/PulseToplShallow/index.html | 2 -
.../odoc/next/infer/Pulselib/index.html | 2 +-
.../next/infer/Pulselib__PulseCItv/index.html | 2 +-
.../infer/Pulselib__PulseFormula/index.html | 2 +-
.../Pulselib__PulsePathCondition/index.html | 2 +-
.../Pulselib__PulseToplShallow/.dune-keep | 0
.../Pulselib__PulseToplShallow/index.html | 2 -
.../odoc/next/infer/TOPLlib/Topl/index.html | 2 +-
.../infer/TOPLlib/ToplAutomaton/index.html | 2 +-
.../next/infer/TOPLlib/ToplMonitor/index.html | 2 -
.../next/infer/TOPLlib/ToplName/index.html | 2 -
.../next/infer/TOPLlib/ToplUtils/index.html | 2 -
.../static/odoc/next/infer/TOPLlib/index.html | 2 +-
.../odoc/next/infer/TOPLlib__Topl/index.html | 2 +-
.../infer/TOPLlib__ToplAutomaton/index.html | 2 +-
.../infer/TOPLlib__ToplMonitor/.dune-keep | 0
.../infer/TOPLlib__ToplMonitor/index.html | 2 -
.../next/infer/TOPLlib__ToplName/.dune-keep | 0
.../next/infer/TOPLlib__ToplName/index.html | 2 -
.../next/infer/TOPLlib__ToplUtils/.dune-keep | 0
.../next/infer/TOPLlib__ToplUtils/index.html | 2 -
54 files changed, 166 insertions(+), 199 deletions(-)
delete mode 100644 website/docs/checker-topl-pulse.md
rename website/docs/{checker-topl-biabd.md => checker-topl.md} (80%)
delete mode 100644 website/static/odoc/next/infer/Pulselib/PulseToplShallow/index.html
delete mode 100644 website/static/odoc/next/infer/Pulselib__PulseToplShallow/.dune-keep
delete mode 100644 website/static/odoc/next/infer/Pulselib__PulseToplShallow/index.html
delete mode 100644 website/static/odoc/next/infer/TOPLlib/ToplMonitor/index.html
delete mode 100644 website/static/odoc/next/infer/TOPLlib/ToplName/index.html
delete mode 100644 website/static/odoc/next/infer/TOPLlib/ToplUtils/index.html
delete mode 100644 website/static/odoc/next/infer/TOPLlib__ToplMonitor/.dune-keep
delete mode 100644 website/static/odoc/next/infer/TOPLlib__ToplMonitor/index.html
delete mode 100644 website/static/odoc/next/infer/TOPLlib__ToplName/.dune-keep
delete mode 100644 website/static/odoc/next/infer/TOPLlib__ToplName/index.html
delete mode 100644 website/static/odoc/next/infer/TOPLlib__ToplUtils/.dune-keep
delete mode 100644 website/static/odoc/next/infer/TOPLlib__ToplUtils/index.html
diff --git a/website/checkers.json b/website/checkers.json
index f28546728..b9a4e532c 100644
--- a/website/checkers.json
+++ b/website/checkers.json
@@ -13,6 +13,6 @@
"checker-purity", "checker-quandary", "checker-racerd",
"checker-resource-leak-lab", "checker-dotnet-resource-leak",
"checker-siof", "checker-self-in-block", "checker-starvation",
- "checker-topl-biabd", "checker-topl-pulse", "checker-uninit"
+ "checker-topl", "checker-uninit"
]
}
\ No newline at end of file
diff --git a/website/docs/all-issue-types.md b/website/docs/all-issue-types.md
index 75a01863f..84e7b3262 100644
--- a/website/docs/all-issue-types.md
+++ b/website/docs/all-issue-types.md
@@ -2226,14 +2226,9 @@ These annotations can be found at `com.facebook.infer.annotation.*`.
other threads. The main utility of this annotation is in interfaces, where
Infer cannot look up the implementation and decide for itself.
-## TOPL_BIABD_ERROR
+## TOPL_ERROR
-Reported as "Topl Biabd Error" by [topl-biabd](/docs/next/checker-topl-biabd).
-
-Experimental.
-## TOPL_PULSE_ERROR
-
-Reported as "Topl Pulse Error" by [topl-pulse](/docs/next/checker-topl-pulse).
+Reported as "Topl Error" by [topl](/docs/next/checker-topl).
Experimental.
## UNINITIALIZED_VALUE
diff --git a/website/docs/checker-topl-pulse.md b/website/docs/checker-topl-pulse.md
deleted file mode 100644
index bf10a8e5d..000000000
--- a/website/docs/checker-topl-pulse.md
+++ /dev/null
@@ -1,20 +0,0 @@
----
-title: "TOPL"
-description: "Detects errors based on user-provided state machines describing multi-object monitors."
----
-
-Detects errors based on user-provided state machines describing multi-object monitors.
-
-Activate with `--topl-pulse`.
-
-Supported languages:
-- C/C++/ObjC: Experimental
-- Java: Experimental
-- C#/.Net: Experimental
-
-
-
-## List of Issue Types
-
-The following issue types are reported by this checker:
-- [TOPL_PULSE_ERROR](/docs/next/all-issue-types#topl_pulse_error)
diff --git a/website/docs/checker-topl-biabd.md b/website/docs/checker-topl.md
similarity index 80%
rename from website/docs/checker-topl-biabd.md
rename to website/docs/checker-topl.md
index b3ba0f669..2a3d62a2c 100644
--- a/website/docs/checker-topl-biabd.md
+++ b/website/docs/checker-topl.md
@@ -5,7 +5,7 @@ description: "Detects errors based on user-provided state machines describing mu
Detects errors based on user-provided state machines describing multi-object monitors.
-Activate with `--topl-biabd`.
+Activate with `--topl`.
Supported languages:
- C/C++/ObjC: Experimental
@@ -17,4 +17,4 @@ Supported languages:
## List of Issue Types
The following issue types are reported by this checker:
-- [TOPL_BIABD_ERROR](/docs/next/all-issue-types#topl_biabd_error)
+- [TOPL_ERROR](/docs/next/all-issue-types#topl_error)
diff --git a/website/static/man/next/infer-analyze.1.html b/website/static/man/next/infer-analyze.1.html
index 42737bf65..3059ff096 100644
--- a/website/static/man/next/infer-analyze.1.html
+++ b/website/static/man/next/infer-analyze.1.html
@@ -101,6 +101,13 @@ many linked to memory safety. (Conversely:
and disable all other checkers (Conversely:
--no-biabduction-only )
+
+--biabduction-write-dotty
+
+Activates: Produce dotty files
+for specs and retain cycles reports in infer-out/captured.
+(Conversely: --no-biabduction-write-dotty )
+
--bufferoverrun
Activates: checker
@@ -196,8 +203,8 @@ sets --debug-level 2 , --developer-mode ,
--print-buckets , --print-types ,
--reports-include-ml-loc ,
--no-only-cheap-debug , --trace-error ,
---write-dotty , --write-html ) (Conversely:
---no-debug | -G )
+--write-html ) (Conversely: --no-debug |
+-G )
--debug-level
level
@@ -321,6 +328,13 @@ disable all other checkers (Conversely:
--no-impurity-only )
+--impurity-report-immutable-modifications
+
+Activates: Report modifications
+to immutable fields in the Impurity checker (Conversely:
+--no-impurity-report-immutable-modifications )
+
+
--no-inefficient-keyset-iterator
Deactivates: checker
@@ -509,6 +523,13 @@ modelled as allocs in Pulse
modelled as release in Pulse
+--pulse-model-return-first-arg
+string
+
+Regex of methods that should be
+modelled as returning the first argument in Pulse
+
+
--pulse-model-return-nonnull
string
@@ -697,31 +718,18 @@ progress is being made because of concurrency errors.
and disable all other checkers (Conversely:
--no-starvation-only )
---topl-biabd
+--topl
-Activates: checker topl-biabd:
+
Activates: checker topl:
Detects errors based on user-provided state machines
describing multi-object monitors. (Conversely:
---no-topl-biabd )
-
---topl-biabd-only
+--no-topl )
-Activates: Enable topl-biabd
-and disable all other checkers (Conversely:
---no-topl-biabd-only )
+--topl-only
---topl-pulse
-
-Activates: checker topl-pulse:
-Detects errors based on user-provided state machines
-describing multi-object monitors. (Conversely:
---no-topl-pulse )
-
---topl-pulse-only
-
-Activates: Enable topl-pulse
-and disable all other checkers (Conversely:
---no-topl-pulse-only )
+Activates: Enable topl and
+disable all other checkers (Conversely:
+--no-topl-only )
--no-uninit
@@ -735,8 +743,25 @@ Warns when values are used before having been initialized.
disable all other checkers (Conversely:
--no-uninit-only )
---xcode-isysroot-suffix
-string
+--write-html
+
+Activates: Produce html debug
+output for the analyses in infer-out/captured. This shows
+the abstract state of all analyses at each program point in
+the source code. Each captured source file has its own html
+page. This HTML file contains the source file, and at each
+line of
+
+the file there are links to the
+nodes of the control flow graph
+of Infer's translation of that line of code into its
+intermediate
+representation (SIL). This way it's possible to see what the
+
+translation is, and the details of the symbolic execution on
+each
+node. (Conversely: --no-write-html )
+--xcode-isysroot-suffix string
Specify the suffix of Xcode
isysroot directory, to avoid absolute paths in tests
@@ -822,6 +847,13 @@ annotation reachability specs with the given sources
spec
+--biabduction-unsafe-malloc
+
+Activates: Assume that
+malloc(3) never returns null. (Conversely:
+--no-biabduction-unsafe-malloc )
+
+
--clang-compound-literal-init-limit
int
@@ -849,22 +881,6 @@ common wrappers around these types such as
when the variables are not read explicitly by the
program.
---ml-buckets
-,-separated sequence of { all | cf | arc | narc | cpp |
-
-unknown_origin }
-
-Specify the memory leak buckets
-to be checked in C++:
-
-- cpp from C++ code
-
---unsafe-malloc
-
-Activates: Assume that
-malloc(3) never returns null. (Conversely:
---no-unsafe-malloc )
-
JAVA OPTIONS
diff --git a/website/static/man/next/infer-capture.1.html b/website/static/man/next/infer-capture.1.html
index 7827e7a5d..91e5dbdd6 100644
--- a/website/static/man/next/infer-capture.1.html
+++ b/website/static/man/next/infer-capture.1.html
@@ -104,8 +104,8 @@ sets --debug-level 2 , --developer-mode ,
--print-buckets , --print-types ,
--reports-include-ml-loc ,
--no-only-cheap-debug , --trace-error ,
---write-dotty , --write-html ) (Conversely:
---no-debug | -G )
+--write-html ) (Conversely: --no-debug |
+-G )
--debug-level
level
diff --git a/website/static/man/next/infer-compile.1.html b/website/static/man/next/infer-compile.1.html
index df328cf2d..e63098f0f 100644
--- a/website/static/man/next/infer-compile.1.html
+++ b/website/static/man/next/infer-compile.1.html
@@ -71,8 +71,8 @@ sets --debug-level 2 , --developer-mode ,
--print-buckets , --print-types ,
--reports-include-ml-loc ,
--no-only-cheap-debug , --trace-error ,
---write-dotty , --write-html ) (Conversely:
---no-debug | -G )
+--write-html ) (Conversely: --no-debug |
+-G )
--debug-level
level
diff --git a/website/static/man/next/infer-explore.1.html b/website/static/man/next/infer-explore.1.html
index 60ae07a57..fb8c0d830 100644
--- a/website/static/man/next/infer-explore.1.html
+++ b/website/static/man/next/infer-explore.1.html
@@ -94,8 +94,8 @@ files in the specified directory
--html
-Activates: Generate html
-report. (Conversely: --no-html )
+Activates: Generate an html
+report of issues found. (Conversely: --no-html )
--max-nesting
int
diff --git a/website/static/man/next/infer-report.1.html b/website/static/man/next/infer-report.1.html
index 1378475bf..ebe7f78ae 100644
--- a/website/static/man/next/infer-report.1.html
+++ b/website/static/man/next/infer-report.1.html
@@ -135,8 +135,8 @@ sets --debug-level 2 , --developer-mode ,
--print-buckets , --print-types ,
--reports-include-ml-loc ,
--no-only-cheap-debug , --trace-error ,
---write-dotty , --write-html ) (Conversely:
---no-debug | -G )
+--write-html ) (Conversely: --no-debug |
+-G )
--debug-level
level
@@ -367,8 +367,7 @@ STRONG_SELF_NOT_CHECKED (enabled by default),
Symexec_memory_error (enabled by default),
THREAD_SAFETY_VIOLATION (enabled by default),
THREAD_SAFETY_VIOLATION_NULLSAFE (enabled by default),
-TOPL_BIABD_ERROR (enabled by default),
-TOPL_PULSE_ERROR (enabled by default),
+TOPL_ERROR (enabled by default),
UNINITIALIZED_VALUE (enabled by default),
UNREACHABLE_CODE (enabled by default),
UNTRUSTED_BUFFER_ACCESS (disabled by default),
@@ -507,13 +506,6 @@ none | phabricator }
emitting the report
---report-immutable-modifications
-
-Activates: Report modifications
-to immutable fields (Conversely:
---no-report-immutable-modifications )
-
-
--report-suppress-errors
+error_name
diff --git a/website/static/man/next/infer-reportdiff.1.html b/website/static/man/next/infer-reportdiff.1.html
index d3b30e854..745df8c8e 100644
--- a/website/static/man/next/infer-reportdiff.1.html
+++ b/website/static/man/next/infer-reportdiff.1.html
@@ -121,8 +121,8 @@ sets --debug-level 2 , --developer-mode ,
--print-buckets , --print-types ,
--reports-include-ml-loc ,
--no-only-cheap-debug , --trace-error ,
---write-dotty , --write-html ) (Conversely:
---no-debug | -G )
+--write-html ) (Conversely: --no-debug |
+-G )
--debug-level
level
diff --git a/website/static/man/next/infer-run.1.html b/website/static/man/next/infer-run.1.html
index dd2541577..7a576bd0d 100644
--- a/website/static/man/next/infer-run.1.html
+++ b/website/static/man/next/infer-run.1.html
@@ -102,8 +102,8 @@ sets --debug-level 2 , --developer-mode ,
--print-buckets , --print-types ,
--reports-include-ml-loc ,
--no-only-cheap-debug , --trace-error ,
---write-dotty , --write-html ) (Conversely:
---no-debug | -G )
+--write-html ) (Conversely: --no-debug |
+-G )
--debug-level
level
@@ -232,13 +232,6 @@ absolute path to a relative path to the root directory
(Conversely: --no-report-force-relative-path )
---report-immutable-modifications
-
-Activates: Report modifications
-to immutable fields (Conversely:
---no-report-immutable-modifications )
-
-
--report-suppress-errors
+error_name
diff --git a/website/static/man/next/infer.1.html b/website/static/man/next/infer.1.html
index d9f994bc8..a985f4fd7 100644
--- a/website/static/man/next/infer.1.html
+++ b/website/static/man/next/infer.1.html
@@ -220,6 +220,22 @@ many linked to memory safety. (Conversely:
and disable all other checkers (Conversely:
--no-biabduction-only )
+See also
+infer-analyze (1).
+--biabduction-unsafe-malloc
+
+Activates: Assume that
+malloc(3) never returns null. (Conversely:
+--no-biabduction-unsafe-malloc )
+
+See also
+infer-analyze (1).
+--biabduction-write-dotty
+
+Activates: Produce dotty files
+for specs and retain cycles reports in infer-out/captured.
+(Conversely: --no-biabduction-write-dotty )
+
See also
infer-analyze (1).
--bo-debug int
@@ -618,8 +634,8 @@ sets --debug-level 2 , --developer-mode ,
--print-buckets , --print-types ,
--reports-include-ml-loc ,
--no-only-cheap-debug , --trace-error ,
---write-dotty , --write-html ) (Conversely:
---no-debug | -G )
+--write-html ) (Conversely: --no-debug |
+-G )
See also
infer-analyze (1), infer-analyzejson (1),
@@ -907,8 +923,7 @@ STRONG_SELF_NOT_CHECKED (enabled by default),
Symexec_memory_error (enabled by default),
THREAD_SAFETY_VIOLATION (enabled by default),
THREAD_SAFETY_VIOLATION_NULLSAFE (enabled by default),
-TOPL_BIABD_ERROR (enabled by default),
-TOPL_PULSE_ERROR (enabled by default),
+TOPL_ERROR (enabled by default),
UNINITIALIZED_VALUE (enabled by default),
UNREACHABLE_CODE (enabled by default),
UNTRUSTED_BUFFER_ACCESS (disabled by default),
@@ -1157,8 +1172,8 @@ i.e. at least linear (Conversely:
infer-report (1).
--html
-Activates: Generate html
-report. (Conversely: --no-html )
+Activates: Generate an html
+report of issues found. (Conversely: --no-html )
See also
infer-explore (1).
@@ -1197,6 +1212,14 @@ Detects functions with potential side-effects. Same as
disable all other checkers (Conversely:
--no-impurity-only )
+See also
+infer-analyze (1).
+--impurity-report-immutable-modifications
+
+Activates: Report modifications
+to immutable fields in the Impurity checker (Conversely:
+--no-impurity-report-immutable-modifications )
+
See also
infer-analyze (1).
--no-inefficient-keyset-iterator
@@ -1476,15 +1499,6 @@ results directories specified in the dependency file.
See also
infer-analyze (1).
---ml-buckets ,-separated sequence of { all | cf | arc
-| narc | cpp |
-unknown_origin }
-
-Specify the memory leak buckets
-to be checked in C++:
-
-- cpp from C++ code
-See also infer-analyze (1).
--pmd-xml
Activates: Output issues in
@@ -1674,6 +1688,13 @@ modelled as allocs in Pulse
Regex of methods that should be
modelled as release in Pulse
+See also
+infer-analyze (1).
+--pulse-model-return-first-arg string
+
+Regex of methods that should be
+modelled as returning the first argument in Pulse
+
See also
infer-analyze (1).
--pulse-model-return-nonnull string
@@ -1886,14 +1907,6 @@ emitting the report
See also
infer-report (1).
---report-immutable-modifications
-
-Activates: Report modifications
-to immutable fields (Conversely:
---no-report-immutable-modifications )
-
-See also infer-report (1)
-and infer-run (1).
--report-previous path
Report of the base revision to
@@ -2161,37 +2174,20 @@ should be considered aliases of @ThreadSafe
See also
infer-analyze (1).
---topl-biabd
-
-Activates: checker topl-biabd:
-Detects errors based on user-provided state machines
-describing multi-object monitors. (Conversely:
---no-topl-biabd )
-
-See also
-infer-analyze (1).
---topl-biabd-only
-
-Activates: Enable topl-biabd
-and disable all other checkers (Conversely:
---no-topl-biabd-only )
-
-See also
-infer-analyze (1).
---topl-pulse
+--topl
-Activates: checker topl-pulse:
+
Activates: checker topl:
Detects errors based on user-provided state machines
describing multi-object monitors. (Conversely:
---no-topl-pulse )
+--no-topl )
See also
infer-analyze (1).
---topl-pulse-only
+--topl-only
-Activates: Enable topl-pulse
-and disable all other checkers (Conversely:
---no-topl-pulse-only )
+Activates: Enable topl and
+disable all other checkers (Conversely:
+--no-topl-only )
See also
infer-analyze (1).
@@ -2209,14 +2205,6 @@ Warns when values are used before having been initialized.
disable all other checkers (Conversely:
--no-uninit-only )
-See also
-infer-analyze (1).
---unsafe-malloc
-
-Activates: Assume that
-malloc(3) never returns null. (Conversely:
---no-unsafe-malloc )
-
See also
infer-analyze (1).
--version
@@ -2244,6 +2232,25 @@ single project root is enough, though.
See also
infer-capture (1).
+--write-html
+
+Activates: Produce html debug
+output for the analyses in infer-out/captured. This shows
+the abstract state of all analyses at each program point in
+the source code. Each captured source file has its own html
+page. This HTML file contains the source file, and at each
+line of
+
+the file there are links to the
+nodes of the control flow graph
+of Infer's translation of that line of code into its
+intermediate
+representation (SIL). This way it's possible to see what the
+
+translation is, and the details of the symbolic execution on
+each
+node. (Conversely: --no-write-html )
+See also infer-analyze (1).
--write-website path_to_website_dir
Use to write website files
diff --git a/website/static/odoc/next/infer/Absint/PatternMatch/Java/index.html b/website/static/odoc/next/infer/Absint/PatternMatch/Java/index.html
index 5f7e56678..2ada76ce6 100644
--- a/website/static/odoc/next/infer/Absint/PatternMatch/Java/index.html
+++ b/website/static/odoc/next/infer/Absint/PatternMatch/Java/index.html
@@ -1,2 +1,2 @@
-
Java (infer.Absint.PatternMatch.Java) val implements : string -> IR.Tenv.t -> string -> bool
Check whether class implements a given Java class
val implements_arrays : IR.Tenv.t -> string -> bool
Check whether class implements Java's Arrays
val implements_iterable : IR.Tenv.t -> string -> bool
Check whether class implements Java's Iterable
val implements_iterator : IR.Tenv.t -> string -> bool
Check whether class implements Java's Iterator
val implements_collection : IR.Tenv.t -> string -> bool
Check whether class implements a Java's Collection
val implements_collections : IR.Tenv.t -> string -> bool
Check whether class implements a Java's Collections
val implements_pseudo_collection : IR.Tenv.t -> string -> bool
Check whether class implements a pseudo Collection with support for get() and size() methods
val implements_enumeration : IR.Tenv.t -> string -> bool
Check whether class implements a Java's Enumeration
val implements_jackson : string -> IR.Tenv.t -> string -> bool
Check whether class implements a class from Jackson
val implements_org_json : string -> IR.Tenv.t -> string -> bool
Check whether class implements a class from Json
val implements_inject : string -> IR.Tenv.t -> string -> bool
Check whether class implements a Javax Inject
val implements_io : string -> IR.Tenv.t -> string -> bool
Check whether class implements a Java IO
val implements_nio : string -> IR.Tenv.t -> string -> bool
Check whether class implements a Java nio
val implements_map : IR.Tenv.t -> string -> bool
Check whether class implements a Java's Map
val implements_androidx_map : IR.Tenv.t -> string -> bool
Check whether class implements a AndroidX's Map
val implements_set : IR.Tenv.t -> string -> bool
Check whether class implements a Java's Set
val implements_map_entry : IR.Tenv.t -> string -> bool
Check whether class implements a Java's Map$Entry
val implements_queue : IR.Tenv.t -> string -> bool
Check whether class implements a Java's Queue
val implements_lang : string -> IR.Tenv.t -> string -> bool
Check whether class implements a Java's lang
val implements_list : IR.Tenv.t -> string -> bool
Check whether class implements a Java's list
val implements_google : string -> IR.Tenv.t -> string -> bool
Check whether class implements a class of Google
val implements_android : string -> IR.Tenv.t -> string -> bool
Check whether class implements a class of Android
val implements_infer_annotation : string -> IR.Tenv.t -> string -> bool
Check whether class implements a class of Infer annotation
val implements_app_activity : IR.Tenv.t -> string -> bool
Check whether class implements a class of android.app.Activity
val implements_app_fragment : IR.Tenv.t -> string -> bool
Check whether class implements a class of androidx.fragment.app.Fragment
val implements_graphql_story : IR.Tenv.t -> string -> bool
Check whether class implements a class of com.facebook.graphql.model.GraphQLStory
val implements_psi_element : IR.Tenv.t -> string -> bool
Check whether class implements a class of com.intellij.psi.PsiElement
val implements_sparse_float_array : IR.Tenv.t -> string -> bool
Check whether class implements a class of com.facebook.litho.internal.SparseFloatArray
val implements_view_group : IR.Tenv.t -> string -> bool
Check whether class implements a class of android.view.ViewGroup
val implements_view_parent : IR.Tenv.t -> string -> bool
Check whether class implements a class of android.view.ViewParent
val implements_xmob_utils : string -> IR.Tenv.t -> string -> bool
Check whether class implements a class of xmod.utils
val is_throwable : IR.Tenv.t -> IR.Typ.Name.t -> bool
is_throwable tenv class_name
checks if class_name is of type java.lang.Throwable
val is_enum : IR.Tenv.t -> IR.Typ.Name.t -> bool
Checks if the type is Java enum (extends java.lang.Enum)
val check_class_attributes : (IR.Annot.Item.t -> bool) -> IR.Tenv.t -> IR.Procname.t -> bool
tests whether any class attributes (e.g., @ThreadSafe
) pass check of first argument, including supertypes
val check_current_class_attributes : (IR.Annot.Item.t -> bool) -> IR.Tenv.t -> IR.Procname.t -> bool
tests whether any class attributes (e.g., @ThreadSafe
) pass check of first argument, for current class only
val find_superclasses_with_attributes : (IR.Annot.Item.t -> bool) -> IR.Tenv.t -> IR.Typ.Name.t -> IR.Typ.Name.t list
find superclasss with attributes (e.g., @ThreadSafe
), including current class
val is_override_of_lang_object_equals : IR.Procname.t -> bool
Whether the method is an override of `java.lang.Object.equals(Object)` or `java.lang.Object.equals(Object)` itself
val method_is_initializer : IR.Tenv.t -> IR.ProcAttributes.t -> bool
Check if the method is one of the known initializer methods.
\ No newline at end of file
+Java (infer.Absint.PatternMatch.Java) val implements : string -> IR.Tenv.t -> string -> bool
Check whether class implements a given Java class
val implements_android : string -> IR.Tenv.t -> string -> bool
Check whether class implements a class of Android
val implements_androidx_map : IR.Tenv.t -> string -> bool
Check whether class implements a AndroidX's Map
val implements_app_activity : IR.Tenv.t -> string -> bool
Check whether class implements a class of android.app.Activity
val implements_app_fragment : IR.Tenv.t -> string -> bool
Check whether class implements a class of androidx.fragment.app.Fragment
val implements_arrays : IR.Tenv.t -> string -> bool
Check whether class implements Java's Arrays
val implements_collection : IR.Tenv.t -> string -> bool
Check whether class implements a Java's Collection
val implements_collections : IR.Tenv.t -> string -> bool
Check whether class implements a Java's Collections
val implements_enumeration : IR.Tenv.t -> string -> bool
Check whether class implements a Java's Enumeration
val implements_google : string -> IR.Tenv.t -> string -> bool
Check whether class implements a class of Google
val implements_graphql_story : IR.Tenv.t -> string -> bool
Check whether class implements a class of com.facebook.graphql.model.GraphQLStory
val implements_infer_annotation : string -> IR.Tenv.t -> string -> bool
Check whether class implements a class of Infer annotation
val implements_inject : string -> IR.Tenv.t -> string -> bool
Check whether class implements a Javax Inject
val implements_io : string -> IR.Tenv.t -> string -> bool
Check whether class implements a Java IO
val implements_iterable : IR.Tenv.t -> string -> bool
Check whether class implements Java's Iterable
val implements_iterator : IR.Tenv.t -> string -> bool
Check whether class implements Java's Iterator
val implements_jackson : string -> IR.Tenv.t -> string -> bool
Check whether class implements a class from Jackson
val implements_lang : string -> IR.Tenv.t -> string -> bool
Check whether class implements a Java's lang
val implements_list : IR.Tenv.t -> string -> bool
Check whether class implements a Java's list
val implements_map : IR.Tenv.t -> string -> bool
Check whether class implements a Java's Map
val implements_map_entry : IR.Tenv.t -> string -> bool
Check whether class implements a Java's Map$Entry
val implements_math : IR.Tenv.t -> string -> bool
Check whether class implements a Java's Math
val implements_nio : string -> IR.Tenv.t -> string -> bool
Check whether class implements a Java nio
val implements_org_json : string -> IR.Tenv.t -> string -> bool
Check whether class implements a class from Json
val implements_pseudo_collection : IR.Tenv.t -> string -> bool
Check whether class implements a pseudo Collection with support for get() and size() methods
val implements_psi_element : IR.Tenv.t -> string -> bool
Check whether class implements a class of com.intellij.psi.PsiElement
val implements_queue : IR.Tenv.t -> string -> bool
Check whether class implements a Java's Queue
val implements_set : IR.Tenv.t -> string -> bool
Check whether class implements a Java's Set
val implements_sparse_float_array : IR.Tenv.t -> string -> bool
Check whether class implements a class of com.facebook.litho.internal.SparseFloatArray
val implements_view_group : IR.Tenv.t -> string -> bool
Check whether class implements a class of android.view.ViewGroup
val implements_view_parent : IR.Tenv.t -> string -> bool
Check whether class implements a class of android.view.ViewParent
val implements_xmob_utils : string -> IR.Tenv.t -> string -> bool
Check whether class implements a class of xmod.utils
val is_throwable : IR.Tenv.t -> IR.Typ.Name.t -> bool
is_throwable tenv class_name
checks if class_name is of type java.lang.Throwable
val is_enum : IR.Tenv.t -> IR.Typ.Name.t -> bool
Checks if the type is Java enum (extends java.lang.Enum)
val check_class_attributes : (IR.Annot.Item.t -> bool) -> IR.Tenv.t -> IR.Procname.t -> bool
tests whether any class attributes (e.g., @ThreadSafe
) pass check of first argument, including supertypes
val check_current_class_attributes : (IR.Annot.Item.t -> bool) -> IR.Tenv.t -> IR.Procname.t -> bool
tests whether any class attributes (e.g., @ThreadSafe
) pass check of first argument, for current class only
val find_superclasses_with_attributes : (IR.Annot.Item.t -> bool) -> IR.Tenv.t -> IR.Typ.Name.t -> IR.Typ.Name.t list
find superclasss with attributes (e.g., @ThreadSafe
), including current class
val is_override_of_lang_object_equals : IR.Procname.t -> bool
Whether the method is an override of `java.lang.Object.equals(Object)` or `java.lang.Object.equals(Object)` itself
val method_is_initializer : IR.Tenv.t -> IR.ProcAttributes.t -> bool
Check if the method is one of the known initializer methods.
\ No newline at end of file
diff --git a/website/static/odoc/next/infer/Absint__PatternMatch/Java/index.html b/website/static/odoc/next/infer/Absint__PatternMatch/Java/index.html
index 15b4859bc..ba9d7ee94 100644
--- a/website/static/odoc/next/infer/Absint__PatternMatch/Java/index.html
+++ b/website/static/odoc/next/infer/Absint__PatternMatch/Java/index.html
@@ -1,2 +1,2 @@
-Java (infer.Absint__PatternMatch.Java) val implements : string -> IR.Tenv.t -> string -> bool
Check whether class implements a given Java class
val implements_arrays : IR.Tenv.t -> string -> bool
Check whether class implements Java's Arrays
val implements_iterable : IR.Tenv.t -> string -> bool
Check whether class implements Java's Iterable
val implements_iterator : IR.Tenv.t -> string -> bool
Check whether class implements Java's Iterator
val implements_collection : IR.Tenv.t -> string -> bool
Check whether class implements a Java's Collection
val implements_collections : IR.Tenv.t -> string -> bool
Check whether class implements a Java's Collections
val implements_pseudo_collection : IR.Tenv.t -> string -> bool
Check whether class implements a pseudo Collection with support for get() and size() methods
val implements_enumeration : IR.Tenv.t -> string -> bool
Check whether class implements a Java's Enumeration
val implements_jackson : string -> IR.Tenv.t -> string -> bool
Check whether class implements a class from Jackson
val implements_org_json : string -> IR.Tenv.t -> string -> bool
Check whether class implements a class from Json
val implements_inject : string -> IR.Tenv.t -> string -> bool
Check whether class implements a Javax Inject
val implements_io : string -> IR.Tenv.t -> string -> bool
Check whether class implements a Java IO
val implements_nio : string -> IR.Tenv.t -> string -> bool
Check whether class implements a Java nio
val implements_map : IR.Tenv.t -> string -> bool
Check whether class implements a Java's Map
val implements_androidx_map : IR.Tenv.t -> string -> bool
Check whether class implements a AndroidX's Map
val implements_set : IR.Tenv.t -> string -> bool
Check whether class implements a Java's Set
val implements_map_entry : IR.Tenv.t -> string -> bool
Check whether class implements a Java's Map$Entry
val implements_queue : IR.Tenv.t -> string -> bool
Check whether class implements a Java's Queue
val implements_lang : string -> IR.Tenv.t -> string -> bool
Check whether class implements a Java's lang
val implements_list : IR.Tenv.t -> string -> bool
Check whether class implements a Java's list
val implements_google : string -> IR.Tenv.t -> string -> bool
Check whether class implements a class of Google
val implements_android : string -> IR.Tenv.t -> string -> bool
Check whether class implements a class of Android
val implements_infer_annotation : string -> IR.Tenv.t -> string -> bool
Check whether class implements a class of Infer annotation
val implements_app_activity : IR.Tenv.t -> string -> bool
Check whether class implements a class of android.app.Activity
val implements_app_fragment : IR.Tenv.t -> string -> bool
Check whether class implements a class of androidx.fragment.app.Fragment
val implements_graphql_story : IR.Tenv.t -> string -> bool
Check whether class implements a class of com.facebook.graphql.model.GraphQLStory
val implements_psi_element : IR.Tenv.t -> string -> bool
Check whether class implements a class of com.intellij.psi.PsiElement
val implements_sparse_float_array : IR.Tenv.t -> string -> bool
Check whether class implements a class of com.facebook.litho.internal.SparseFloatArray
val implements_view_group : IR.Tenv.t -> string -> bool
Check whether class implements a class of android.view.ViewGroup
val implements_view_parent : IR.Tenv.t -> string -> bool
Check whether class implements a class of android.view.ViewParent
val implements_xmob_utils : string -> IR.Tenv.t -> string -> bool
Check whether class implements a class of xmod.utils
val is_throwable : IR.Tenv.t -> IR.Typ.Name.t -> bool
is_throwable tenv class_name
checks if class_name is of type java.lang.Throwable
val is_enum : IR.Tenv.t -> IR.Typ.Name.t -> bool
Checks if the type is Java enum (extends java.lang.Enum)
val check_class_attributes : (IR.Annot.Item.t -> bool) -> IR.Tenv.t -> IR.Procname.t -> bool
tests whether any class attributes (e.g., @ThreadSafe
) pass check of first argument, including supertypes
val check_current_class_attributes : (IR.Annot.Item.t -> bool) -> IR.Tenv.t -> IR.Procname.t -> bool
tests whether any class attributes (e.g., @ThreadSafe
) pass check of first argument, for current class only
val find_superclasses_with_attributes : (IR.Annot.Item.t -> bool) -> IR.Tenv.t -> IR.Typ.Name.t -> IR.Typ.Name.t list
find superclasss with attributes (e.g., @ThreadSafe
), including current class
val is_override_of_lang_object_equals : IR.Procname.t -> bool
Whether the method is an override of `java.lang.Object.equals(Object)` or `java.lang.Object.equals(Object)` itself
val method_is_initializer : IR.Tenv.t -> IR.ProcAttributes.t -> bool
Check if the method is one of the known initializer methods.
\ No newline at end of file
+Java (infer.Absint__PatternMatch.Java) val implements : string -> IR.Tenv.t -> string -> bool
Check whether class implements a given Java class
val implements_android : string -> IR.Tenv.t -> string -> bool
Check whether class implements a class of Android
val implements_androidx_map : IR.Tenv.t -> string -> bool
Check whether class implements a AndroidX's Map
val implements_app_activity : IR.Tenv.t -> string -> bool
Check whether class implements a class of android.app.Activity
val implements_app_fragment : IR.Tenv.t -> string -> bool
Check whether class implements a class of androidx.fragment.app.Fragment
val implements_arrays : IR.Tenv.t -> string -> bool
Check whether class implements Java's Arrays
val implements_collection : IR.Tenv.t -> string -> bool
Check whether class implements a Java's Collection
val implements_collections : IR.Tenv.t -> string -> bool
Check whether class implements a Java's Collections
val implements_enumeration : IR.Tenv.t -> string -> bool
Check whether class implements a Java's Enumeration
val implements_google : string -> IR.Tenv.t -> string -> bool
Check whether class implements a class of Google
val implements_graphql_story : IR.Tenv.t -> string -> bool
Check whether class implements a class of com.facebook.graphql.model.GraphQLStory
val implements_infer_annotation : string -> IR.Tenv.t -> string -> bool
Check whether class implements a class of Infer annotation
val implements_inject : string -> IR.Tenv.t -> string -> bool
Check whether class implements a Javax Inject
val implements_io : string -> IR.Tenv.t -> string -> bool
Check whether class implements a Java IO
val implements_iterable : IR.Tenv.t -> string -> bool
Check whether class implements Java's Iterable
val implements_iterator : IR.Tenv.t -> string -> bool
Check whether class implements Java's Iterator
val implements_jackson : string -> IR.Tenv.t -> string -> bool
Check whether class implements a class from Jackson
val implements_lang : string -> IR.Tenv.t -> string -> bool
Check whether class implements a Java's lang
val implements_list : IR.Tenv.t -> string -> bool
Check whether class implements a Java's list
val implements_map : IR.Tenv.t -> string -> bool
Check whether class implements a Java's Map
val implements_map_entry : IR.Tenv.t -> string -> bool
Check whether class implements a Java's Map$Entry
val implements_math : IR.Tenv.t -> string -> bool
Check whether class implements a Java's Math
val implements_nio : string -> IR.Tenv.t -> string -> bool
Check whether class implements a Java nio
val implements_org_json : string -> IR.Tenv.t -> string -> bool
Check whether class implements a class from Json
val implements_pseudo_collection : IR.Tenv.t -> string -> bool
Check whether class implements a pseudo Collection with support for get() and size() methods
val implements_psi_element : IR.Tenv.t -> string -> bool
Check whether class implements a class of com.intellij.psi.PsiElement
val implements_queue : IR.Tenv.t -> string -> bool
Check whether class implements a Java's Queue
val implements_set : IR.Tenv.t -> string -> bool
Check whether class implements a Java's Set
val implements_sparse_float_array : IR.Tenv.t -> string -> bool
Check whether class implements a class of com.facebook.litho.internal.SparseFloatArray
val implements_view_group : IR.Tenv.t -> string -> bool
Check whether class implements a class of android.view.ViewGroup
val implements_view_parent : IR.Tenv.t -> string -> bool
Check whether class implements a class of android.view.ViewParent
val implements_xmob_utils : string -> IR.Tenv.t -> string -> bool
Check whether class implements a class of xmod.utils
val is_throwable : IR.Tenv.t -> IR.Typ.Name.t -> bool
is_throwable tenv class_name
checks if class_name is of type java.lang.Throwable
val is_enum : IR.Tenv.t -> IR.Typ.Name.t -> bool
Checks if the type is Java enum (extends java.lang.Enum)
val check_class_attributes : (IR.Annot.Item.t -> bool) -> IR.Tenv.t -> IR.Procname.t -> bool
tests whether any class attributes (e.g., @ThreadSafe
) pass check of first argument, including supertypes
val check_current_class_attributes : (IR.Annot.Item.t -> bool) -> IR.Tenv.t -> IR.Procname.t -> bool
tests whether any class attributes (e.g., @ThreadSafe
) pass check of first argument, for current class only
val find_superclasses_with_attributes : (IR.Annot.Item.t -> bool) -> IR.Tenv.t -> IR.Typ.Name.t -> IR.Typ.Name.t list
find superclasss with attributes (e.g., @ThreadSafe
), including current class
val is_override_of_lang_object_equals : IR.Procname.t -> bool
Whether the method is an override of `java.lang.Object.equals(Object)` or `java.lang.Object.equals(Object)` itself
val method_is_initializer : IR.Tenv.t -> IR.ProcAttributes.t -> bool
Check if the method is one of the known initializer methods.
\ No newline at end of file
diff --git a/website/static/odoc/next/infer/Biabduction/Predicates/index.html b/website/static/odoc/next/infer/Biabduction/Predicates/index.html
index b2d99bdd7..b8a8505fb 100644
--- a/website/static/odoc/next/infer/Biabduction/Predicates/index.html
+++ b/website/static/odoc/next/infer/Biabduction/Predicates/index.html
@@ -1,2 +1,2 @@
-Predicates (infer.Biabduction.Predicates) type offset
=
Offset for an lvalue.
Components of Propositionstype atom
=
an atom is a pure atomic formula
val equal_atom : atom -> atom -> bool
val atom_has_local_addr : atom -> bool
type lseg_kind
=
|
Lseg_NE
nonempty (possibly circular) listseg
|
Lseg_PE
possibly empty (possibly circular) listseg
kind of lseg or dllseg predicates
val equal_lseg_kind : lseg_kind -> lseg_kind -> bool
type zero_flag
= bool option
The boolean is true when the pointer was dereferenced without testing for zero.
type null_case_flag
= bool
True when the value was obtained by doing case analysis on null in a procedure call.
type inst
=
instrumentation of heap values
val equal_inst : inst -> inst -> bool
val inst_actual_precondition : inst
val inst_formal : inst
val inst_initial : inst
for formal parameters and heap values at the beginning of the function
val inst_lookup : inst
for initial values
val inst_none : inst
val inst_nullify : inst
val inst_rearrange : bool -> IBase.Location.t -> IR.PredSymb.path_pos -> inst
the boolean indicates whether the pointer is known nonzero
val inst_update : IBase.Location.t -> IR.PredSymb.path_pos -> inst
val inst_set_null_case_flag : inst -> inst
Set the null case flag of the inst.
val inst_new_loc : IBase.Location.t -> inst -> inst
update the location of the instrumentation
val update_inst : inst -> inst -> inst
Update inst_old
to inst_new
preserving the zero flag
exception
JoinFail
val inst_partial_join : inst -> inst -> inst
join of instrumentations, can raise JoinFail
val inst_partial_meet : inst -> inst -> inst
meet of instrumentations
type 'inst strexp0
=
|
Eexp of IR.Exp.t * 'inst
Base case: expression with instrumentation
|
Estruct of (IR.Fieldname.t * 'inst strexp0 ) list * 'inst
C structure
|
Earray of IR.Exp.t * (IR.Exp.t * 'inst strexp0 ) list * 'inst
Array of given length There are two conditions imposed / used in the array case. First, if some index and value pair appears inside an array in a strexp, then the index is less than the length of the array. For instance, x |->[10 | e1: v1]
implies that e1 <= 9
. Second, if two indices appear in an array, they should be different. For instance, x |->[10 | e1: v1, e2: v2]
implies that e1 != e2
.
structured expressions represent a value of structured type, such as an array or a struct.
val compare_strexp0 : ('inst -> 'inst -> int) -> 'inst strexp0 -> 'inst strexp0 -> int
type strexp
= inst strexp0
val compare_strexp : ?inst:bool -> strexp -> strexp -> int
Comparison function for strexp. The inst:: parameter specifies whether instumentations should also be considered (false by default).
val equal_strexp : ?inst:bool -> strexp -> strexp -> bool
Equality function for strexp. The inst:: parameter specifies whether instumentations should also be considered (false by default).
type 'inst hpred0
=
|
Hpointsto of IR.Exp.t * 'inst strexp0 * IR.Exp.t
represents exp|->strexp:typexp
where typexp
is an expression representing a type, e.h. sizeof(t)
.
|
Hlseg of lseg_kind * 'inst hpara0 * IR.Exp.t * IR.Exp.t * IR.Exp.t list
higher - order predicate for singly - linked lists. Should ensure that exp1!= exp2 implies that exp1 is allocated. This assumption is used in the rearrangement. The last exp list
parameter is used to denote the shared links by all the nodes in the list.
|
Hdllseg of lseg_kind * 'inst hpara_dll0 * IR.Exp.t * IR.Exp.t * IR.Exp.t * IR.Exp.t * IR.Exp.t list
higher-order predicate for doubly-linked lists. Parameter for the higher-order singly-linked list predicate. Means "lambda (root,next,svars). Exists evars. body". Assume that root, next, svars, evars are disjoint sets of primed identifiers, and include all the free primed identifiers in body. body should not contain any non - primed identifiers or program variables (i.e. pvars).
an atomic heap predicate
and 'inst hpara0
=
{
}
and 'inst hpara_dll0
=
{
}
parameter for the higher-order doubly-linked list predicates. Assume that all the free identifiers in body_dll should belong to cell, blink, flink, svars_dll, evars_dll.
val compare_hpred0 : ('inst -> 'inst -> int) -> 'inst hpred0 -> 'inst hpred0 -> int
val compare_hpara0 : ('inst -> 'inst -> int) -> 'inst hpara0 -> 'inst hpara0 -> int
val compare_hpara_dll0 : ('inst -> 'inst -> int) -> 'inst hpara_dll0 -> 'inst hpara_dll0 -> int
val compare_hpred0 : ('inst -> 'inst -> int) -> 'inst hpred0 -> 'inst hpred0 -> int
val compare_hpara0 : ('inst -> 'inst -> int) -> 'inst hpara0 -> 'inst hpara0 -> int
val compare_hpara_dll0 : ('inst -> 'inst -> int) -> 'inst hpara_dll0 -> 'inst hpara_dll0 -> int
val compare_hpred0 : ('inst -> 'inst -> int) -> 'inst hpred0 -> 'inst hpred0 -> int
val compare_hpara0 : ('inst -> 'inst -> int) -> 'inst hpara0 -> 'inst hpara0 -> int
val compare_hpara_dll0 : ('inst -> 'inst -> int) -> 'inst hpara_dll0 -> 'inst hpara_dll0 -> int
type hpred
= inst hpred0
type hpara
= inst hpara0
type hpara_dll
= inst hpara_dll0
val compare_hpred : ?inst:bool -> hpred -> hpred -> int
Comparison function for hpred. The inst:: parameter specifies whether instumentations should also be considered (false by default).
val equal_hpred : ?inst:bool -> hpred -> hpred -> bool
Equality function for hpred. The inst:: parameter specifies whether instumentations should also be considered (false by default).
module HpredSet : IStdlib.IStd .Caml.Set.S with type HpredSet .elt = hpred
Sets of heap predicates
type sharing_env
val create_sharing_env : unit -> sharing_env
Create a sharing env to store canonical representations
val hpred_compact : sharing_env -> hpred -> hpred
Return a compact representation of the exp
val is_objc_object : hpred -> bool
Comparision And Inspection Functionsval pp_offset : IStdlib.Pp.env -> F .formatter -> offset -> unit
val d_offset_list : offset list -> unit
Dump a list of offsets
val pp_atom : IStdlib.Pp.env -> F .formatter -> atom -> unit
Pretty print an atom.
val d_atom : atom -> unit
Dump an atom.
val pp_inst : F .formatter -> inst -> unit
pretty-print an inst
val pp_sexp : IStdlib.Pp.env -> F .formatter -> strexp -> unit
Pretty print a strexp.
val d_sexp : strexp -> unit
Dump a strexp.
val pp_hpred : IStdlib.Pp.env -> F .formatter -> hpred -> unit
Pretty print a hpred.
val d_hpred : hpred -> unit
Dump a hpred.
val pp_hpara : IStdlib.Pp.env -> F .formatter -> hpara -> unit
Pretty print a hpara.
val pp_hpara_dll : IStdlib.Pp.env -> F .formatter -> hpara_dll -> unit
Pretty print a hpara_dll.
module Env : sig ... end
record the occurrences of predicates as parameters of (doubly -)linked lists and Epara. Provides unique numbering for predicates and an iterator.
val pp_hpred_env : IStdlib.Pp.env -> Env.t option -> F .formatter -> hpred -> unit
Pretty print a hpred with optional predicate env
type subst
= private (IR.Ident.t * IR.Exp.t ) list
val equal_subst : subst -> subst -> bool
Equality for substitutions.
val subst_of_list : (IR.Ident.t * IR.Exp.t ) list -> subst
Create a substitution from a list of pairs. For all (id1, e1), (id2, e2) in the input list, if id1 = id2, then e1 = e2.
val subst_of_list_duplicates : (IR.Ident.t * IR.Exp.t ) list -> subst
like subst_of_list, but allow duplicate ids and only keep the first occurrence
val sub_to_list : subst -> (IR.Ident.t * IR.Exp.t ) list
Convert a subst to a list of pairs.
val sub_empty : subst
The empty substitution.
val is_sub_empty : subst -> bool
val sub_join : subst -> subst -> subst
Compute the common id-exp part of two inputs subst1
and subst2
. The first component of the output is this common part. The second and third components are the remainder of subst1
and subst2
, respectively.
val sub_symmetric_difference : subst -> subst -> subst * subst * subst
Compute the common id-exp part of two inputs subst1
and subst2
. The first component of the output is this common part. The second and third components are the remainder of subst1
and subst2
, respectively.
val sub_find : (IR.Ident.t -> bool) -> subst -> IR.Exp.t
sub_find filter sub
returns the expression associated to the first identifier that satisfies filter
. Raise Not_found_s/Caml.Not_found
if there isn't one.
val sub_filter : (IR.Ident.t -> bool) -> subst -> subst
sub_filter filter sub
restricts the domain of sub
to the identifiers satisfying filter
.
val sub_filter_pair : subst -> f:((IR.Ident.t * IR.Exp.t ) -> bool) -> subst
sub_filter_exp filter sub
restricts the domain of sub
to the identifiers satisfying filter(id, sub(id))
.
val sub_range_partition : (IR.Exp.t -> bool) -> subst -> subst * subst
sub_range_partition filter sub
partitions sub
according to whether range expressions satisfy filter
.
val sub_domain_partition : (IR.Ident.t -> bool) -> subst -> subst * subst
sub_domain_partition filter sub
partitions sub
according to whether domain identifiers satisfy filter
.
val sub_domain : subst -> IR.Ident.t list
Return the list of identifiers in the domain of the substitution.
val sub_range : subst -> IR.Exp.t list
Return the list of expressions in the range of the substitution.
val sub_range_map : (IR.Exp.t -> IR.Exp.t ) -> subst -> subst
sub_range_map f sub
applies f
to the expressions in the range of sub
.
val sub_map : (IR.Ident.t -> IR.Ident.t ) -> (IR.Exp.t -> IR.Exp.t ) -> subst -> subst
sub_map f g sub
applies the renaming f
to identifiers in the domain of sub
and the substitution g
to the expressions in the range of sub
.
val extend_sub : subst -> IR.Ident.t -> IR.Exp.t -> subst option
Extend substitution and return None
if not possible.
val subst_free_vars : subst -> IR.Ident.t IStdlib.IStd .Sequence.t
val subst_gen_free_vars : subst -> (unit, IR.Ident.t ) IStdlib.IStd .Sequence.Generator.t
val exp_sub : subst -> IR.Exp.t -> IR.Exp.t
val atom_sub : subst -> atom -> atom
val instr_sub : subst -> IR.Sil.instr -> IR.Sil.instr
apply subst
to all id's in instr
, including LHS id's
val hpred_sub : subst -> hpred -> hpred
Functions for constructing or destructing entities in this moduleval exp_get_offsets : IR.Exp.t -> offset list
Compute the offset list of an expression
val exp_add_offsets : IR.Exp.t -> offset list -> IR.Exp.t
Add the offset list to an expression
val sigma_to_sigma_ne : hpred list -> (atom list * hpred list ) list
val hpara_instantiate : hpara -> IR.Exp.t -> IR.Exp.t -> IR.Exp.t list -> IR.Ident.t list * hpred list
hpara_instantiate para e1 e2 elist
instantiates para
with e1
, e2
and elist
. If para = lambda (x, y, xs). exists zs. b
, then the result of the instantiation is b[e1 / x, e2 / y, elist / xs, _zs'/ zs]
for some fresh _zs'
.
val hpara_dll_instantiate : hpara_dll -> IR.Exp.t -> IR.Exp.t -> IR.Exp.t -> IR.Exp.t list -> IR.Ident.t list * hpred list
hpara_dll_instantiate para cell blink flink elist
instantiates para
with cell
, blink
, flink
, and elist
. If para = lambda (x, y, z, xs). exists zs. b
, then the result of the instantiation is b[cell / x, blink / y, flink / z, elist / xs, _zs'/ zs]
for some fresh _zs'
.
val custom_error : IR.Pvar.t
\ No newline at end of file
+Predicates (infer.Biabduction.Predicates) type offset
=
Offset for an lvalue.
Components of Propositionstype atom
=
an atom is a pure atomic formula
val equal_atom : atom -> atom -> bool
val atom_has_local_addr : atom -> bool
type lseg_kind
=
|
Lseg_NE
nonempty (possibly circular) listseg
|
Lseg_PE
possibly empty (possibly circular) listseg
kind of lseg or dllseg predicates
val equal_lseg_kind : lseg_kind -> lseg_kind -> bool
type zero_flag
= bool option
The boolean is true when the pointer was dereferenced without testing for zero.
type null_case_flag
= bool
True when the value was obtained by doing case analysis on null in a procedure call.
type inst
=
instrumentation of heap values
val equal_inst : inst -> inst -> bool
val inst_actual_precondition : inst
val inst_formal : inst
val inst_initial : inst
for formal parameters and heap values at the beginning of the function
val inst_lookup : inst
for initial values
val inst_none : inst
val inst_nullify : inst
val inst_rearrange : bool -> IBase.Location.t -> IR.PredSymb.path_pos -> inst
the boolean indicates whether the pointer is known nonzero
val inst_update : IBase.Location.t -> IR.PredSymb.path_pos -> inst
val inst_set_null_case_flag : inst -> inst
Set the null case flag of the inst.
val inst_new_loc : IBase.Location.t -> inst -> inst
update the location of the instrumentation
val update_inst : inst -> inst -> inst
Update inst_old
to inst_new
preserving the zero flag
exception
JoinFail
val inst_partial_join : inst -> inst -> inst
join of instrumentations, can raise JoinFail
val inst_partial_meet : inst -> inst -> inst
meet of instrumentations
type 'inst strexp0
=
|
Eexp of IR.Exp.t * 'inst
Base case: expression with instrumentation
|
Estruct of (IR.Fieldname.t * 'inst strexp0 ) list * 'inst
C structure
|
Earray of IR.Exp.t * (IR.Exp.t * 'inst strexp0 ) list * 'inst
Array of given length There are two conditions imposed / used in the array case. First, if some index and value pair appears inside an array in a strexp, then the index is less than the length of the array. For instance, x |->[10 | e1: v1]
implies that e1 <= 9
. Second, if two indices appear in an array, they should be different. For instance, x |->[10 | e1: v1, e2: v2]
implies that e1 != e2
.
structured expressions represent a value of structured type, such as an array or a struct.
val compare_strexp0 : ('inst -> 'inst -> int) -> 'inst strexp0 -> 'inst strexp0 -> int
type strexp
= inst strexp0
val compare_strexp : ?inst:bool -> strexp -> strexp -> int
Comparison function for strexp. The inst:: parameter specifies whether instumentations should also be considered (false by default).
val equal_strexp : ?inst:bool -> strexp -> strexp -> bool
Equality function for strexp. The inst:: parameter specifies whether instumentations should also be considered (false by default).
type 'inst hpred0
=
|
Hpointsto of IR.Exp.t * 'inst strexp0 * IR.Exp.t
represents exp|->strexp:typexp
where typexp
is an expression representing a type, e.h. sizeof(t)
.
|
Hlseg of lseg_kind * 'inst hpara0 * IR.Exp.t * IR.Exp.t * IR.Exp.t list
higher - order predicate for singly - linked lists. Should ensure that exp1!= exp2 implies that exp1 is allocated. This assumption is used in the rearrangement. The last exp list
parameter is used to denote the shared links by all the nodes in the list.
|
Hdllseg of lseg_kind * 'inst hpara_dll0 * IR.Exp.t * IR.Exp.t * IR.Exp.t * IR.Exp.t * IR.Exp.t list
higher-order predicate for doubly-linked lists. Parameter for the higher-order singly-linked list predicate. Means "lambda (root,next,svars). Exists evars. body". Assume that root, next, svars, evars are disjoint sets of primed identifiers, and include all the free primed identifiers in body. body should not contain any non - primed identifiers or program variables (i.e. pvars).
an atomic heap predicate
and 'inst hpara0
=
{
}
and 'inst hpara_dll0
=
{
}
parameter for the higher-order doubly-linked list predicates. Assume that all the free identifiers in body_dll should belong to cell, blink, flink, svars_dll, evars_dll.
val compare_hpred0 : ('inst -> 'inst -> int) -> 'inst hpred0 -> 'inst hpred0 -> int
val compare_hpara0 : ('inst -> 'inst -> int) -> 'inst hpara0 -> 'inst hpara0 -> int
val compare_hpara_dll0 : ('inst -> 'inst -> int) -> 'inst hpara_dll0 -> 'inst hpara_dll0 -> int
val compare_hpred0 : ('inst -> 'inst -> int) -> 'inst hpred0 -> 'inst hpred0 -> int
val compare_hpara0 : ('inst -> 'inst -> int) -> 'inst hpara0 -> 'inst hpara0 -> int
val compare_hpara_dll0 : ('inst -> 'inst -> int) -> 'inst hpara_dll0 -> 'inst hpara_dll0 -> int
val compare_hpred0 : ('inst -> 'inst -> int) -> 'inst hpred0 -> 'inst hpred0 -> int
val compare_hpara0 : ('inst -> 'inst -> int) -> 'inst hpara0 -> 'inst hpara0 -> int
val compare_hpara_dll0 : ('inst -> 'inst -> int) -> 'inst hpara_dll0 -> 'inst hpara_dll0 -> int
type hpred
= inst hpred0
type hpara
= inst hpara0
type hpara_dll
= inst hpara_dll0
val compare_hpred : ?inst:bool -> hpred -> hpred -> int
Comparison function for hpred. The inst:: parameter specifies whether instumentations should also be considered (false by default).
val equal_hpred : ?inst:bool -> hpred -> hpred -> bool
Equality function for hpred. The inst:: parameter specifies whether instumentations should also be considered (false by default).
module HpredSet : IStdlib.IStd .Caml.Set.S with type HpredSet .elt = hpred
Sets of heap predicates
type sharing_env
val create_sharing_env : unit -> sharing_env
Create a sharing env to store canonical representations
val hpred_compact : sharing_env -> hpred -> hpred
Return a compact representation of the exp
val is_objc_object : hpred -> bool
Comparision And Inspection Functionsval pp_offset : IStdlib.Pp.env -> F .formatter -> offset -> unit
val d_offset_list : offset list -> unit
Dump a list of offsets
val pp_atom : IStdlib.Pp.env -> F .formatter -> atom -> unit
Pretty print an atom.
val d_atom : atom -> unit
Dump an atom.
val pp_inst : F .formatter -> inst -> unit
pretty-print an inst
val pp_sexp : IStdlib.Pp.env -> F .formatter -> strexp -> unit
Pretty print a strexp.
val d_sexp : strexp -> unit
Dump a strexp.
val pp_hpred : IStdlib.Pp.env -> F .formatter -> hpred -> unit
Pretty print a hpred.
val d_hpred : hpred -> unit
Dump a hpred.
val pp_hpara : IStdlib.Pp.env -> F .formatter -> hpara -> unit
Pretty print a hpara.
val pp_hpara_dll : IStdlib.Pp.env -> F .formatter -> hpara_dll -> unit
Pretty print a hpara_dll.
module Env : sig ... end
record the occurrences of predicates as parameters of (doubly -)linked lists and Epara. Provides unique numbering for predicates and an iterator.
val pp_hpred_env : IStdlib.Pp.env -> Env.t option -> F .formatter -> hpred -> unit
Pretty print a hpred with optional predicate env
type subst
= private (IR.Ident.t * IR.Exp.t ) list
val equal_subst : subst -> subst -> bool
Equality for substitutions.
val subst_of_list : (IR.Ident.t * IR.Exp.t ) list -> subst
Create a substitution from a list of pairs. For all (id1, e1), (id2, e2) in the input list, if id1 = id2, then e1 = e2.
val subst_of_list_duplicates : (IR.Ident.t * IR.Exp.t ) list -> subst
like subst_of_list, but allow duplicate ids and only keep the first occurrence
val sub_to_list : subst -> (IR.Ident.t * IR.Exp.t ) list
Convert a subst to a list of pairs.
val sub_empty : subst
The empty substitution.
val is_sub_empty : subst -> bool
val sub_join : subst -> subst -> subst
Compute the common id-exp part of two inputs subst1
and subst2
. The first component of the output is this common part. The second and third components are the remainder of subst1
and subst2
, respectively.
val sub_symmetric_difference : subst -> subst -> subst * subst * subst
Compute the common id-exp part of two inputs subst1
and subst2
. The first component of the output is this common part. The second and third components are the remainder of subst1
and subst2
, respectively.
val sub_find : (IR.Ident.t -> bool) -> subst -> IR.Exp.t
sub_find filter sub
returns the expression associated to the first identifier that satisfies filter
. Raise Not_found_s/Caml.Not_found
if there isn't one.
val sub_filter : (IR.Ident.t -> bool) -> subst -> subst
sub_filter filter sub
restricts the domain of sub
to the identifiers satisfying filter
.
val sub_filter_pair : subst -> f:((IR.Ident.t * IR.Exp.t ) -> bool) -> subst
sub_filter_exp filter sub
restricts the domain of sub
to the identifiers satisfying filter(id, sub(id))
.
val sub_range_partition : (IR.Exp.t -> bool) -> subst -> subst * subst
sub_range_partition filter sub
partitions sub
according to whether range expressions satisfy filter
.
val sub_domain_partition : (IR.Ident.t -> bool) -> subst -> subst * subst
sub_domain_partition filter sub
partitions sub
according to whether domain identifiers satisfy filter
.
val sub_domain : subst -> IR.Ident.t list
Return the list of identifiers in the domain of the substitution.
val sub_range : subst -> IR.Exp.t list
Return the list of expressions in the range of the substitution.
val sub_range_map : (IR.Exp.t -> IR.Exp.t ) -> subst -> subst
sub_range_map f sub
applies f
to the expressions in the range of sub
.
val sub_map : (IR.Ident.t -> IR.Ident.t ) -> (IR.Exp.t -> IR.Exp.t ) -> subst -> subst
sub_map f g sub
applies the renaming f
to identifiers in the domain of sub
and the substitution g
to the expressions in the range of sub
.
val extend_sub : subst -> IR.Ident.t -> IR.Exp.t -> subst option
Extend substitution and return None
if not possible.
val subst_free_vars : subst -> IR.Ident.t IStdlib.IStd .Sequence.t
val subst_gen_free_vars : subst -> (unit, IR.Ident.t ) IStdlib.IStd .Sequence.Generator.t
val exp_sub : subst -> IR.Exp.t -> IR.Exp.t
val atom_sub : subst -> atom -> atom
val instr_sub : subst -> IR.Sil.instr -> IR.Sil.instr
apply subst
to all id's in instr
, including LHS id's
val hpred_sub : subst -> hpred -> hpred
Functions for constructing or destructing entities in this moduleval exp_get_offsets : IR.Exp.t -> offset list
Compute the offset list of an expression
val exp_add_offsets : IR.Exp.t -> offset list -> IR.Exp.t
Add the offset list to an expression
val sigma_to_sigma_ne : hpred list -> (atom list * hpred list ) list
val hpara_instantiate : hpara -> IR.Exp.t -> IR.Exp.t -> IR.Exp.t list -> IR.Ident.t list * hpred list
hpara_instantiate para e1 e2 elist
instantiates para
with e1
, e2
and elist
. If para = lambda (x, y, xs). exists zs. b
, then the result of the instantiation is b[e1 / x, e2 / y, elist / xs, _zs'/ zs]
for some fresh _zs'
.
val hpara_dll_instantiate : hpara_dll -> IR.Exp.t -> IR.Exp.t -> IR.Exp.t -> IR.Exp.t list -> IR.Ident.t list * hpred list
hpara_dll_instantiate para cell blink flink elist
instantiates para
with cell
, blink
, flink
, and elist
. If para = lambda (x, y, z, xs). exists zs. b
, then the result of the instantiation is b[cell / x, blink / y, flink / z, elist / xs, _zs'/ zs]
for some fresh _zs'
.
val custom_error : IR.Pvar.t
\ No newline at end of file
diff --git a/website/static/odoc/next/infer/Biabduction__Predicates/index.html b/website/static/odoc/next/infer/Biabduction__Predicates/index.html
index f6f48652e..da3de9f98 100644
--- a/website/static/odoc/next/infer/Biabduction__Predicates/index.html
+++ b/website/static/odoc/next/infer/Biabduction__Predicates/index.html
@@ -1,2 +1,2 @@
-Biabduction__Predicates (infer.Biabduction__Predicates) Up – infer » Biabduction__PredicatesModule Biabduction__Predicates
type offset
=
Offset for an lvalue.
Components of Propositionstype atom
=
an atom is a pure atomic formula
val equal_atom : atom -> atom -> bool
val atom_has_local_addr : atom -> bool
type lseg_kind
=
|
Lseg_NE
nonempty (possibly circular) listseg
|
Lseg_PE
possibly empty (possibly circular) listseg
kind of lseg or dllseg predicates
val equal_lseg_kind : lseg_kind -> lseg_kind -> bool
type zero_flag
= bool option
The boolean is true when the pointer was dereferenced without testing for zero.
type null_case_flag
= bool
True when the value was obtained by doing case analysis on null in a procedure call.
type inst
=
instrumentation of heap values
val equal_inst : inst -> inst -> bool
val inst_actual_precondition : inst
val inst_formal : inst
val inst_initial : inst
for formal parameters and heap values at the beginning of the function
val inst_lookup : inst
for initial values
val inst_none : inst
val inst_nullify : inst
val inst_rearrange : bool -> IBase.Location.t -> IR.PredSymb.path_pos -> inst
the boolean indicates whether the pointer is known nonzero
val inst_update : IBase.Location.t -> IR.PredSymb.path_pos -> inst
val inst_set_null_case_flag : inst -> inst
Set the null case flag of the inst.
val inst_new_loc : IBase.Location.t -> inst -> inst
update the location of the instrumentation
val update_inst : inst -> inst -> inst
Update inst_old
to inst_new
preserving the zero flag
exception
JoinFail
val inst_partial_join : inst -> inst -> inst
join of instrumentations, can raise JoinFail
val inst_partial_meet : inst -> inst -> inst
meet of instrumentations
type 'inst strexp0
=
|
Eexp of IR.Exp.t * 'inst
Base case: expression with instrumentation
|
Estruct of (IR.Fieldname.t * 'inst strexp0 ) list * 'inst
C structure
|
Earray of IR.Exp.t * (IR.Exp.t * 'inst strexp0 ) list * 'inst
Array of given length There are two conditions imposed / used in the array case. First, if some index and value pair appears inside an array in a strexp, then the index is less than the length of the array. For instance, x |->[10 | e1: v1]
implies that e1 <= 9
. Second, if two indices appear in an array, they should be different. For instance, x |->[10 | e1: v1, e2: v2]
implies that e1 != e2
.
structured expressions represent a value of structured type, such as an array or a struct.
val compare_strexp0 : ('inst -> 'inst -> int) -> 'inst strexp0 -> 'inst strexp0 -> int
type strexp
= inst strexp0
val compare_strexp : ?inst:bool -> strexp -> strexp -> int
Comparison function for strexp. The inst:: parameter specifies whether instumentations should also be considered (false by default).
val equal_strexp : ?inst:bool -> strexp -> strexp -> bool
Equality function for strexp. The inst:: parameter specifies whether instumentations should also be considered (false by default).
type 'inst hpred0
=
|
Hpointsto of IR.Exp.t * 'inst strexp0 * IR.Exp.t
represents exp|->strexp:typexp
where typexp
is an expression representing a type, e.h. sizeof(t)
.
|
Hlseg of lseg_kind * 'inst hpara0 * IR.Exp.t * IR.Exp.t * IR.Exp.t list
higher - order predicate for singly - linked lists. Should ensure that exp1!= exp2 implies that exp1 is allocated. This assumption is used in the rearrangement. The last exp list
parameter is used to denote the shared links by all the nodes in the list.
|
Hdllseg of lseg_kind * 'inst hpara_dll0 * IR.Exp.t * IR.Exp.t * IR.Exp.t * IR.Exp.t * IR.Exp.t list
higher-order predicate for doubly-linked lists. Parameter for the higher-order singly-linked list predicate. Means "lambda (root,next,svars). Exists evars. body". Assume that root, next, svars, evars are disjoint sets of primed identifiers, and include all the free primed identifiers in body. body should not contain any non - primed identifiers or program variables (i.e. pvars).
an atomic heap predicate
and 'inst hpara0
=
{
}
and 'inst hpara_dll0
=
{
}
parameter for the higher-order doubly-linked list predicates. Assume that all the free identifiers in body_dll should belong to cell, blink, flink, svars_dll, evars_dll.
val compare_hpred0 : ('inst -> 'inst -> int) -> 'inst hpred0 -> 'inst hpred0 -> int
val compare_hpara0 : ('inst -> 'inst -> int) -> 'inst hpara0 -> 'inst hpara0 -> int
val compare_hpara_dll0 : ('inst -> 'inst -> int) -> 'inst hpara_dll0 -> 'inst hpara_dll0 -> int
val compare_hpred0 : ('inst -> 'inst -> int) -> 'inst hpred0 -> 'inst hpred0 -> int
val compare_hpara0 : ('inst -> 'inst -> int) -> 'inst hpara0 -> 'inst hpara0 -> int
val compare_hpara_dll0 : ('inst -> 'inst -> int) -> 'inst hpara_dll0 -> 'inst hpara_dll0 -> int
val compare_hpred0 : ('inst -> 'inst -> int) -> 'inst hpred0 -> 'inst hpred0 -> int
val compare_hpara0 : ('inst -> 'inst -> int) -> 'inst hpara0 -> 'inst hpara0 -> int
val compare_hpara_dll0 : ('inst -> 'inst -> int) -> 'inst hpara_dll0 -> 'inst hpara_dll0 -> int
type hpred
= inst hpred0
type hpara
= inst hpara0
type hpara_dll
= inst hpara_dll0
val compare_hpred : ?inst:bool -> hpred -> hpred -> int
Comparison function for hpred. The inst:: parameter specifies whether instumentations should also be considered (false by default).
val equal_hpred : ?inst:bool -> hpred -> hpred -> bool
Equality function for hpred. The inst:: parameter specifies whether instumentations should also be considered (false by default).
module HpredSet : IStdlib.IStd .Caml.Set.S with type HpredSet .elt = hpred
Sets of heap predicates
type sharing_env
val create_sharing_env : unit -> sharing_env
Create a sharing env to store canonical representations
val hpred_compact : sharing_env -> hpred -> hpred
Return a compact representation of the exp
val is_objc_object : hpred -> bool
Comparision And Inspection Functionsval pp_offset : IStdlib.Pp.env -> F .formatter -> offset -> unit
val d_offset_list : offset list -> unit
Dump a list of offsets
val pp_atom : IStdlib.Pp.env -> F .formatter -> atom -> unit
Pretty print an atom.
val d_atom : atom -> unit
Dump an atom.
val pp_inst : F .formatter -> inst -> unit
pretty-print an inst
val pp_sexp : IStdlib.Pp.env -> F .formatter -> strexp -> unit
Pretty print a strexp.
val d_sexp : strexp -> unit
Dump a strexp.
val pp_hpred : IStdlib.Pp.env -> F .formatter -> hpred -> unit
Pretty print a hpred.
val d_hpred : hpred -> unit
Dump a hpred.
val pp_hpara : IStdlib.Pp.env -> F .formatter -> hpara -> unit
Pretty print a hpara.
val pp_hpara_dll : IStdlib.Pp.env -> F .formatter -> hpara_dll -> unit
Pretty print a hpara_dll.
module Env : sig ... end
record the occurrences of predicates as parameters of (doubly -)linked lists and Epara. Provides unique numbering for predicates and an iterator.
val pp_hpred_env : IStdlib.Pp.env -> Env.t option -> F .formatter -> hpred -> unit
Pretty print a hpred with optional predicate env
type subst
= private (IR.Ident.t * IR.Exp.t ) list
val equal_subst : subst -> subst -> bool
Equality for substitutions.
val subst_of_list : (IR.Ident.t * IR.Exp.t ) list -> subst
Create a substitution from a list of pairs. For all (id1, e1), (id2, e2) in the input list, if id1 = id2, then e1 = e2.
val subst_of_list_duplicates : (IR.Ident.t * IR.Exp.t ) list -> subst
like subst_of_list, but allow duplicate ids and only keep the first occurrence
val sub_to_list : subst -> (IR.Ident.t * IR.Exp.t ) list
Convert a subst to a list of pairs.
val sub_empty : subst
The empty substitution.
val is_sub_empty : subst -> bool
val sub_join : subst -> subst -> subst
Compute the common id-exp part of two inputs subst1
and subst2
. The first component of the output is this common part. The second and third components are the remainder of subst1
and subst2
, respectively.
val sub_symmetric_difference : subst -> subst -> subst * subst * subst
Compute the common id-exp part of two inputs subst1
and subst2
. The first component of the output is this common part. The second and third components are the remainder of subst1
and subst2
, respectively.
val sub_find : (IR.Ident.t -> bool) -> subst -> IR.Exp.t
sub_find filter sub
returns the expression associated to the first identifier that satisfies filter
. Raise Not_found_s/Caml.Not_found
if there isn't one.
val sub_filter : (IR.Ident.t -> bool) -> subst -> subst
sub_filter filter sub
restricts the domain of sub
to the identifiers satisfying filter
.
val sub_filter_pair : subst -> f:((IR.Ident.t * IR.Exp.t ) -> bool) -> subst
sub_filter_exp filter sub
restricts the domain of sub
to the identifiers satisfying filter(id, sub(id))
.
val sub_range_partition : (IR.Exp.t -> bool) -> subst -> subst * subst
sub_range_partition filter sub
partitions sub
according to whether range expressions satisfy filter
.
val sub_domain_partition : (IR.Ident.t -> bool) -> subst -> subst * subst
sub_domain_partition filter sub
partitions sub
according to whether domain identifiers satisfy filter
.
val sub_domain : subst -> IR.Ident.t list
Return the list of identifiers in the domain of the substitution.
val sub_range : subst -> IR.Exp.t list
Return the list of expressions in the range of the substitution.
val sub_range_map : (IR.Exp.t -> IR.Exp.t ) -> subst -> subst
sub_range_map f sub
applies f
to the expressions in the range of sub
.
val sub_map : (IR.Ident.t -> IR.Ident.t ) -> (IR.Exp.t -> IR.Exp.t ) -> subst -> subst
sub_map f g sub
applies the renaming f
to identifiers in the domain of sub
and the substitution g
to the expressions in the range of sub
.
val extend_sub : subst -> IR.Ident.t -> IR.Exp.t -> subst option
Extend substitution and return None
if not possible.
val subst_free_vars : subst -> IR.Ident.t IStdlib.IStd .Sequence.t
val subst_gen_free_vars : subst -> (unit, IR.Ident.t ) IStdlib.IStd .Sequence.Generator.t
val exp_sub : subst -> IR.Exp.t -> IR.Exp.t
val atom_sub : subst -> atom -> atom
val instr_sub : subst -> IR.Sil.instr -> IR.Sil.instr
apply subst
to all id's in instr
, including LHS id's
val hpred_sub : subst -> hpred -> hpred
Functions for constructing or destructing entities in this moduleval exp_get_offsets : IR.Exp.t -> offset list
Compute the offset list of an expression
val exp_add_offsets : IR.Exp.t -> offset list -> IR.Exp.t
Add the offset list to an expression
val sigma_to_sigma_ne : hpred list -> (atom list * hpred list ) list
val hpara_instantiate : hpara -> IR.Exp.t -> IR.Exp.t -> IR.Exp.t list -> IR.Ident.t list * hpred list
hpara_instantiate para e1 e2 elist
instantiates para
with e1
, e2
and elist
. If para = lambda (x, y, xs). exists zs. b
, then the result of the instantiation is b[e1 / x, e2 / y, elist / xs, _zs'/ zs]
for some fresh _zs'
.
val hpara_dll_instantiate : hpara_dll -> IR.Exp.t -> IR.Exp.t -> IR.Exp.t -> IR.Exp.t list -> IR.Ident.t list * hpred list
hpara_dll_instantiate para cell blink flink elist
instantiates para
with cell
, blink
, flink
, and elist
. If para = lambda (x, y, z, xs). exists zs. b
, then the result of the instantiation is b[cell / x, blink / y, flink / z, elist / xs, _zs'/ zs]
for some fresh _zs'
.
val custom_error : IR.Pvar.t
\ No newline at end of file
+Biabduction__Predicates (infer.Biabduction__Predicates) Up – infer » Biabduction__PredicatesModule Biabduction__Predicates
type offset
=
Offset for an lvalue.
Components of Propositionstype atom
=
an atom is a pure atomic formula
val equal_atom : atom -> atom -> bool
val atom_has_local_addr : atom -> bool
type lseg_kind
=
|
Lseg_NE
nonempty (possibly circular) listseg
|
Lseg_PE
possibly empty (possibly circular) listseg
kind of lseg or dllseg predicates
val equal_lseg_kind : lseg_kind -> lseg_kind -> bool
type zero_flag
= bool option
The boolean is true when the pointer was dereferenced without testing for zero.
type null_case_flag
= bool
True when the value was obtained by doing case analysis on null in a procedure call.
type inst
=
instrumentation of heap values
val equal_inst : inst -> inst -> bool
val inst_actual_precondition : inst
val inst_formal : inst
val inst_initial : inst
for formal parameters and heap values at the beginning of the function
val inst_lookup : inst
for initial values
val inst_none : inst
val inst_nullify : inst
val inst_rearrange : bool -> IBase.Location.t -> IR.PredSymb.path_pos -> inst
the boolean indicates whether the pointer is known nonzero
val inst_update : IBase.Location.t -> IR.PredSymb.path_pos -> inst
val inst_set_null_case_flag : inst -> inst
Set the null case flag of the inst.
val inst_new_loc : IBase.Location.t -> inst -> inst
update the location of the instrumentation
val update_inst : inst -> inst -> inst
Update inst_old
to inst_new
preserving the zero flag
exception
JoinFail
val inst_partial_join : inst -> inst -> inst
join of instrumentations, can raise JoinFail
val inst_partial_meet : inst -> inst -> inst
meet of instrumentations
type 'inst strexp0
=
|
Eexp of IR.Exp.t * 'inst
Base case: expression with instrumentation
|
Estruct of (IR.Fieldname.t * 'inst strexp0 ) list * 'inst
C structure
|
Earray of IR.Exp.t * (IR.Exp.t * 'inst strexp0 ) list * 'inst
Array of given length There are two conditions imposed / used in the array case. First, if some index and value pair appears inside an array in a strexp, then the index is less than the length of the array. For instance, x |->[10 | e1: v1]
implies that e1 <= 9
. Second, if two indices appear in an array, they should be different. For instance, x |->[10 | e1: v1, e2: v2]
implies that e1 != e2
.
structured expressions represent a value of structured type, such as an array or a struct.
val compare_strexp0 : ('inst -> 'inst -> int) -> 'inst strexp0 -> 'inst strexp0 -> int
type strexp
= inst strexp0
val compare_strexp : ?inst:bool -> strexp -> strexp -> int
Comparison function for strexp. The inst:: parameter specifies whether instumentations should also be considered (false by default).
val equal_strexp : ?inst:bool -> strexp -> strexp -> bool
Equality function for strexp. The inst:: parameter specifies whether instumentations should also be considered (false by default).
type 'inst hpred0
=
|
Hpointsto of IR.Exp.t * 'inst strexp0 * IR.Exp.t
represents exp|->strexp:typexp
where typexp
is an expression representing a type, e.h. sizeof(t)
.
|
Hlseg of lseg_kind * 'inst hpara0 * IR.Exp.t * IR.Exp.t * IR.Exp.t list
higher - order predicate for singly - linked lists. Should ensure that exp1!= exp2 implies that exp1 is allocated. This assumption is used in the rearrangement. The last exp list
parameter is used to denote the shared links by all the nodes in the list.
|
Hdllseg of lseg_kind * 'inst hpara_dll0 * IR.Exp.t * IR.Exp.t * IR.Exp.t * IR.Exp.t * IR.Exp.t list
higher-order predicate for doubly-linked lists. Parameter for the higher-order singly-linked list predicate. Means "lambda (root,next,svars). Exists evars. body". Assume that root, next, svars, evars are disjoint sets of primed identifiers, and include all the free primed identifiers in body. body should not contain any non - primed identifiers or program variables (i.e. pvars).
an atomic heap predicate
and 'inst hpara0
=
{
}
and 'inst hpara_dll0
=
{
}
parameter for the higher-order doubly-linked list predicates. Assume that all the free identifiers in body_dll should belong to cell, blink, flink, svars_dll, evars_dll.
val compare_hpred0 : ('inst -> 'inst -> int) -> 'inst hpred0 -> 'inst hpred0 -> int
val compare_hpara0 : ('inst -> 'inst -> int) -> 'inst hpara0 -> 'inst hpara0 -> int
val compare_hpara_dll0 : ('inst -> 'inst -> int) -> 'inst hpara_dll0 -> 'inst hpara_dll0 -> int
val compare_hpred0 : ('inst -> 'inst -> int) -> 'inst hpred0 -> 'inst hpred0 -> int
val compare_hpara0 : ('inst -> 'inst -> int) -> 'inst hpara0 -> 'inst hpara0 -> int
val compare_hpara_dll0 : ('inst -> 'inst -> int) -> 'inst hpara_dll0 -> 'inst hpara_dll0 -> int
val compare_hpred0 : ('inst -> 'inst -> int) -> 'inst hpred0 -> 'inst hpred0 -> int
val compare_hpara0 : ('inst -> 'inst -> int) -> 'inst hpara0 -> 'inst hpara0 -> int
val compare_hpara_dll0 : ('inst -> 'inst -> int) -> 'inst hpara_dll0 -> 'inst hpara_dll0 -> int
type hpred
= inst hpred0
type hpara
= inst hpara0
type hpara_dll
= inst hpara_dll0
val compare_hpred : ?inst:bool -> hpred -> hpred -> int
Comparison function for hpred. The inst:: parameter specifies whether instumentations should also be considered (false by default).
val equal_hpred : ?inst:bool -> hpred -> hpred -> bool
Equality function for hpred. The inst:: parameter specifies whether instumentations should also be considered (false by default).
module HpredSet : IStdlib.IStd .Caml.Set.S with type HpredSet .elt = hpred
Sets of heap predicates
type sharing_env
val create_sharing_env : unit -> sharing_env
Create a sharing env to store canonical representations
val hpred_compact : sharing_env -> hpred -> hpred
Return a compact representation of the exp
val is_objc_object : hpred -> bool
Comparision And Inspection Functionsval pp_offset : IStdlib.Pp.env -> F .formatter -> offset -> unit
val d_offset_list : offset list -> unit
Dump a list of offsets
val pp_atom : IStdlib.Pp.env -> F .formatter -> atom -> unit
Pretty print an atom.
val d_atom : atom -> unit
Dump an atom.
val pp_inst : F .formatter -> inst -> unit
pretty-print an inst
val pp_sexp : IStdlib.Pp.env -> F .formatter -> strexp -> unit
Pretty print a strexp.
val d_sexp : strexp -> unit
Dump a strexp.
val pp_hpred : IStdlib.Pp.env -> F .formatter -> hpred -> unit
Pretty print a hpred.
val d_hpred : hpred -> unit
Dump a hpred.
val pp_hpara : IStdlib.Pp.env -> F .formatter -> hpara -> unit
Pretty print a hpara.
val pp_hpara_dll : IStdlib.Pp.env -> F .formatter -> hpara_dll -> unit
Pretty print a hpara_dll.
module Env : sig ... end
record the occurrences of predicates as parameters of (doubly -)linked lists and Epara. Provides unique numbering for predicates and an iterator.
val pp_hpred_env : IStdlib.Pp.env -> Env.t option -> F .formatter -> hpred -> unit
Pretty print a hpred with optional predicate env
type subst
= private (IR.Ident.t * IR.Exp.t ) list
val equal_subst : subst -> subst -> bool
Equality for substitutions.
val subst_of_list : (IR.Ident.t * IR.Exp.t ) list -> subst
Create a substitution from a list of pairs. For all (id1, e1), (id2, e2) in the input list, if id1 = id2, then e1 = e2.
val subst_of_list_duplicates : (IR.Ident.t * IR.Exp.t ) list -> subst
like subst_of_list, but allow duplicate ids and only keep the first occurrence
val sub_to_list : subst -> (IR.Ident.t * IR.Exp.t ) list
Convert a subst to a list of pairs.
val sub_empty : subst
The empty substitution.
val is_sub_empty : subst -> bool
val sub_join : subst -> subst -> subst
Compute the common id-exp part of two inputs subst1
and subst2
. The first component of the output is this common part. The second and third components are the remainder of subst1
and subst2
, respectively.
val sub_symmetric_difference : subst -> subst -> subst * subst * subst
Compute the common id-exp part of two inputs subst1
and subst2
. The first component of the output is this common part. The second and third components are the remainder of subst1
and subst2
, respectively.
val sub_find : (IR.Ident.t -> bool) -> subst -> IR.Exp.t
sub_find filter sub
returns the expression associated to the first identifier that satisfies filter
. Raise Not_found_s/Caml.Not_found
if there isn't one.
val sub_filter : (IR.Ident.t -> bool) -> subst -> subst
sub_filter filter sub
restricts the domain of sub
to the identifiers satisfying filter
.
val sub_filter_pair : subst -> f:((IR.Ident.t * IR.Exp.t ) -> bool) -> subst
sub_filter_exp filter sub
restricts the domain of sub
to the identifiers satisfying filter(id, sub(id))
.
val sub_range_partition : (IR.Exp.t -> bool) -> subst -> subst * subst
sub_range_partition filter sub
partitions sub
according to whether range expressions satisfy filter
.
val sub_domain_partition : (IR.Ident.t -> bool) -> subst -> subst * subst
sub_domain_partition filter sub
partitions sub
according to whether domain identifiers satisfy filter
.
val sub_domain : subst -> IR.Ident.t list
Return the list of identifiers in the domain of the substitution.
val sub_range : subst -> IR.Exp.t list
Return the list of expressions in the range of the substitution.
val sub_range_map : (IR.Exp.t -> IR.Exp.t ) -> subst -> subst
sub_range_map f sub
applies f
to the expressions in the range of sub
.
val sub_map : (IR.Ident.t -> IR.Ident.t ) -> (IR.Exp.t -> IR.Exp.t ) -> subst -> subst
sub_map f g sub
applies the renaming f
to identifiers in the domain of sub
and the substitution g
to the expressions in the range of sub
.
val extend_sub : subst -> IR.Ident.t -> IR.Exp.t -> subst option
Extend substitution and return None
if not possible.
val subst_free_vars : subst -> IR.Ident.t IStdlib.IStd .Sequence.t
val subst_gen_free_vars : subst -> (unit, IR.Ident.t ) IStdlib.IStd .Sequence.Generator.t
val exp_sub : subst -> IR.Exp.t -> IR.Exp.t
val atom_sub : subst -> atom -> atom
val instr_sub : subst -> IR.Sil.instr -> IR.Sil.instr
apply subst
to all id's in instr
, including LHS id's
val hpred_sub : subst -> hpred -> hpred
Functions for constructing or destructing entities in this moduleval exp_get_offsets : IR.Exp.t -> offset list
Compute the offset list of an expression
val exp_add_offsets : IR.Exp.t -> offset list -> IR.Exp.t
Add the offset list to an expression
val sigma_to_sigma_ne : hpred list -> (atom list * hpred list ) list
val hpara_instantiate : hpara -> IR.Exp.t -> IR.Exp.t -> IR.Exp.t list -> IR.Ident.t list * hpred list
hpara_instantiate para e1 e2 elist
instantiates para
with e1
, e2
and elist
. If para = lambda (x, y, xs). exists zs. b
, then the result of the instantiation is b[e1 / x, e2 / y, elist / xs, _zs'/ zs]
for some fresh _zs'
.
val hpara_dll_instantiate : hpara_dll -> IR.Exp.t -> IR.Exp.t -> IR.Exp.t -> IR.Exp.t list -> IR.Ident.t list * hpred list
hpara_dll_instantiate para cell blink flink elist
instantiates para
with cell
, blink
, flink
, and elist
. If para = lambda (x, y, z, xs). exists zs. b
, then the result of the instantiation is b[cell / x, blink / y, flink / z, elist / xs, _zs'/ zs]
for some fresh _zs'
.
val custom_error : IR.Pvar.t
\ No newline at end of file
diff --git a/website/static/odoc/next/infer/IBase/Checker/index.html b/website/static/odoc/next/infer/IBase/Checker/index.html
index dbed5f7cd..b2ad7db3d 100644
--- a/website/static/odoc/next/infer/IBase/Checker/index.html
+++ b/website/static/odoc/next/infer/IBase/Checker/index.html
@@ -1,2 +1,2 @@
-Checker (infer.IBase.Checker) type t
=
|
AnnotationReachability
|
Biabduction
|
BufferOverrunAnalysis
|
BufferOverrunChecker
|
ConfigChecksBetweenMarkers
|
ConfigImpactAnalysis
|
Cost
|
Eradicate
|
FragmentRetainsView
|
ImmutableCast
|
Impurity
|
InefficientKeysetIterator
|
Linters
|
LithoRequiredProps
|
Liveness
|
LoopHoisting
|
NullsafeDeprecated
|
PrintfArgs
|
Pulse
|
PurityAnalysis
|
PurityChecker
|
Quandary
|
RacerD
|
ResourceLeakLabExercise
|
DOTNETResourceLeaks
|
SIOF
|
SelfInBlock
|
Starvation
|
ToplOnBiabduction
|
ToplOnPulse
|
Uninit
val equal : t -> t -> bool
val all : t list
type support
=
|
NoSupport
checker does not run at all for this language
|
ExperimentalSupport
checker runs but is not expected to give reasonable results
|
Support
checker is expected to give reasonable results
per-language support for each checker
type cli_flags
=
{
deprecated : string list ;
More command-line flags, similar to ~deprecated
arguments in CommandLineOption
.
show_in_help : bool;
}
type kind
=
|
UserFacing of
{
title : string;
the title of the documentation web page
markdown_body : string;
main text of the documentation
}
can report issues to users
|
UserFacingDeprecated of
{
title : string;
the title of the documentation web page
markdown_body : string;
main text of the documentation
deprecation_message : string;
}
can report issues to users but should probably be deleted from infer
|
Internal
Analysis that only serves other analyses. Do not use to mean experimental! Please still document experimental checkers as they will become non-experimental.
|
Exercise
reserved for the "resource leak" lab exercise
type config
=
{
id : string;
Unique identifier. Used to generate web URLs for the documentation as well as the flag to enable this option on the command line.
kind : kind ;
support : Language.t -> support ;
short_documentation : string;
used in man pages and as a short intro on the website
cli_flags : cli_flags option ;
If None
then the checker cannot be enabled/disabled from the command line.
enabled_by_default : bool;
activates : t list ;
list of checkers that get enabled when this checker is enabled
}
val config : t -> config
val get_id : t -> string
get_id c
is (config c).id
val from_id : string -> t option
\ No newline at end of file
+Checker (infer.IBase.Checker) type t
=
|
AnnotationReachability
|
Biabduction
|
BufferOverrunAnalysis
|
BufferOverrunChecker
|
ConfigChecksBetweenMarkers
|
ConfigImpactAnalysis
|
Cost
|
Eradicate
|
FragmentRetainsView
|
ImmutableCast
|
Impurity
|
InefficientKeysetIterator
|
Linters
|
LithoRequiredProps
|
Liveness
|
LoopHoisting
|
NullsafeDeprecated
|
PrintfArgs
|
Pulse
|
PurityAnalysis
|
PurityChecker
|
Quandary
|
RacerD
|
ResourceLeakLabExercise
|
DOTNETResourceLeaks
|
SIOF
|
SelfInBlock
|
Starvation
|
TOPL
|
Uninit
val equal : t -> t -> bool
val all : t list
type support
=
|
NoSupport
checker does not run at all for this language
|
ExperimentalSupport
checker runs but is not expected to give reasonable results
|
Support
checker is expected to give reasonable results
per-language support for each checker
type cli_flags
=
{
deprecated : string list ;
More command-line flags, similar to ~deprecated
arguments in CommandLineOption
.
show_in_help : bool;
}
type kind
=
|
UserFacing of
{
title : string;
the title of the documentation web page
markdown_body : string;
main text of the documentation
}
can report issues to users
|
UserFacingDeprecated of
{
title : string;
the title of the documentation web page
markdown_body : string;
main text of the documentation
deprecation_message : string;
}
can report issues to users but should probably be deleted from infer
|
Internal
Analysis that only serves other analyses. Do not use to mean experimental! Please still document experimental checkers as they will become non-experimental.
|
Exercise
reserved for the "resource leak" lab exercise
type config
=
{
id : string;
Unique identifier. Used to generate web URLs for the documentation as well as the flag to enable this option on the command line.
kind : kind ;
support : Language.t -> support ;
short_documentation : string;
used in man pages and as a short intro on the website
cli_flags : cli_flags option ;
If None
then the checker cannot be enabled/disabled from the command line.
enabled_by_default : bool;
activates : t list ;
list of checkers that get enabled when this checker is enabled
}
val config : t -> config
val get_id : t -> string
get_id c
is (config c).id
val from_id : string -> t option
\ No newline at end of file
diff --git a/website/static/odoc/next/infer/IBase/Config/index.html b/website/static/odoc/next/infer/IBase/Config/index.html
index deacef9f1..f5b8e31bd 100644
--- a/website/static/odoc/next/infer/IBase/Config/index.html
+++ b/website/static/odoc/next/infer/IBase/Config/index.html
@@ -1,2 +1,2 @@
-Config (infer.IBase.Config) Configuration values: either constant, determined at compile time, or set at startup time by system calls, environment variables, or command line options
type os_type
=
type build_system
=
|
BAnt
|
BBuck
|
BClang
|
BGradle
|
BJava
|
BJavac
|
BMake
|
BMvn
|
BNdk
|
BXcode
type scheduler
=
|
File
|
Restart
|
SyntacticCallGraph
val build_system_of_exe_name : string -> build_system
val string_of_build_system : build_system -> string
val env_inside_maven : IStdlib.IStd .Unix.env
Constant configuration valuesval anonymous_block_num_sep : string
val anonymous_block_prefix : string
val append_buck_flavors : string list
val assign : string
val biabduction_models_sql : string
val biabduction_models_jar : string
val bin_dir : string
val bound_error_allowed_in_procedure_call : bool
val buck_java_flavor_suppress_config : bool
val clang_exe_aliases : string list
val clang_initializer_prefix : string
val clang_inner_destructor_prefix : string
val clang_plugin_path : string
val classpath : string option
val default_failure_name : string
val dotty_frontend_output : string
val etc_dir : string
val fail_on_issue_exit_code : int
val fcp_dir : string
val idempotent_getters : bool
val initial_analysis_time : float
val ivar_attributes : string
val java_lambda_marker_infix : string
marker to recognize methods generated by javalib to eliminate lambdas
val lib_dir : string
val load_average : float option
val max_narrows : int
val max_widens : int
val meet_level : int
val nsnotification_center_checker_backend : bool
val os_type : os_type
val passthroughs : bool
val patterns_modeled_expensive : string * Yojson.Basic.t
val patterns_never_returning_null : string * Yojson.Basic.t
val patterns_skip_implementation : string * Yojson.Basic.t
val patterns_skip_translation : string * Yojson.Basic.t
val pp_version : Stdlib.Format.formatter -> unit -> unit
val property_attributes : string
val relative_path_backtrack : int
val report : bool
val report_custom_error : bool
val report_force_relative_path : bool
val report_immutable_modifications : bool
val report_nullable_inconsistency : bool
val save_compact_summaries : bool
val smt_output : bool
val source_file_extentions : string list
val kotlin_source_extension : string
val sourcepath : string option
val sources : string list
val trace_absarray : bool
val unsafe_unret : string
val incremental_analysis : bool
val weak : string
val whitelisted_cpp_classes : string list
val whitelisted_cpp_methods : string list
val wrappers_dir : string
Configuration values specified by command-line optionsval abs_struct : int
val abs_val : int
val allow_leak : bool
val annotation_reachability_cxx : Yojson.Basic.t
val annotation_reachability_cxx_sources : Yojson.Basic.t
val annotation_reachability_custom_pairs : Yojson.Basic.t
val array_level : int
val biabduction_models_mode : bool
val bo_debug : int
val bo_field_depth_limit : int option
val bootclasspath : string option
val buck : bool
val buck_blacklist : string list
val buck_build_args : string list
val buck_build_args_no_inline : string list
val buck_cache_mode : bool
val buck_java_heap_size_gb : int option
val buck_merge_all_deps : bool
val buck_mode : BuckMode.t option
val buck_out_gen : string
val buck_targets_blacklist : string list
val call_graph_schedule : bool
val capture : bool
val capture_blacklist : string option
val cfg_json : string option
val censor_report : ((bool * Str.regexp) * (bool * Str.regexp) * string) list
val changed_files_index : string option
val check_version : string option
val clang_ast_file : [ `Biniou of string | `Yojson of string ] option
val clang_compound_literal_init_limit : int
val clang_blacklisted_flags : string list
val clang_blacklisted_flags_with_arg : string list
val clang_ignore_regex : string option
val clang_isystem_to_override_regex : Str.regexp option
val clang_idirafter_to_override_regex : Str.regexp option
val clang_libcxx_include_to_override_regex : string option
val command : ATDGenerated.InferCommand.t
val config_impact_current : string option
val config_impact_data_file : string option
val config_impact_issues_tests : string option
val config_impact_max_callees_to_print : int
val config_impact_previous : string option
val continue_analysis : bool
val continue_capture : bool
val costs_current : string option
val cost_issues_tests : string option
val cost_scuba_logging : bool
val costs_previous : string option
val cost_suppress_func_ptr : bool
val cost_tests_only_autoreleasepool : bool
val cxx : bool
val cxx_scope_guards : Yojson.Basic.t
val deduplicate : bool
val debug_exceptions : bool
val debug_level_analysis : int
val debug_level_capture : int
val debug_level_linters : int
val debug_level_test_determinator : int
val debug_mode : bool
val default_linters : bool
val dependency_mode : bool
val developer_mode : bool
val differential_filter_files : string option
val differential_filter_set : [ `Introduced | `Fixed | `Preexisting ] list
val dotty_cfg_libs : bool
val dump_duplicate_symbols : bool
val eradicate_condition_redundant : bool
val eradicate_field_over_annotated : bool
val eradicate_return_over_annotated : bool
val eradicate_verbose : bool
val fail_on_bug : bool
val fcp_apple_clang : string option
val fcp_syntax_only : bool
val file_renamings : string option
val filter_paths : bool
val filtering : bool
val force_delete_results_dir : bool
val force_integration : build_system option
val from_json_report : string
val from_json_config_impact_report : string
val from_json_costs_report : string
val frontend_stats : bool
val frontend_tests : bool
val function_pointer_specialization : bool
val generated_classes : string option
val genrule_mode : bool
val get_linter_doc_url : linter_id:string -> string option
val help_checker : Checker.t list
val help_issue_type : IssueType.t list
val hoisting_report_only_expensive : bool
val html : bool
val global_tenv : bool
val icfg_dotty_outfile : string option
val infer_is_clang : bool
val infer_is_javac : bool
val implicit_sdk_root : string option
val inclusive_cost : bool
val inferconfig_file : string option
val inferconfig_dir : string option
val is_checker_enabled : Checker.t -> bool
val issues_tests : string option
val issues_tests_fields : IssuesTestField.t list
val iterations : int
val java_debug_source_file_info : string option
val java_jar_compiler : string option
val java_source_parser_experimental : bool
val java_version : int option
val javac_classes_out : string
val job_id : string option
val jobs : int
val join_cond : int
val keep_going : bool
val linter : string option
val linters_def_file : string list
val linters_def_folder : string list
val linters_developer_mode : bool
val linters_ignore_clang_failures : bool
val linters_validate_syntax_only : bool
val list_checkers : bool
val list_issue_types : bool
val liveness_dangerous_classes : Yojson.Basic.t
val liveness_ignored_constant : string list
val max_nesting : int option
val memtrace_analysis : bool
val memtrace_sampling_rate : float
val merge : bool
val method_decls_info : string option
val ml_buckets : [ `MLeak_all | `MLeak_arc | `MLeak_cf | `MLeak_cpp | `MLeak_no_arc | `MLeak_unknown ] list
val modified_lines : string option
val monitor_prop_size : bool
val nelseg : bool
val no_translate_libs : bool
val nullable_annotation : string option
val nullsafe_annotation_graph : bool
val nullsafe_disable_field_not_initialized_in_nonstrict_classes : bool
val nullsafe_optimistic_third_party_in_default_mode : bool
val nullsafe_third_party_signatures : string option
val nullsafe_third_party_location_for_messaging_only : string option
val nullsafe_strict_containers : bool
val oom_threshold : int option
val only_cheap_debug : bool
val pmd_xml : bool
val print_active_checkers : bool
val print_builtins : bool
val print_jbir : bool
val print_logs : bool
val print_types : bool
val print_using_diff : bool
val procedures : bool
val procedures_attributes : bool
val procedures_cfg : bool
val procedures_definedness : bool
val procedures_filter : string option
val procedures_name : bool
val procedures_source_file : bool
val procedures_summary : bool
val procedures_summary_json : bool
val process_clang_ast : bool
val clang_frontend_action_string : string
val profiler_samples : string option
val progress_bar : [ `MultiLine | `Plain | `Quiet ]
val project_root : string
val pulse_cut_to_one_path_procedures_pattern : Str.regexp option
val pulse_intraprocedural_only : bool
val pulse_isl : bool
val pulse_max_disjuncts : int
val pulse_model_abort : string list
val pulse_model_alloc_pattern : Str.regexp option
val pulse_model_release_pattern : Str.regexp option
val pulse_model_return_nonnull : Str.regexp option
val pulse_model_skip_pattern : Str.regexp option
val pulse_report_ignore_unknown_java_methods_patterns : Str.regexp option
val pulse_model_transfer_ownership_namespace : (string * string) list
val pulse_model_transfer_ownership : string list
val pulse_report_latent_issues : bool
val pulse_recency_limit : int
val pulse_widen_threshold : int
val pulse_nullsafe_report_npe : bool
val pure_by_default : bool
val quandary_endpoints : Yojson.Basic.t
val quandary_sanitizers : Yojson.Basic.t
val quandary_sinks : Yojson.Basic.t
val quandary_sources : Yojson.Basic.t
val quiet : bool
val racerd_guardedby : bool
val reactive_mode : bool
val reanalyze : bool
val report_blacklist_files_containing : string list
val report_console_limit : int option
val report_current : string option
val report_formatter : [ `No_formatter | `Phabricator_formatter ]
val report_path_regex_blacklist : string list
val report_path_regex_whitelist : string list
val report_previous : string option
val report_suppress_errors : string list
val reports_include_ml_loc : bool
val rest : string list
val results_dir : string
val scheduler : scheduler
val scuba_logging : bool
val scuba_normals : string IStdlib.IStd .String.Map.t
val scuba_tags : string list IStdlib.IStd .String.Map.t
val seconds_per_iteration : float option
val select : [ `All | `Select of int ] option
val show_buckets : bool
val siof_check_iostreams : bool
val siof_safe_methods : string list
val skip_analysis_in_path : string list
val skip_analysis_in_path_skips_compilation : bool
val skip_duplicated_types : bool
val skip_non_capture_clang_commands : bool
val source_files : bool
val source_files_cfg : bool
val source_files_filter : string option
val source_files_freshly_captured : bool
val source_files_procedure_names : bool
val source_files_type_environment : bool
val source_preview : bool
val sqlite_cache_size : int
val sqlite_page_size : int
val sqlite_lock_timeout : int
val sqlite_vfs : string option
val starvation_skip_analysis : Yojson.Basic.t
val starvation_strict_mode : bool
val starvation_whole_program : bool
val subtype_multirange : bool
val summaries_caches_max_size : int
val suppress_lint_ignore_types : bool
val symops_per_iteration : int option
val tenv_json : string option
val test_determinator : bool
val export_changed_functions : bool
val test_filtering : bool
val testing_mode : bool
val threadsafe_aliases : Yojson.Basic.t
val topl_max_conjuncts : int
val topl_max_disjuncts : int
val topl_properties : string list
val trace_error : bool
val trace_events : bool
val trace_join : bool
val trace_ondemand : bool
val trace_rearrange : bool
val trace_topl : bool
val tv_commit : string option
val tv_limit : int
val tv_limit_filtered : int
val type_size : bool
val uninit_interproc : bool
val unsafe_malloc : bool
val worklist_mode : int
val workspace : string option
val write_dotty : bool
val write_html : bool
val write_html_whitelist_regex : string list
val write_website : string option
val xcode_developer_dir : string option
val xcode_isysroot_suffix : string option
val xcpretty : bool
Configuration values derived from command-line optionsval dynamic_dispatch : bool
val toplevel_results_dir : string
In some integrations, eg Buck, infer subprocesses started by the build system (started by the toplevel infer process) will have their own results directory; this points to the results directory of the toplevel infer process, which can be useful for, eg, storing debug info. In other cases this is equal to results_dir
.
val is_in_custom_symbols : string -> string -> bool
Does named symbol match any prefix in the named custom symbol list?
val java_package_is_external : string -> bool
Check if a Java package is external to the repository
val scuba_execution_id : IStdlib.IStd .Int64.t option
a random number to (hopefully) uniquely identify this run
Global variables with initial values specified by command-line optionsval clang_compilation_dbs : [ `Escaped of string | `Raw of string ] list
\ No newline at end of file
+Config (infer.IBase.Config) Configuration values: either constant, determined at compile time, or set at startup time by system calls, environment variables, or command line options
type os_type
=
type build_system
=
|
BAnt
|
BBuck
|
BClang
|
BGradle
|
BJava
|
BJavac
|
BMake
|
BMvn
|
BNdk
|
BXcode
type scheduler
=
|
File
|
Restart
|
SyntacticCallGraph
val build_system_of_exe_name : string -> build_system
val string_of_build_system : build_system -> string
val env_inside_maven : IStdlib.IStd .Unix.env
Constant configuration valuesval anonymous_block_num_sep : string
val anonymous_block_prefix : string
val assign : string
val biabduction_models_sql : string
val biabduction_models_jar : string
val bin_dir : string
val bound_error_allowed_in_procedure_call : bool
val clang_exe_aliases : string list
val clang_initializer_prefix : string
val clang_inner_destructor_prefix : string
val clang_plugin_path : string
val default_failure_name : string
val dotty_frontend_output : string
val etc_dir : string
val fail_on_issue_exit_code : int
val fcp_dir : string
val idempotent_getters : bool
val initial_analysis_time : float
val ivar_attributes : string
val java_lambda_marker_infix : string
marker to recognize methods generated by javalib to eliminate lambdas
val kotlin_source_extension : string
val lib_dir : string
val max_narrows : int
val max_widens : int
val meet_level : int
val nsnotification_center_checker_backend : bool
val os_type : os_type
val pp_version : Stdlib.Format.formatter -> unit -> unit
val property_attributes : string
val report_nullable_inconsistency : bool
val save_compact_summaries : bool
val smt_output : bool
val source_file_extentions : string list
val unsafe_unret : string
val weak : string
val whitelisted_cpp_classes : string list
val whitelisted_cpp_methods : string list
val wrappers_dir : string
Configuration values specified by command-line optionsval annotation_reachability_cxx : Yojson.Basic.t
val annotation_reachability_cxx_sources : Yojson.Basic.t
val annotation_reachability_custom_pairs : Yojson.Basic.t
val append_buck_flavors : string list
val biabduction_abs_struct : int
val biabduction_abs_val : int
val biabduction_allow_leak : bool
val biabduction_array_level : int
val biabduction_models_mode : bool
val biabduction_iterations : int
val biabduction_join_cond : int
val biabduction_memleak_buckets : [ `MLeak_all | `MLeak_arc | `MLeak_cf | `MLeak_cpp | `MLeak_no_arc | `MLeak_unknown ] list
val biabduction_monitor_prop_size : bool
val biabduction_nelseg : bool
val biabduction_seconds_per_iteration : float option
val biabduction_symops_per_iteration : int option
val biabduction_trace_join : bool
val biabduction_trace_rearrange : bool
val biabduction_type_size : bool
val biabduction_unsafe_malloc : bool
val biabduction_worklist_mode : int
val biabduction_write_dotty : bool
val bo_debug : int
val bo_field_depth_limit : int option
val bootclasspath : string option
val buck : bool
val buck_blacklist : string list
val buck_build_args : string list
val buck_build_args_no_inline : string list
val buck_cache_mode : bool
val buck_java_flavor_suppress_config : bool
val buck_java_heap_size_gb : int option
val buck_merge_all_deps : bool
val buck_mode : BuckMode.t option
val buck_out_gen : string
val buck_targets_blacklist : string list
val call_graph_schedule : bool
val capture : bool
val capture_blacklist : string option
val censor_report : ((bool * Str.regexp) * (bool * Str.regexp) * string) list
val cfg_json : string option
val changed_files_index : string option
val check_version : string option
val clang_ast_file : [ `Biniou of string | `Yojson of string ] option
val clang_compound_literal_init_limit : int
val clang_blacklisted_flags : string list
val clang_blacklisted_flags_with_arg : string list
val clang_frontend_action_string : string
val clang_ignore_regex : string option
val clang_isystem_to_override_regex : Str.regexp option
val clang_idirafter_to_override_regex : Str.regexp option
val clang_libcxx_include_to_override_regex : string option
val classpath : string option
val command : ATDGenerated.InferCommand.t
val config_impact_current : string option
val config_impact_data_file : string option
val config_impact_issues_tests : string option
val config_impact_max_callees_to_print : int
val config_impact_previous : string option
val continue_analysis : bool
val continue_capture : bool
val costs_current : string option
val cost_issues_tests : string option
val cost_scuba_logging : bool
val costs_previous : string option
val cost_suppress_func_ptr : bool
val cost_tests_only_autoreleasepool : bool
val cxx : bool
val cxx_scope_guards : Yojson.Basic.t
val deduplicate : bool
val debug_exceptions : bool
val debug_level_analysis : int
val debug_level_capture : int
val debug_level_linters : int
val debug_level_test_determinator : int
val debug_mode : bool
val default_linters : bool
val dependency_mode : bool
val developer_mode : bool
val differential_filter_files : string option
val differential_filter_set : [ `Introduced | `Fixed | `Preexisting ] list
val dotty_cfg_libs : bool
val dump_duplicate_symbols : bool
val eradicate_condition_redundant : bool
val eradicate_field_over_annotated : bool
val eradicate_return_over_annotated : bool
val eradicate_verbose : bool
val fail_on_bug : bool
val fcp_apple_clang : string option
val fcp_syntax_only : bool
val file_renamings : string option
val filter_paths : bool
val filtering : bool
val force_delete_results_dir : bool
val force_integration : build_system option
val from_json_report : string
val from_json_config_impact_report : string
val from_json_costs_report : string
val frontend_stats : bool
val frontend_tests : bool
val function_pointer_specialization : bool
val generated_classes : string option
val genrule_mode : bool
val get_linter_doc_url : linter_id:string -> string option
val help_checker : Checker.t list
val help_issue_type : IssueType.t list
val hoisting_report_only_expensive : bool
val html : bool
val global_tenv : bool
val icfg_dotty_outfile : string option
val impurity_report_immutable_modifications : bool
val incremental_analysis : bool
val infer_is_clang : bool
val infer_is_javac : bool
val implicit_sdk_root : string option
val inclusive_cost : bool
val inferconfig_file : string option
val inferconfig_dir : string option
val is_checker_enabled : Checker.t -> bool
val issues_tests : string option
val issues_tests_fields : IssuesTestField.t list
val java_debug_source_file_info : string option
val java_jar_compiler : string option
val java_source_parser_experimental : bool
val java_version : int option
val javac_classes_out : string
val job_id : string option
val jobs : int
val keep_going : bool
val linter : string option
val linters_def_file : string list
val linters_def_folder : string list
val linters_developer_mode : bool
val linters_ignore_clang_failures : bool
val linters_validate_syntax_only : bool
val list_checkers : bool
val list_issue_types : bool
val liveness_dangerous_classes : Yojson.Basic.t
val liveness_ignored_constant : string list
val load_average : float option
val max_nesting : int option
val memtrace_analysis : bool
val memtrace_sampling_rate : float
val merge : bool
val method_decls_info : string option
val modified_lines : string option
val no_translate_libs : bool
val nullable_annotation : string option
val nullsafe_annotation_graph : bool
val nullsafe_disable_field_not_initialized_in_nonstrict_classes : bool
val nullsafe_optimistic_third_party_in_default_mode : bool
val nullsafe_third_party_signatures : string option
val nullsafe_third_party_location_for_messaging_only : string option
val nullsafe_strict_containers : bool
val oom_threshold : int option
val only_cheap_debug : bool
val patterns_modeled_expensive : string * Yojson.Basic.t
val patterns_never_returning_null : string * Yojson.Basic.t
val patterns_skip_implementation : string * Yojson.Basic.t
val patterns_skip_translation : string * Yojson.Basic.t
val pmd_xml : bool
val print_active_checkers : bool
val print_builtins : bool
val print_jbir : bool
val print_logs : bool
val print_types : bool
val print_using_diff : bool
val procedures : bool
val procedures_attributes : bool
val procedures_cfg : bool
val procedures_definedness : bool
val procedures_filter : string option
val procedures_name : bool
val procedures_source_file : bool
val procedures_summary : bool
val procedures_summary_json : bool
val process_clang_ast : bool
val profiler_samples : string option
val progress_bar : [ `MultiLine | `Plain | `Quiet ]
val project_root : string
val pulse_cut_to_one_path_procedures_pattern : Str.regexp option
val pulse_intraprocedural_only : bool
val pulse_isl : bool
val pulse_max_disjuncts : int
val pulse_model_abort : string list
val pulse_model_alloc_pattern : Str.regexp option
val pulse_model_release_pattern : Str.regexp option
val pulse_model_return_first_arg : Str.regexp option
val pulse_model_return_nonnull : Str.regexp option
val pulse_model_skip_pattern : Str.regexp option
val pulse_report_ignore_unknown_java_methods_patterns : Str.regexp option
val pulse_model_transfer_ownership_namespace : (string * string) list
val pulse_model_transfer_ownership : string list
val pulse_report_latent_issues : bool
val pulse_recency_limit : int
val pulse_widen_threshold : int
val pulse_nullsafe_report_npe : bool
val pure_by_default : bool
val quandary_endpoints : Yojson.Basic.t
val quandary_sanitizers : Yojson.Basic.t
val quandary_show_passthroughs : bool
val quandary_sinks : Yojson.Basic.t
val quandary_sources : Yojson.Basic.t
val quiet : bool
val racerd_guardedby : bool
val reactive_mode : bool
val reanalyze : bool
val relative_path_backtrack : int
val report : bool
val report_blacklist_files_containing : string list
val report_console_limit : int option
val report_current : string option
val report_custom_error : bool
val report_force_relative_path : bool
val report_formatter : [ `No_formatter | `Phabricator_formatter ]
val report_path_regex_blacklist : string list
val report_path_regex_whitelist : string list
val report_previous : string option
val report_suppress_errors : string list
val reports_include_ml_loc : bool
val rest : string list
val results_dir : string
val scheduler : scheduler
val scuba_logging : bool
val scuba_normals : string IStdlib.IStd .String.Map.t
val scuba_tags : string list IStdlib.IStd .String.Map.t
val select : [ `All | `Select of int ] option
val show_buckets : bool
val siof_check_iostreams : bool
val siof_safe_methods : string list
val skip_analysis_in_path : string list
val skip_analysis_in_path_skips_compilation : bool
val skip_duplicated_types : bool
val skip_non_capture_clang_commands : bool
val source_files : bool
val source_files_cfg : bool
val source_files_filter : string option
val source_files_freshly_captured : bool
val source_files_procedure_names : bool
val source_files_type_environment : bool
val source_preview : bool
val sourcepath : string option
val sources : string list
val sqlite_cache_size : int
val sqlite_page_size : int
val sqlite_lock_timeout : int
val sqlite_vfs : string option
val starvation_skip_analysis : Yojson.Basic.t
val starvation_strict_mode : bool
val starvation_whole_program : bool
val subtype_multirange : bool
val summaries_caches_max_size : int
val suppress_lint_ignore_types : bool
val tenv_json : string option
val test_determinator : bool
val export_changed_functions : bool
val test_filtering : bool
val testing_mode : bool
val threadsafe_aliases : Yojson.Basic.t
val topl_max_conjuncts : int
val topl_max_disjuncts : int
val topl_properties : string list
val trace_absarray : bool
val trace_error : bool
val trace_events : bool
val trace_ondemand : bool
val trace_topl : bool
val tv_commit : string option
val tv_limit : int
val tv_limit_filtered : int
val uninit_interproc : bool
val workspace : string option
val write_html : bool
val write_html_whitelist_regex : string list
val write_website : string option
val xcode_developer_dir : string option
val xcode_isysroot_suffix : string option
val xcpretty : bool
Configuration values derived from command-line optionsval dynamic_dispatch : bool
val toplevel_results_dir : string
In some integrations, eg Buck, infer subprocesses started by the build system (started by the toplevel infer process) will have their own results directory; this points to the results directory of the toplevel infer process, which can be useful for, eg, storing debug info. In other cases this is equal to results_dir
.
val is_in_custom_symbols : string -> string -> bool
Does named symbol match any prefix in the named custom symbol list?
val java_package_is_external : string -> bool
Check if a Java package is external to the repository
val scuba_execution_id : IStdlib.IStd .Int64.t option
a random number to (hopefully) uniquely identify this run
Global variables with initial values specified by command-line optionsval clang_compilation_dbs : [ `Escaped of string | `Raw of string ] list
\ No newline at end of file
diff --git a/website/static/odoc/next/infer/IBase/IssueType/index.html b/website/static/odoc/next/infer/IBase/IssueType/index.html
index bfd877d32..d08720ad2 100644
--- a/website/static/odoc/next/infer/IBase/IssueType/index.html
+++ b/website/static/odoc/next/infer/IBase/IssueType/index.html
@@ -1,2 +1,2 @@
-IssueType (infer.IBase.IssueType) type visibility
=
|
User
always add to error log
|
Developer
only add to error log in some debug modes
|
Silent
never add to error log
visibility of the issue type
val string_of_visibility : visibility -> string
type severity
=
|
Like
|
Info
|
Advice
|
Warning
|
Error
severity of the report
val string_of_severity : severity -> string
type t
= private
{
unique_id : string;
checker : Checker.t ;
visibility : visibility ;
user_documentation : string option ;
mutable default_severity : severity ;
used for documentation but can be overriden at report time
mutable enabled : bool;
mutable hum : string;
mutable doc_url : string option ;
mutable linters_def_file : string option ;
}
val compare : t -> t -> int
val equal : t -> t -> bool
val all_issues : unit -> t list
all the issues declared so far
val pp : Stdlib.Format.formatter -> t -> unit
pretty print a localised string
val find_from_string : id:string -> t option
return the issue type if it was previously registered
val register_dynamic : ?enabled:bool -> ?hum:string -> ?doc_url:string -> linters_def_file:string option -> id:string -> ?user_documentation:string -> severity -> Checker.t -> t
Create a new issue and register it in the list of all issues. NOTE: if the issue with the same string id is already registered, overrides `hum`, `doc_url`, and `linters_def_file`, but DOES NOT override `enabled`. This trick allows to deal with disabling/enabling dynamic AL issues from the config, when we don't know all params yet. Thus, the human-readable description can be updated when we encounter the definition of the issue type, eg in AL.
val checker_can_report : Checker.t -> t -> bool
Whether the issue was registered as coming from the given checker. Important to call this before reporting to keep documentation accurate.
val set_enabled : t -> bool -> unit
val abduction_case_not_implemented : t
val arbitrary_code_execution_under_lock : t
val array_of_pointsto : t
val array_out_of_bounds_l1 : t
val array_out_of_bounds_l2 : t
val array_out_of_bounds_l3 : t
val assert_failure : t
val biabduction_analysis_stops : t
val buffer_overrun_l1 : t
val buffer_overrun_l2 : t
val buffer_overrun_l3 : t
val buffer_overrun_l4 : t
val buffer_overrun_l5 : t
val buffer_overrun_s2 : t
val buffer_overrun_u5 : t
val cannot_star : t
val captured_strong_self : t
val checkers_allocates_memory : t
Warning name when a performance critical method directly or indirectly calls a method allocating memory
val checkers_annotation_reachability_error : t
val checkers_calls_expensive_method : t
Warning name when a performance critical method directly or indirectly calls a method annotatd as expensive
val checkers_expensive_overrides_unexpensive : t
Warning name for the subtyping rule: method not annotated as expensive cannot be overridden by a method annotated as expensive
val checkers_fragment_retain_view : t
val checkers_immutable_cast : t
val checkers_printf_args : t
val class_cast_exception : t
val complexity_increase : kind:CostKind.t -> is_on_ui_thread:bool -> t
val component_with_multiple_factory_methods : t
val condition_always_false : t
val condition_always_true : t
val config_checks_between_markers : t
val config_impact_analysis : t
val constant_address_dereference : t
val create_intent_from_uri : t
val cross_site_scripting : t
val dangling_pointer_dereference : t
val dangling_pointer_dereference_maybe : t
val dead_store : t
val deadlock : t
val divide_by_zero : t
val do_not_report : t
an issue type that should never be reported
val empty_vector_access : t
val eradicate_annotation_graph : t
val eradicate_condition_redundant : t
val eradicate_field_not_initialized : t
val eradicate_field_not_nullable : t
val eradicate_field_over_annotated : t
val eradicate_inconsistent_subclass_parameter_annotation : t
val eradicate_inconsistent_subclass_return_annotation : t
val eradicate_redundant_nested_class_annotation : t
val eradicate_bad_nested_class_annotation : t
val eradicate_nullable_dereference : t
val eradicate_parameter_not_nullable : t
val eradicate_return_not_nullable : t
val eradicate_return_over_annotated : t
val eradicate_unvetted_third_party_in_nullsafe : t
val eradicate_unchecked_usage_in_nullsafe : t
val eradicate_meta_class_can_be_nullsafe : t
val eradicate_meta_class_needs_improvement : t
val eradicate_meta_class_is_nullsafe : t
val exposed_insecure_intent_handling : t
val expensive_cost_call : kind:CostKind.t -> t
val failure_exe : t
val field_not_null_checked : t
val guardedby_violation : t
val guardedby_violation_nullsafe : t
val impure_function : t
val inefficient_keyset_iterator : t
val inferbo_alloc_is_big : t
val inferbo_alloc_is_negative : t
val inferbo_alloc_is_zero : t
val inferbo_alloc_may_be_big : t
val inferbo_alloc_may_be_negative : t
val infinite_cost_call : kind:CostKind.t -> t
val inherently_dangerous_function : t
val insecure_intent_handling : t
val integer_overflow_l1 : t
val integer_overflow_l2 : t
val integer_overflow_l5 : t
val integer_overflow_u5 : t
val interface_not_thread_safe : t
val internal_error : t
val invariant_call : t
val ipc_on_ui_thread : t
val javascript_injection : t
val lab_resource_leak : t
val dotnet_resource_leak : t
val leak_after_array_abstraction : t
val leak_unknown_origin : t
val lockless_violation : t
val lock_consistency_violation : t
val logging_private_data : t
val expensive_loop_invariant_call : t
val memory_leak : t
val missing_fld : t
val missing_required_prop : t
val mixed_self_weakself : t
val modifies_immutable : t
val multiple_weakself : t
val mutable_local_variable_in_component_file : t
val null_dereference : t
val nullptr_dereference : t
val optional_empty_access : t
val parameter_not_null_checked : t
val precondition_not_found : t
val precondition_not_met : t
val premature_nil_termination : t
val pulse_memory_leak : t
val pure_function : t
val quandary_taint_error : t
val resource_leak : t
val retain_cycle : t
val skip_function : t
val shell_injection : t
val shell_injection_risk : t
val sql_injection : t
val sql_injection_risk : t
val stack_variable_address_escape : t
val starvation : t
val static_initialization_order_fiasco : t
val strict_mode_violation : t
val strong_self_not_checked : t
val symexec_memory_error : t
val thread_safety_violation : t
val thread_safety_violation_nullsafe : t
val topl_biabd_error : t
val topl_pulse_error : t
val uninitialized_value : t
val uninitialized_value_pulse : t
val unreachable_code_after : t
val use_after_delete : t
val use_after_free : t
val use_after_lifetime : t
val untrusted_buffer_access : t
val untrusted_deserialization : t
val untrusted_deserialization_risk : t
val untrusted_file : t
val untrusted_file_risk : t
val untrusted_heap_allocation : t
val untrusted_intent_creation : t
val untrusted_url_risk : t
val untrusted_environment_change_risk : t
val untrusted_variable_length_array : t
val user_controlled_sql_risk : t
val vector_invalidation : t
val weak_self_in_noescape_block : t
val wrong_argument_number : t
val unreachable_cost_call : kind:CostKind.t -> t
val is_autoreleasepool_size_issue : t -> bool
\ No newline at end of file
+IssueType (infer.IBase.IssueType) type visibility
=
|
User
always add to error log
|
Developer
only add to error log in some debug modes
|
Silent
never add to error log
visibility of the issue type
val string_of_visibility : visibility -> string
type severity
=
|
Like
|
Info
|
Advice
|
Warning
|
Error
severity of the report
val string_of_severity : severity -> string
type t
= private
{
unique_id : string;
checker : Checker.t ;
visibility : visibility ;
user_documentation : string option ;
mutable default_severity : severity ;
used for documentation but can be overriden at report time
mutable enabled : bool;
mutable hum : string;
mutable doc_url : string option ;
mutable linters_def_file : string option ;
}
val compare : t -> t -> int
val equal : t -> t -> bool
val all_issues : unit -> t list
all the issues declared so far
val pp : Stdlib.Format.formatter -> t -> unit
pretty print a localised string
val find_from_string : id:string -> t option
return the issue type if it was previously registered
val register_dynamic : ?enabled:bool -> ?hum:string -> ?doc_url:string -> linters_def_file:string option -> id:string -> ?user_documentation:string -> severity -> Checker.t -> t
Create a new issue and register it in the list of all issues. NOTE: if the issue with the same string id is already registered, overrides `hum`, `doc_url`, and `linters_def_file`, but DOES NOT override `enabled`. This trick allows to deal with disabling/enabling dynamic AL issues from the config, when we don't know all params yet. Thus, the human-readable description can be updated when we encounter the definition of the issue type, eg in AL.
val checker_can_report : Checker.t -> t -> bool
Whether the issue was registered as coming from the given checker. Important to call this before reporting to keep documentation accurate.
val set_enabled : t -> bool -> unit
val abduction_case_not_implemented : t
val arbitrary_code_execution_under_lock : t
val array_of_pointsto : t
val array_out_of_bounds_l1 : t
val array_out_of_bounds_l2 : t
val array_out_of_bounds_l3 : t
val assert_failure : t
val biabduction_analysis_stops : t
val buffer_overrun_l1 : t
val buffer_overrun_l2 : t
val buffer_overrun_l3 : t
val buffer_overrun_l4 : t
val buffer_overrun_l5 : t
val buffer_overrun_s2 : t
val buffer_overrun_u5 : t
val cannot_star : t
val captured_strong_self : t
val checkers_allocates_memory : t
Warning name when a performance critical method directly or indirectly calls a method allocating memory
val checkers_annotation_reachability_error : t
val checkers_calls_expensive_method : t
Warning name when a performance critical method directly or indirectly calls a method annotatd as expensive
val checkers_expensive_overrides_unexpensive : t
Warning name for the subtyping rule: method not annotated as expensive cannot be overridden by a method annotated as expensive
val checkers_fragment_retain_view : t
val checkers_immutable_cast : t
val checkers_printf_args : t
val class_cast_exception : t
val complexity_increase : kind:CostKind.t -> is_on_ui_thread:bool -> t
val component_with_multiple_factory_methods : t
val condition_always_false : t
val condition_always_true : t
val config_checks_between_markers : t
val config_impact_analysis : t
val constant_address_dereference : t
val create_intent_from_uri : t
val cross_site_scripting : t
val dangling_pointer_dereference : t
val dangling_pointer_dereference_maybe : t
val dead_store : t
val deadlock : t
val divide_by_zero : t
val do_not_report : t
an issue type that should never be reported
val empty_vector_access : t
val eradicate_annotation_graph : t
val eradicate_condition_redundant : t
val eradicate_field_not_initialized : t
val eradicate_field_not_nullable : t
val eradicate_field_over_annotated : t
val eradicate_inconsistent_subclass_parameter_annotation : t
val eradicate_inconsistent_subclass_return_annotation : t
val eradicate_redundant_nested_class_annotation : t
val eradicate_bad_nested_class_annotation : t
val eradicate_nullable_dereference : t
val eradicate_parameter_not_nullable : t
val eradicate_return_not_nullable : t
val eradicate_return_over_annotated : t
val eradicate_unvetted_third_party_in_nullsafe : t
val eradicate_unchecked_usage_in_nullsafe : t
val eradicate_meta_class_can_be_nullsafe : t
val eradicate_meta_class_needs_improvement : t
val eradicate_meta_class_is_nullsafe : t
val exposed_insecure_intent_handling : t
val expensive_cost_call : kind:CostKind.t -> t
val failure_exe : t
val field_not_null_checked : t
val guardedby_violation : t
val guardedby_violation_nullsafe : t
val impure_function : t
val inefficient_keyset_iterator : t
val inferbo_alloc_is_big : t
val inferbo_alloc_is_negative : t
val inferbo_alloc_is_zero : t
val inferbo_alloc_may_be_big : t
val inferbo_alloc_may_be_negative : t
val infinite_cost_call : kind:CostKind.t -> t
val inherently_dangerous_function : t
val insecure_intent_handling : t
val integer_overflow_l1 : t
val integer_overflow_l2 : t
val integer_overflow_l5 : t
val integer_overflow_u5 : t
val interface_not_thread_safe : t
val internal_error : t
val invariant_call : t
val ipc_on_ui_thread : t
val javascript_injection : t
val lab_resource_leak : t
val dotnet_resource_leak : t
val leak_after_array_abstraction : t
val leak_unknown_origin : t
val lockless_violation : t
val lock_consistency_violation : t
val logging_private_data : t
val expensive_loop_invariant_call : t
val memory_leak : t
val missing_fld : t
val missing_required_prop : t
val mixed_self_weakself : t
val modifies_immutable : t
val multiple_weakself : t
val mutable_local_variable_in_component_file : t
val null_dereference : t
val nullptr_dereference : t
val optional_empty_access : t
val parameter_not_null_checked : t
val precondition_not_found : t
val precondition_not_met : t
val premature_nil_termination : t
val pulse_memory_leak : t
val pure_function : t
val quandary_taint_error : t
val resource_leak : t
val retain_cycle : t
val skip_function : t
val shell_injection : t
val shell_injection_risk : t
val sql_injection : t
val sql_injection_risk : t
val stack_variable_address_escape : t
val starvation : t
val static_initialization_order_fiasco : t
val strict_mode_violation : t
val strong_self_not_checked : t
val symexec_memory_error : t
val thread_safety_violation : t
val thread_safety_violation_nullsafe : t
val topl_error : t
val uninitialized_value : t
val uninitialized_value_pulse : t
val unreachable_code_after : t
val use_after_delete : t
val use_after_free : t
val use_after_lifetime : t
val untrusted_buffer_access : t
val untrusted_deserialization : t
val untrusted_deserialization_risk : t
val untrusted_file : t
val untrusted_file_risk : t
val untrusted_heap_allocation : t
val untrusted_intent_creation : t
val untrusted_url_risk : t
val untrusted_environment_change_risk : t
val untrusted_variable_length_array : t
val user_controlled_sql_risk : t
val vector_invalidation : t
val weak_self_in_noescape_block : t
val wrong_argument_number : t
val unreachable_cost_call : kind:CostKind.t -> t
val is_autoreleasepool_size_issue : t -> bool
\ No newline at end of file
diff --git a/website/static/odoc/next/infer/IBase__Checker/index.html b/website/static/odoc/next/infer/IBase__Checker/index.html
index e9ff53031..aa332d53b 100644
--- a/website/static/odoc/next/infer/IBase__Checker/index.html
+++ b/website/static/odoc/next/infer/IBase__Checker/index.html
@@ -1,2 +1,2 @@
-IBase__Checker (infer.IBase__Checker) Up – infer » IBase__CheckerModule IBase__Checker
type t
=
|
AnnotationReachability
|
Biabduction
|
BufferOverrunAnalysis
|
BufferOverrunChecker
|
ConfigChecksBetweenMarkers
|
ConfigImpactAnalysis
|
Cost
|
Eradicate
|
FragmentRetainsView
|
ImmutableCast
|
Impurity
|
InefficientKeysetIterator
|
Linters
|
LithoRequiredProps
|
Liveness
|
LoopHoisting
|
NullsafeDeprecated
|
PrintfArgs
|
Pulse
|
PurityAnalysis
|
PurityChecker
|
Quandary
|
RacerD
|
ResourceLeakLabExercise
|
DOTNETResourceLeaks
|
SIOF
|
SelfInBlock
|
Starvation
|
ToplOnBiabduction
|
ToplOnPulse
|
Uninit
val equal : t -> t -> bool
val all : t list
type support
=
|
NoSupport
checker does not run at all for this language
|
ExperimentalSupport
checker runs but is not expected to give reasonable results
|
Support
checker is expected to give reasonable results
per-language support for each checker
type cli_flags
=
{
deprecated : string list ;
More command-line flags, similar to ~deprecated
arguments in CommandLineOption
.
show_in_help : bool;
}
type kind
=
|
UserFacing of
{
title : string;
the title of the documentation web page
markdown_body : string;
main text of the documentation
}
can report issues to users
|
UserFacingDeprecated of
{
title : string;
the title of the documentation web page
markdown_body : string;
main text of the documentation
deprecation_message : string;
}
can report issues to users but should probably be deleted from infer
|
Internal
Analysis that only serves other analyses. Do not use to mean experimental! Please still document experimental checkers as they will become non-experimental.
|
Exercise
reserved for the "resource leak" lab exercise
type config
=
{
id : string;
Unique identifier. Used to generate web URLs for the documentation as well as the flag to enable this option on the command line.
kind : kind ;
support : IBase.Language.t -> support ;
short_documentation : string;
used in man pages and as a short intro on the website
cli_flags : cli_flags option ;
If None
then the checker cannot be enabled/disabled from the command line.
enabled_by_default : bool;
activates : t list ;
list of checkers that get enabled when this checker is enabled
}
val config : t -> config
val get_id : t -> string
get_id c
is (config c).id
val from_id : string -> t option
\ No newline at end of file
+IBase__Checker (infer.IBase__Checker) Up – infer » IBase__CheckerModule IBase__Checker
type t
=
|
AnnotationReachability
|
Biabduction
|
BufferOverrunAnalysis
|
BufferOverrunChecker
|
ConfigChecksBetweenMarkers
|
ConfigImpactAnalysis
|
Cost
|
Eradicate
|
FragmentRetainsView
|
ImmutableCast
|
Impurity
|
InefficientKeysetIterator
|
Linters
|
LithoRequiredProps
|
Liveness
|
LoopHoisting
|
NullsafeDeprecated
|
PrintfArgs
|
Pulse
|
PurityAnalysis
|
PurityChecker
|
Quandary
|
RacerD
|
ResourceLeakLabExercise
|
DOTNETResourceLeaks
|
SIOF
|
SelfInBlock
|
Starvation
|
TOPL
|
Uninit
val equal : t -> t -> bool
val all : t list
type support
=
|
NoSupport
checker does not run at all for this language
|
ExperimentalSupport
checker runs but is not expected to give reasonable results
|
Support
checker is expected to give reasonable results
per-language support for each checker
type cli_flags
=
{
deprecated : string list ;
More command-line flags, similar to ~deprecated
arguments in CommandLineOption
.
show_in_help : bool;
}
type kind
=
|
UserFacing of
{
title : string;
the title of the documentation web page
markdown_body : string;
main text of the documentation
}
can report issues to users
|
UserFacingDeprecated of
{
title : string;
the title of the documentation web page
markdown_body : string;
main text of the documentation
deprecation_message : string;
}
can report issues to users but should probably be deleted from infer
|
Internal
Analysis that only serves other analyses. Do not use to mean experimental! Please still document experimental checkers as they will become non-experimental.
|
Exercise
reserved for the "resource leak" lab exercise
type config
=
{
id : string;
Unique identifier. Used to generate web URLs for the documentation as well as the flag to enable this option on the command line.
kind : kind ;
support : IBase.Language.t -> support ;
short_documentation : string;
used in man pages and as a short intro on the website
cli_flags : cli_flags option ;
If None
then the checker cannot be enabled/disabled from the command line.
enabled_by_default : bool;
activates : t list ;
list of checkers that get enabled when this checker is enabled
}
val config : t -> config
val get_id : t -> string
get_id c
is (config c).id
val from_id : string -> t option
\ No newline at end of file
diff --git a/website/static/odoc/next/infer/IBase__Config/index.html b/website/static/odoc/next/infer/IBase__Config/index.html
index 17dc69731..14d8dfe13 100644
--- a/website/static/odoc/next/infer/IBase__Config/index.html
+++ b/website/static/odoc/next/infer/IBase__Config/index.html
@@ -1,2 +1,2 @@
-IBase__Config (infer.IBase__Config) Up – infer » IBase__ConfigModule IBase__Config
Configuration values: either constant, determined at compile time, or set at startup time by system calls, environment variables, or command line options
type os_type
=
type build_system
=
|
BAnt
|
BBuck
|
BClang
|
BGradle
|
BJava
|
BJavac
|
BMake
|
BMvn
|
BNdk
|
BXcode
type scheduler
=
|
File
|
Restart
|
SyntacticCallGraph
val build_system_of_exe_name : string -> build_system
val string_of_build_system : build_system -> string
val env_inside_maven : IStdlib.IStd .Unix.env
Constant configuration valuesval anonymous_block_num_sep : string
val anonymous_block_prefix : string
val append_buck_flavors : string list
val assign : string
val biabduction_models_sql : string
val biabduction_models_jar : string
val bin_dir : string
val bound_error_allowed_in_procedure_call : bool
val buck_java_flavor_suppress_config : bool
val clang_exe_aliases : string list
val clang_initializer_prefix : string
val clang_inner_destructor_prefix : string
val clang_plugin_path : string
val classpath : string option
val default_failure_name : string
val dotty_frontend_output : string
val etc_dir : string
val fail_on_issue_exit_code : int
val fcp_dir : string
val idempotent_getters : bool
val initial_analysis_time : float
val ivar_attributes : string
val java_lambda_marker_infix : string
marker to recognize methods generated by javalib to eliminate lambdas
val lib_dir : string
val load_average : float option
val max_narrows : int
val max_widens : int
val meet_level : int
val nsnotification_center_checker_backend : bool
val os_type : os_type
val passthroughs : bool
val patterns_modeled_expensive : string * Yojson.Basic.t
val patterns_never_returning_null : string * Yojson.Basic.t
val patterns_skip_implementation : string * Yojson.Basic.t
val patterns_skip_translation : string * Yojson.Basic.t
val pp_version : Stdlib.Format.formatter -> unit -> unit
val property_attributes : string
val relative_path_backtrack : int
val report : bool
val report_custom_error : bool
val report_force_relative_path : bool
val report_immutable_modifications : bool
val report_nullable_inconsistency : bool
val save_compact_summaries : bool
val smt_output : bool
val source_file_extentions : string list
val kotlin_source_extension : string
val sourcepath : string option
val sources : string list
val trace_absarray : bool
val unsafe_unret : string
val incremental_analysis : bool
val weak : string
val whitelisted_cpp_classes : string list
val whitelisted_cpp_methods : string list
val wrappers_dir : string
Configuration values specified by command-line optionsval abs_struct : int
val abs_val : int
val allow_leak : bool
val annotation_reachability_cxx : Yojson.Basic.t
val annotation_reachability_cxx_sources : Yojson.Basic.t
val annotation_reachability_custom_pairs : Yojson.Basic.t
val array_level : int
val biabduction_models_mode : bool
val bo_debug : int
val bo_field_depth_limit : int option
val bootclasspath : string option
val buck : bool
val buck_blacklist : string list
val buck_build_args : string list
val buck_build_args_no_inline : string list
val buck_cache_mode : bool
val buck_java_heap_size_gb : int option
val buck_merge_all_deps : bool
val buck_mode : IBase.BuckMode.t option
val buck_out_gen : string
val buck_targets_blacklist : string list
val call_graph_schedule : bool
val capture : bool
val capture_blacklist : string option
val cfg_json : string option
val censor_report : ((bool * Str.regexp) * (bool * Str.regexp) * string) list
val changed_files_index : string option
val check_version : string option
val clang_ast_file : [ `Biniou of string | `Yojson of string ] option
val clang_compound_literal_init_limit : int
val clang_blacklisted_flags : string list
val clang_blacklisted_flags_with_arg : string list
val clang_ignore_regex : string option
val clang_isystem_to_override_regex : Str.regexp option
val clang_idirafter_to_override_regex : Str.regexp option
val clang_libcxx_include_to_override_regex : string option
val command : ATDGenerated.InferCommand.t
val config_impact_current : string option
val config_impact_data_file : string option
val config_impact_issues_tests : string option
val config_impact_max_callees_to_print : int
val config_impact_previous : string option
val continue_analysis : bool
val continue_capture : bool
val costs_current : string option
val cost_issues_tests : string option
val cost_scuba_logging : bool
val costs_previous : string option
val cost_suppress_func_ptr : bool
val cost_tests_only_autoreleasepool : bool
val cxx : bool
val cxx_scope_guards : Yojson.Basic.t
val deduplicate : bool
val debug_exceptions : bool
val debug_level_analysis : int
val debug_level_capture : int
val debug_level_linters : int
val debug_level_test_determinator : int
val debug_mode : bool
val default_linters : bool
val dependency_mode : bool
val developer_mode : bool
val differential_filter_files : string option
val differential_filter_set : [ `Introduced | `Fixed | `Preexisting ] list
val dotty_cfg_libs : bool
val dump_duplicate_symbols : bool
val eradicate_condition_redundant : bool
val eradicate_field_over_annotated : bool
val eradicate_return_over_annotated : bool
val eradicate_verbose : bool
val fail_on_bug : bool
val fcp_apple_clang : string option
val fcp_syntax_only : bool
val file_renamings : string option
val filter_paths : bool
val filtering : bool
val force_delete_results_dir : bool
val force_integration : build_system option
val from_json_report : string
val from_json_config_impact_report : string
val from_json_costs_report : string
val frontend_stats : bool
val frontend_tests : bool
val function_pointer_specialization : bool
val generated_classes : string option
val genrule_mode : bool
val get_linter_doc_url : linter_id:string -> string option
val help_checker : IBase.Checker.t list
val help_issue_type : IBase.IssueType.t list
val hoisting_report_only_expensive : bool
val html : bool
val global_tenv : bool
val icfg_dotty_outfile : string option
val infer_is_clang : bool
val infer_is_javac : bool
val implicit_sdk_root : string option
val inclusive_cost : bool
val inferconfig_file : string option
val inferconfig_dir : string option
val is_checker_enabled : IBase.Checker.t -> bool
val issues_tests : string option
val issues_tests_fields : IBase.IssuesTestField.t list
val iterations : int
val java_debug_source_file_info : string option
val java_jar_compiler : string option
val java_source_parser_experimental : bool
val java_version : int option
val javac_classes_out : string
val job_id : string option
val jobs : int
val join_cond : int
val keep_going : bool
val linter : string option
val linters_def_file : string list
val linters_def_folder : string list
val linters_developer_mode : bool
val linters_ignore_clang_failures : bool
val linters_validate_syntax_only : bool
val list_checkers : bool
val list_issue_types : bool
val liveness_dangerous_classes : Yojson.Basic.t
val liveness_ignored_constant : string list
val max_nesting : int option
val memtrace_analysis : bool
val memtrace_sampling_rate : float
val merge : bool
val method_decls_info : string option
val ml_buckets : [ `MLeak_all | `MLeak_arc | `MLeak_cf | `MLeak_cpp | `MLeak_no_arc | `MLeak_unknown ] list
val modified_lines : string option
val monitor_prop_size : bool
val nelseg : bool
val no_translate_libs : bool
val nullable_annotation : string option
val nullsafe_annotation_graph : bool
val nullsafe_disable_field_not_initialized_in_nonstrict_classes : bool
val nullsafe_optimistic_third_party_in_default_mode : bool
val nullsafe_third_party_signatures : string option
val nullsafe_third_party_location_for_messaging_only : string option
val nullsafe_strict_containers : bool
val oom_threshold : int option
val only_cheap_debug : bool
val pmd_xml : bool
val print_active_checkers : bool
val print_builtins : bool
val print_jbir : bool
val print_logs : bool
val print_types : bool
val print_using_diff : bool
val procedures : bool
val procedures_attributes : bool
val procedures_cfg : bool
val procedures_definedness : bool
val procedures_filter : string option
val procedures_name : bool
val procedures_source_file : bool
val procedures_summary : bool
val procedures_summary_json : bool
val process_clang_ast : bool
val clang_frontend_action_string : string
val profiler_samples : string option
val progress_bar : [ `MultiLine | `Plain | `Quiet ]
val project_root : string
val pulse_cut_to_one_path_procedures_pattern : Str.regexp option
val pulse_intraprocedural_only : bool
val pulse_isl : bool
val pulse_max_disjuncts : int
val pulse_model_abort : string list
val pulse_model_alloc_pattern : Str.regexp option
val pulse_model_release_pattern : Str.regexp option
val pulse_model_return_nonnull : Str.regexp option
val pulse_model_skip_pattern : Str.regexp option
val pulse_report_ignore_unknown_java_methods_patterns : Str.regexp option
val pulse_model_transfer_ownership_namespace : (string * string) list
val pulse_model_transfer_ownership : string list
val pulse_report_latent_issues : bool
val pulse_recency_limit : int
val pulse_widen_threshold : int
val pulse_nullsafe_report_npe : bool
val pure_by_default : bool
val quandary_endpoints : Yojson.Basic.t
val quandary_sanitizers : Yojson.Basic.t
val quandary_sinks : Yojson.Basic.t
val quandary_sources : Yojson.Basic.t
val quiet : bool
val racerd_guardedby : bool
val reactive_mode : bool
val reanalyze : bool
val report_blacklist_files_containing : string list
val report_console_limit : int option
val report_current : string option
val report_formatter : [ `No_formatter | `Phabricator_formatter ]
val report_path_regex_blacklist : string list
val report_path_regex_whitelist : string list
val report_previous : string option
val report_suppress_errors : string list
val reports_include_ml_loc : bool
val rest : string list
val results_dir : string
val scheduler : scheduler
val scuba_logging : bool
val scuba_normals : string IStdlib.IStd .String.Map.t
val scuba_tags : string list IStdlib.IStd .String.Map.t
val seconds_per_iteration : float option
val select : [ `All | `Select of int ] option
val show_buckets : bool
val siof_check_iostreams : bool
val siof_safe_methods : string list
val skip_analysis_in_path : string list
val skip_analysis_in_path_skips_compilation : bool
val skip_duplicated_types : bool
val skip_non_capture_clang_commands : bool
val source_files : bool
val source_files_cfg : bool
val source_files_filter : string option
val source_files_freshly_captured : bool
val source_files_procedure_names : bool
val source_files_type_environment : bool
val source_preview : bool
val sqlite_cache_size : int
val sqlite_page_size : int
val sqlite_lock_timeout : int
val sqlite_vfs : string option
val starvation_skip_analysis : Yojson.Basic.t
val starvation_strict_mode : bool
val starvation_whole_program : bool
val subtype_multirange : bool
val summaries_caches_max_size : int
val suppress_lint_ignore_types : bool
val symops_per_iteration : int option
val tenv_json : string option
val test_determinator : bool
val export_changed_functions : bool
val test_filtering : bool
val testing_mode : bool
val threadsafe_aliases : Yojson.Basic.t
val topl_max_conjuncts : int
val topl_max_disjuncts : int
val topl_properties : string list
val trace_error : bool
val trace_events : bool
val trace_join : bool
val trace_ondemand : bool
val trace_rearrange : bool
val trace_topl : bool
val tv_commit : string option
val tv_limit : int
val tv_limit_filtered : int
val type_size : bool
val uninit_interproc : bool
val unsafe_malloc : bool
val worklist_mode : int
val workspace : string option
val write_dotty : bool
val write_html : bool
val write_html_whitelist_regex : string list
val write_website : string option
val xcode_developer_dir : string option
val xcode_isysroot_suffix : string option
val xcpretty : bool
Configuration values derived from command-line optionsval dynamic_dispatch : bool
val toplevel_results_dir : string
In some integrations, eg Buck, infer subprocesses started by the build system (started by the toplevel infer process) will have their own results directory; this points to the results directory of the toplevel infer process, which can be useful for, eg, storing debug info. In other cases this is equal to results_dir
.
val is_in_custom_symbols : string -> string -> bool
Does named symbol match any prefix in the named custom symbol list?
val java_package_is_external : string -> bool
Check if a Java package is external to the repository
val scuba_execution_id : IStdlib.IStd .Int64.t option
a random number to (hopefully) uniquely identify this run
Global variables with initial values specified by command-line optionsval clang_compilation_dbs : [ `Escaped of string | `Raw of string ] list
\ No newline at end of file
+IBase__Config (infer.IBase__Config) Up – infer » IBase__ConfigModule IBase__Config
Configuration values: either constant, determined at compile time, or set at startup time by system calls, environment variables, or command line options
type os_type
=
type build_system
=
|
BAnt
|
BBuck
|
BClang
|
BGradle
|
BJava
|
BJavac
|
BMake
|
BMvn
|
BNdk
|
BXcode
type scheduler
=
|
File
|
Restart
|
SyntacticCallGraph
val build_system_of_exe_name : string -> build_system
val string_of_build_system : build_system -> string
val env_inside_maven : IStdlib.IStd .Unix.env
Constant configuration valuesval anonymous_block_num_sep : string
val anonymous_block_prefix : string
val assign : string
val biabduction_models_sql : string
val biabduction_models_jar : string
val bin_dir : string
val bound_error_allowed_in_procedure_call : bool
val clang_exe_aliases : string list
val clang_initializer_prefix : string
val clang_inner_destructor_prefix : string
val clang_plugin_path : string
val default_failure_name : string
val dotty_frontend_output : string
val etc_dir : string
val fail_on_issue_exit_code : int
val fcp_dir : string
val idempotent_getters : bool
val initial_analysis_time : float
val ivar_attributes : string
val java_lambda_marker_infix : string
marker to recognize methods generated by javalib to eliminate lambdas
val kotlin_source_extension : string
val lib_dir : string
val max_narrows : int
val max_widens : int
val meet_level : int
val nsnotification_center_checker_backend : bool
val os_type : os_type
val pp_version : Stdlib.Format.formatter -> unit -> unit
val property_attributes : string
val report_nullable_inconsistency : bool
val save_compact_summaries : bool
val smt_output : bool
val source_file_extentions : string list
val unsafe_unret : string
val weak : string
val whitelisted_cpp_classes : string list
val whitelisted_cpp_methods : string list
val wrappers_dir : string
Configuration values specified by command-line optionsval annotation_reachability_cxx : Yojson.Basic.t
val annotation_reachability_cxx_sources : Yojson.Basic.t
val annotation_reachability_custom_pairs : Yojson.Basic.t
val append_buck_flavors : string list
val biabduction_abs_struct : int
val biabduction_abs_val : int
val biabduction_allow_leak : bool
val biabduction_array_level : int
val biabduction_models_mode : bool
val biabduction_iterations : int
val biabduction_join_cond : int
val biabduction_memleak_buckets : [ `MLeak_all | `MLeak_arc | `MLeak_cf | `MLeak_cpp | `MLeak_no_arc | `MLeak_unknown ] list
val biabduction_monitor_prop_size : bool
val biabduction_nelseg : bool
val biabduction_seconds_per_iteration : float option
val biabduction_symops_per_iteration : int option
val biabduction_trace_join : bool
val biabduction_trace_rearrange : bool
val biabduction_type_size : bool
val biabduction_unsafe_malloc : bool
val biabduction_worklist_mode : int
val biabduction_write_dotty : bool
val bo_debug : int
val bo_field_depth_limit : int option
val bootclasspath : string option
val buck : bool
val buck_blacklist : string list
val buck_build_args : string list
val buck_build_args_no_inline : string list
val buck_cache_mode : bool
val buck_java_flavor_suppress_config : bool
val buck_java_heap_size_gb : int option
val buck_merge_all_deps : bool
val buck_mode : IBase.BuckMode.t option
val buck_out_gen : string
val buck_targets_blacklist : string list
val call_graph_schedule : bool
val capture : bool
val capture_blacklist : string option
val censor_report : ((bool * Str.regexp) * (bool * Str.regexp) * string) list
val cfg_json : string option
val changed_files_index : string option
val check_version : string option
val clang_ast_file : [ `Biniou of string | `Yojson of string ] option
val clang_compound_literal_init_limit : int
val clang_blacklisted_flags : string list
val clang_blacklisted_flags_with_arg : string list
val clang_frontend_action_string : string
val clang_ignore_regex : string option
val clang_isystem_to_override_regex : Str.regexp option
val clang_idirafter_to_override_regex : Str.regexp option
val clang_libcxx_include_to_override_regex : string option
val classpath : string option
val command : ATDGenerated.InferCommand.t
val config_impact_current : string option
val config_impact_data_file : string option
val config_impact_issues_tests : string option
val config_impact_max_callees_to_print : int
val config_impact_previous : string option
val continue_analysis : bool
val continue_capture : bool
val costs_current : string option
val cost_issues_tests : string option
val cost_scuba_logging : bool
val costs_previous : string option
val cost_suppress_func_ptr : bool
val cost_tests_only_autoreleasepool : bool
val cxx : bool
val cxx_scope_guards : Yojson.Basic.t
val deduplicate : bool
val debug_exceptions : bool
val debug_level_analysis : int
val debug_level_capture : int
val debug_level_linters : int
val debug_level_test_determinator : int
val debug_mode : bool
val default_linters : bool
val dependency_mode : bool
val developer_mode : bool
val differential_filter_files : string option
val differential_filter_set : [ `Introduced | `Fixed | `Preexisting ] list
val dotty_cfg_libs : bool
val dump_duplicate_symbols : bool
val eradicate_condition_redundant : bool
val eradicate_field_over_annotated : bool
val eradicate_return_over_annotated : bool
val eradicate_verbose : bool
val fail_on_bug : bool
val fcp_apple_clang : string option
val fcp_syntax_only : bool
val file_renamings : string option
val filter_paths : bool
val filtering : bool
val force_delete_results_dir : bool
val force_integration : build_system option
val from_json_report : string
val from_json_config_impact_report : string
val from_json_costs_report : string
val frontend_stats : bool
val frontend_tests : bool
val function_pointer_specialization : bool
val generated_classes : string option
val genrule_mode : bool
val get_linter_doc_url : linter_id:string -> string option
val help_checker : IBase.Checker.t list
val help_issue_type : IBase.IssueType.t list
val hoisting_report_only_expensive : bool
val html : bool
val global_tenv : bool
val icfg_dotty_outfile : string option
val impurity_report_immutable_modifications : bool
val incremental_analysis : bool
val infer_is_clang : bool
val infer_is_javac : bool
val implicit_sdk_root : string option
val inclusive_cost : bool
val inferconfig_file : string option
val inferconfig_dir : string option
val is_checker_enabled : IBase.Checker.t -> bool
val issues_tests : string option
val issues_tests_fields : IBase.IssuesTestField.t list
val java_debug_source_file_info : string option
val java_jar_compiler : string option
val java_source_parser_experimental : bool
val java_version : int option
val javac_classes_out : string
val job_id : string option
val jobs : int
val keep_going : bool
val linter : string option
val linters_def_file : string list
val linters_def_folder : string list
val linters_developer_mode : bool
val linters_ignore_clang_failures : bool
val linters_validate_syntax_only : bool
val list_checkers : bool
val list_issue_types : bool
val liveness_dangerous_classes : Yojson.Basic.t
val liveness_ignored_constant : string list
val load_average : float option
val max_nesting : int option
val memtrace_analysis : bool
val memtrace_sampling_rate : float
val merge : bool
val method_decls_info : string option
val modified_lines : string option
val no_translate_libs : bool
val nullable_annotation : string option
val nullsafe_annotation_graph : bool
val nullsafe_disable_field_not_initialized_in_nonstrict_classes : bool
val nullsafe_optimistic_third_party_in_default_mode : bool
val nullsafe_third_party_signatures : string option
val nullsafe_third_party_location_for_messaging_only : string option
val nullsafe_strict_containers : bool
val oom_threshold : int option
val only_cheap_debug : bool
val patterns_modeled_expensive : string * Yojson.Basic.t
val patterns_never_returning_null : string * Yojson.Basic.t
val patterns_skip_implementation : string * Yojson.Basic.t
val patterns_skip_translation : string * Yojson.Basic.t
val pmd_xml : bool
val print_active_checkers : bool
val print_builtins : bool
val print_jbir : bool
val print_logs : bool
val print_types : bool
val print_using_diff : bool
val procedures : bool
val procedures_attributes : bool
val procedures_cfg : bool
val procedures_definedness : bool
val procedures_filter : string option
val procedures_name : bool
val procedures_source_file : bool
val procedures_summary : bool
val procedures_summary_json : bool
val process_clang_ast : bool
val profiler_samples : string option
val progress_bar : [ `MultiLine | `Plain | `Quiet ]
val project_root : string
val pulse_cut_to_one_path_procedures_pattern : Str.regexp option
val pulse_intraprocedural_only : bool
val pulse_isl : bool
val pulse_max_disjuncts : int
val pulse_model_abort : string list
val pulse_model_alloc_pattern : Str.regexp option
val pulse_model_release_pattern : Str.regexp option
val pulse_model_return_first_arg : Str.regexp option
val pulse_model_return_nonnull : Str.regexp option
val pulse_model_skip_pattern : Str.regexp option
val pulse_report_ignore_unknown_java_methods_patterns : Str.regexp option
val pulse_model_transfer_ownership_namespace : (string * string) list
val pulse_model_transfer_ownership : string list
val pulse_report_latent_issues : bool
val pulse_recency_limit : int
val pulse_widen_threshold : int
val pulse_nullsafe_report_npe : bool
val pure_by_default : bool
val quandary_endpoints : Yojson.Basic.t
val quandary_sanitizers : Yojson.Basic.t
val quandary_show_passthroughs : bool
val quandary_sinks : Yojson.Basic.t
val quandary_sources : Yojson.Basic.t
val quiet : bool
val racerd_guardedby : bool
val reactive_mode : bool
val reanalyze : bool
val relative_path_backtrack : int
val report : bool
val report_blacklist_files_containing : string list
val report_console_limit : int option
val report_current : string option
val report_custom_error : bool
val report_force_relative_path : bool
val report_formatter : [ `No_formatter | `Phabricator_formatter ]
val report_path_regex_blacklist : string list
val report_path_regex_whitelist : string list
val report_previous : string option
val report_suppress_errors : string list
val reports_include_ml_loc : bool
val rest : string list
val results_dir : string
val scheduler : scheduler
val scuba_logging : bool
val scuba_normals : string IStdlib.IStd .String.Map.t
val scuba_tags : string list IStdlib.IStd .String.Map.t
val select : [ `All | `Select of int ] option
val show_buckets : bool
val siof_check_iostreams : bool
val siof_safe_methods : string list
val skip_analysis_in_path : string list
val skip_analysis_in_path_skips_compilation : bool
val skip_duplicated_types : bool
val skip_non_capture_clang_commands : bool
val source_files : bool
val source_files_cfg : bool
val source_files_filter : string option
val source_files_freshly_captured : bool
val source_files_procedure_names : bool
val source_files_type_environment : bool
val source_preview : bool
val sourcepath : string option
val sources : string list
val sqlite_cache_size : int
val sqlite_page_size : int
val sqlite_lock_timeout : int
val sqlite_vfs : string option
val starvation_skip_analysis : Yojson.Basic.t
val starvation_strict_mode : bool
val starvation_whole_program : bool
val subtype_multirange : bool
val summaries_caches_max_size : int
val suppress_lint_ignore_types : bool
val tenv_json : string option
val test_determinator : bool
val export_changed_functions : bool
val test_filtering : bool
val testing_mode : bool
val threadsafe_aliases : Yojson.Basic.t
val topl_max_conjuncts : int
val topl_max_disjuncts : int
val topl_properties : string list
val trace_absarray : bool
val trace_error : bool
val trace_events : bool
val trace_ondemand : bool
val trace_topl : bool
val tv_commit : string option
val tv_limit : int
val tv_limit_filtered : int
val uninit_interproc : bool
val workspace : string option
val write_html : bool
val write_html_whitelist_regex : string list
val write_website : string option
val xcode_developer_dir : string option
val xcode_isysroot_suffix : string option
val xcpretty : bool
Configuration values derived from command-line optionsval dynamic_dispatch : bool
val toplevel_results_dir : string
In some integrations, eg Buck, infer subprocesses started by the build system (started by the toplevel infer process) will have their own results directory; this points to the results directory of the toplevel infer process, which can be useful for, eg, storing debug info. In other cases this is equal to results_dir
.
val is_in_custom_symbols : string -> string -> bool
Does named symbol match any prefix in the named custom symbol list?
val java_package_is_external : string -> bool
Check if a Java package is external to the repository
val scuba_execution_id : IStdlib.IStd .Int64.t option
a random number to (hopefully) uniquely identify this run
Global variables with initial values specified by command-line optionsval clang_compilation_dbs : [ `Escaped of string | `Raw of string ] list
\ No newline at end of file
diff --git a/website/static/odoc/next/infer/IBase__IssueType/index.html b/website/static/odoc/next/infer/IBase__IssueType/index.html
index 9abb72052..43646125d 100644
--- a/website/static/odoc/next/infer/IBase__IssueType/index.html
+++ b/website/static/odoc/next/infer/IBase__IssueType/index.html
@@ -1,2 +1,2 @@
-IBase__IssueType (infer.IBase__IssueType) Up – infer » IBase__IssueTypeModule IBase__IssueType
type visibility
=
|
User
always add to error log
|
Developer
only add to error log in some debug modes
|
Silent
never add to error log
visibility of the issue type
val string_of_visibility : visibility -> string
type severity
=
|
Like
|
Info
|
Advice
|
Warning
|
Error
severity of the report
val string_of_severity : severity -> string
type t
= private
{
unique_id : string;
checker : IBase.Checker.t ;
visibility : visibility ;
user_documentation : string option ;
mutable default_severity : severity ;
used for documentation but can be overriden at report time
mutable enabled : bool;
mutable hum : string;
mutable doc_url : string option ;
mutable linters_def_file : string option ;
}
val compare : t -> t -> int
val equal : t -> t -> bool
val all_issues : unit -> t list
all the issues declared so far
val pp : Stdlib.Format.formatter -> t -> unit
pretty print a localised string
val find_from_string : id:string -> t option
return the issue type if it was previously registered
val register_dynamic : ?enabled:bool -> ?hum:string -> ?doc_url:string -> linters_def_file:string option -> id:string -> ?user_documentation:string -> severity -> IBase.Checker.t -> t
Create a new issue and register it in the list of all issues. NOTE: if the issue with the same string id is already registered, overrides `hum`, `doc_url`, and `linters_def_file`, but DOES NOT override `enabled`. This trick allows to deal with disabling/enabling dynamic AL issues from the config, when we don't know all params yet. Thus, the human-readable description can be updated when we encounter the definition of the issue type, eg in AL.
val checker_can_report : IBase.Checker.t -> t -> bool
Whether the issue was registered as coming from the given checker. Important to call this before reporting to keep documentation accurate.
val set_enabled : t -> bool -> unit
val abduction_case_not_implemented : t
val arbitrary_code_execution_under_lock : t
val array_of_pointsto : t
val array_out_of_bounds_l1 : t
val array_out_of_bounds_l2 : t
val array_out_of_bounds_l3 : t
val assert_failure : t
val biabduction_analysis_stops : t
val buffer_overrun_l1 : t
val buffer_overrun_l2 : t
val buffer_overrun_l3 : t
val buffer_overrun_l4 : t
val buffer_overrun_l5 : t
val buffer_overrun_s2 : t
val buffer_overrun_u5 : t
val cannot_star : t
val captured_strong_self : t
val checkers_allocates_memory : t
Warning name when a performance critical method directly or indirectly calls a method allocating memory
val checkers_annotation_reachability_error : t
val checkers_calls_expensive_method : t
Warning name when a performance critical method directly or indirectly calls a method annotatd as expensive
val checkers_expensive_overrides_unexpensive : t
Warning name for the subtyping rule: method not annotated as expensive cannot be overridden by a method annotated as expensive
val checkers_fragment_retain_view : t
val checkers_immutable_cast : t
val checkers_printf_args : t
val class_cast_exception : t
val complexity_increase : kind:IBase.CostKind.t -> is_on_ui_thread:bool -> t
val component_with_multiple_factory_methods : t
val condition_always_false : t
val condition_always_true : t
val config_checks_between_markers : t
val config_impact_analysis : t
val constant_address_dereference : t
val create_intent_from_uri : t
val cross_site_scripting : t
val dangling_pointer_dereference : t
val dangling_pointer_dereference_maybe : t
val dead_store : t
val deadlock : t
val divide_by_zero : t
val do_not_report : t
an issue type that should never be reported
val empty_vector_access : t
val eradicate_annotation_graph : t
val eradicate_condition_redundant : t
val eradicate_field_not_initialized : t
val eradicate_field_not_nullable : t
val eradicate_field_over_annotated : t
val eradicate_inconsistent_subclass_parameter_annotation : t
val eradicate_inconsistent_subclass_return_annotation : t
val eradicate_redundant_nested_class_annotation : t
val eradicate_bad_nested_class_annotation : t
val eradicate_nullable_dereference : t
val eradicate_parameter_not_nullable : t
val eradicate_return_not_nullable : t
val eradicate_return_over_annotated : t
val eradicate_unvetted_third_party_in_nullsafe : t
val eradicate_unchecked_usage_in_nullsafe : t
val eradicate_meta_class_can_be_nullsafe : t
val eradicate_meta_class_needs_improvement : t
val eradicate_meta_class_is_nullsafe : t
val exposed_insecure_intent_handling : t
val expensive_cost_call : kind:IBase.CostKind.t -> t
val failure_exe : t
val field_not_null_checked : t
val guardedby_violation : t
val guardedby_violation_nullsafe : t
val impure_function : t
val inefficient_keyset_iterator : t
val inferbo_alloc_is_big : t
val inferbo_alloc_is_negative : t
val inferbo_alloc_is_zero : t
val inferbo_alloc_may_be_big : t
val inferbo_alloc_may_be_negative : t
val infinite_cost_call : kind:IBase.CostKind.t -> t
val inherently_dangerous_function : t
val insecure_intent_handling : t
val integer_overflow_l1 : t
val integer_overflow_l2 : t
val integer_overflow_l5 : t
val integer_overflow_u5 : t
val interface_not_thread_safe : t
val internal_error : t
val invariant_call : t
val ipc_on_ui_thread : t
val javascript_injection : t
val lab_resource_leak : t
val dotnet_resource_leak : t
val leak_after_array_abstraction : t
val leak_unknown_origin : t
val lockless_violation : t
val lock_consistency_violation : t
val logging_private_data : t
val expensive_loop_invariant_call : t
val memory_leak : t
val missing_fld : t
val missing_required_prop : t
val mixed_self_weakself : t
val modifies_immutable : t
val multiple_weakself : t
val mutable_local_variable_in_component_file : t
val null_dereference : t
val nullptr_dereference : t
val optional_empty_access : t
val parameter_not_null_checked : t
val precondition_not_found : t
val precondition_not_met : t
val premature_nil_termination : t
val pulse_memory_leak : t
val pure_function : t
val quandary_taint_error : t
val resource_leak : t
val retain_cycle : t
val skip_function : t
val shell_injection : t
val shell_injection_risk : t
val sql_injection : t
val sql_injection_risk : t
val stack_variable_address_escape : t
val starvation : t
val static_initialization_order_fiasco : t
val strict_mode_violation : t
val strong_self_not_checked : t
val symexec_memory_error : t
val thread_safety_violation : t
val thread_safety_violation_nullsafe : t
val topl_biabd_error : t
val topl_pulse_error : t
val uninitialized_value : t
val uninitialized_value_pulse : t
val unreachable_code_after : t
val use_after_delete : t
val use_after_free : t
val use_after_lifetime : t
val untrusted_buffer_access : t
val untrusted_deserialization : t
val untrusted_deserialization_risk : t
val untrusted_file : t
val untrusted_file_risk : t
val untrusted_heap_allocation : t
val untrusted_intent_creation : t
val untrusted_url_risk : t
val untrusted_environment_change_risk : t
val untrusted_variable_length_array : t
val user_controlled_sql_risk : t
val vector_invalidation : t
val weak_self_in_noescape_block : t
val wrong_argument_number : t
val unreachable_cost_call : kind:IBase.CostKind.t -> t
val is_autoreleasepool_size_issue : t -> bool
\ No newline at end of file
+IBase__IssueType (infer.IBase__IssueType) Up – infer » IBase__IssueTypeModule IBase__IssueType
type visibility
=
|
User
always add to error log
|
Developer
only add to error log in some debug modes
|
Silent
never add to error log
visibility of the issue type
val string_of_visibility : visibility -> string
type severity
=
|
Like
|
Info
|
Advice
|
Warning
|
Error
severity of the report
val string_of_severity : severity -> string
type t
= private
{
unique_id : string;
checker : IBase.Checker.t ;
visibility : visibility ;
user_documentation : string option ;
mutable default_severity : severity ;
used for documentation but can be overriden at report time
mutable enabled : bool;
mutable hum : string;
mutable doc_url : string option ;
mutable linters_def_file : string option ;
}
val compare : t -> t -> int
val equal : t -> t -> bool
val all_issues : unit -> t list
all the issues declared so far
val pp : Stdlib.Format.formatter -> t -> unit
pretty print a localised string
val find_from_string : id:string -> t option
return the issue type if it was previously registered
val register_dynamic : ?enabled:bool -> ?hum:string -> ?doc_url:string -> linters_def_file:string option -> id:string -> ?user_documentation:string -> severity -> IBase.Checker.t -> t
Create a new issue and register it in the list of all issues. NOTE: if the issue with the same string id is already registered, overrides `hum`, `doc_url`, and `linters_def_file`, but DOES NOT override `enabled`. This trick allows to deal with disabling/enabling dynamic AL issues from the config, when we don't know all params yet. Thus, the human-readable description can be updated when we encounter the definition of the issue type, eg in AL.
val checker_can_report : IBase.Checker.t -> t -> bool
Whether the issue was registered as coming from the given checker. Important to call this before reporting to keep documentation accurate.
val set_enabled : t -> bool -> unit
val abduction_case_not_implemented : t
val arbitrary_code_execution_under_lock : t
val array_of_pointsto : t
val array_out_of_bounds_l1 : t
val array_out_of_bounds_l2 : t
val array_out_of_bounds_l3 : t
val assert_failure : t
val biabduction_analysis_stops : t
val buffer_overrun_l1 : t
val buffer_overrun_l2 : t
val buffer_overrun_l3 : t
val buffer_overrun_l4 : t
val buffer_overrun_l5 : t
val buffer_overrun_s2 : t
val buffer_overrun_u5 : t
val cannot_star : t
val captured_strong_self : t
val checkers_allocates_memory : t
Warning name when a performance critical method directly or indirectly calls a method allocating memory
val checkers_annotation_reachability_error : t
val checkers_calls_expensive_method : t
Warning name when a performance critical method directly or indirectly calls a method annotatd as expensive
val checkers_expensive_overrides_unexpensive : t
Warning name for the subtyping rule: method not annotated as expensive cannot be overridden by a method annotated as expensive
val checkers_fragment_retain_view : t
val checkers_immutable_cast : t
val checkers_printf_args : t
val class_cast_exception : t
val complexity_increase : kind:IBase.CostKind.t -> is_on_ui_thread:bool -> t
val component_with_multiple_factory_methods : t
val condition_always_false : t
val condition_always_true : t
val config_checks_between_markers : t
val config_impact_analysis : t
val constant_address_dereference : t
val create_intent_from_uri : t
val cross_site_scripting : t
val dangling_pointer_dereference : t
val dangling_pointer_dereference_maybe : t
val dead_store : t
val deadlock : t
val divide_by_zero : t
val do_not_report : t
an issue type that should never be reported
val empty_vector_access : t
val eradicate_annotation_graph : t
val eradicate_condition_redundant : t
val eradicate_field_not_initialized : t
val eradicate_field_not_nullable : t
val eradicate_field_over_annotated : t
val eradicate_inconsistent_subclass_parameter_annotation : t
val eradicate_inconsistent_subclass_return_annotation : t
val eradicate_redundant_nested_class_annotation : t
val eradicate_bad_nested_class_annotation : t
val eradicate_nullable_dereference : t
val eradicate_parameter_not_nullable : t
val eradicate_return_not_nullable : t
val eradicate_return_over_annotated : t
val eradicate_unvetted_third_party_in_nullsafe : t
val eradicate_unchecked_usage_in_nullsafe : t
val eradicate_meta_class_can_be_nullsafe : t
val eradicate_meta_class_needs_improvement : t
val eradicate_meta_class_is_nullsafe : t
val exposed_insecure_intent_handling : t
val expensive_cost_call : kind:IBase.CostKind.t -> t
val failure_exe : t
val field_not_null_checked : t
val guardedby_violation : t
val guardedby_violation_nullsafe : t
val impure_function : t
val inefficient_keyset_iterator : t
val inferbo_alloc_is_big : t
val inferbo_alloc_is_negative : t
val inferbo_alloc_is_zero : t
val inferbo_alloc_may_be_big : t
val inferbo_alloc_may_be_negative : t
val infinite_cost_call : kind:IBase.CostKind.t -> t
val inherently_dangerous_function : t
val insecure_intent_handling : t
val integer_overflow_l1 : t
val integer_overflow_l2 : t
val integer_overflow_l5 : t
val integer_overflow_u5 : t
val interface_not_thread_safe : t
val internal_error : t
val invariant_call : t
val ipc_on_ui_thread : t
val javascript_injection : t
val lab_resource_leak : t
val dotnet_resource_leak : t
val leak_after_array_abstraction : t
val leak_unknown_origin : t
val lockless_violation : t
val lock_consistency_violation : t
val logging_private_data : t
val expensive_loop_invariant_call : t
val memory_leak : t
val missing_fld : t
val missing_required_prop : t
val mixed_self_weakself : t
val modifies_immutable : t
val multiple_weakself : t
val mutable_local_variable_in_component_file : t
val null_dereference : t
val nullptr_dereference : t
val optional_empty_access : t
val parameter_not_null_checked : t
val precondition_not_found : t
val precondition_not_met : t
val premature_nil_termination : t
val pulse_memory_leak : t
val pure_function : t
val quandary_taint_error : t
val resource_leak : t
val retain_cycle : t
val skip_function : t
val shell_injection : t
val shell_injection_risk : t
val sql_injection : t
val sql_injection_risk : t
val stack_variable_address_escape : t
val starvation : t
val static_initialization_order_fiasco : t
val strict_mode_violation : t
val strong_self_not_checked : t
val symexec_memory_error : t
val thread_safety_violation : t
val thread_safety_violation_nullsafe : t
val topl_error : t
val uninitialized_value : t
val uninitialized_value_pulse : t
val unreachable_code_after : t
val use_after_delete : t
val use_after_free : t
val use_after_lifetime : t
val untrusted_buffer_access : t
val untrusted_deserialization : t
val untrusted_deserialization_risk : t
val untrusted_file : t
val untrusted_file_risk : t
val untrusted_heap_allocation : t
val untrusted_intent_creation : t
val untrusted_url_risk : t
val untrusted_environment_change_risk : t
val untrusted_variable_length_array : t
val user_controlled_sql_risk : t
val vector_invalidation : t
val weak_self_in_noescape_block : t
val wrong_argument_number : t
val unreachable_cost_call : kind:IBase.CostKind.t -> t
val is_autoreleasepool_size_issue : t -> bool
\ No newline at end of file
diff --git a/website/static/odoc/next/infer/IR/Exp/index.html b/website/static/odoc/next/infer/IR/Exp/index.html
index 23e0eb823..16ca479da 100644
--- a/website/static/odoc/next/infer/IR/Exp/index.html
+++ b/website/static/odoc/next/infer/IR/Exp/index.html
@@ -1,2 +1,2 @@
-Exp (infer.IR.Exp) The Smallfoot Intermediate Language: Expressions
NOTE: For doing substitutionson expressions, there are some functions in Sil
.
type closure
=
{
}
and sizeof_data
=
{
typ : Typ.t ;
nbytes : int option ;
dynamic_length : t option ;
subtype : Subtype.t ;
}
This records information about a sizeof(typ)
expression.
nbytes
represents the result of the evaluation of sizeof(typ)
if it is statically known.
If typ
is of the form Tarray elt (Some static_length)
, then dynamic_length
is the number of elements of type elt
in the array. The dynamic_length
, tracked by symbolic execution, may differ from the static_length
obtained from the type definition, e.g. when an array is over-allocated.
If typ
is a struct type, the dynamic_length
is that of the final extensible array, if any.
and t
=
|
Var of Ident.t
Pure variable: it is not an lvalue
|
UnOp of Unop.t * t * Typ.t option
Unary operator with type of the result if known
|
BinOp of Binop.t * t * t
Binary operator
|
Exn of t
Exception
|
Closure of closure
Anonymous function
|
Const of Const.t
Constants
|
Cast of Typ.t * t
Type cast
|
Lvar of Pvar.t
The address of a program variable
|
Lfield of t * Fieldname.t * Typ.t
A field offset, the type is the surrounding struct type
|
Lindex of t * t
An array index offset: exp1[exp2]
|
Sizeof of sizeof_data
Program expressions.
val equal : t -> t -> bool
Equality for expressions.
module Set : IStdlib.IStd .Caml.Set.S with type Set .elt = t
Set of expressions.
module Map : IStdlib.IStd .Caml.Map.S with type Map .key = t
Map with expression keys.
module Hash : IStdlib.IStd .Caml.Hashtbl.S with type Hash .key = t
Hashtable with expression keys.
val is_null_literal : t -> bool
val is_this : t -> bool
return true if exp
is the special this/self expression
val is_zero : t -> bool
val is_const : t -> bool
Utility Functions for Expressionsval texp_to_typ : Typ.t option -> t -> Typ.t
Turn an expression representing a type into the type it represents If not a sizeof, return the default type if given, otherwise raise an exception
val root_of_lexp : t -> t
Return the root of lexp
.
val get_undefined : bool -> t
Get an expression "undefined", the boolean indicates whether the undefined value goest into the footprint
val pointer_arith : t -> bool
Checks whether an expression denotes a location using pointer arithmetic. Currently, catches array - indexing expressions such as ai
only.
val has_local_addr : t -> bool
returns true if the expression operates on address of local variable
val zero : t
Integer constant 0
val null : t
Null constant
val one : t
Integer constant 1
val minus_one : t
Integer constant -1
val int : IntLit.t -> t
Create integer constant
val float : float -> t
Create float constant
val bool : bool -> t
Create integer constant corresponding to the boolean value
val eq : t -> t -> t
Create expression e1 == e2
val ne : t -> t -> t
Create expression e1 != e2
val le : t -> t -> t
Create expression e1 <= e2
val lt : t -> t -> t
Create expression e1 < e2
val and_nary : t list -> t
Create expression e1 && e2 && e3 && ...
val free_vars : t -> Ident.t IStdlib.IStd .Sequence.t
all the idents appearing in the expression
val gen_free_vars : t -> (unit, Ident.t ) IStdlib.IStd .Sequence.Generator.t
val ident_mem : t -> Ident.t -> bool
true if the identifier appears in the expression
val program_vars : t -> Pvar.t IStdlib.IStd .Sequence.t
all the program variables appearing in the expression
val rename_pvars : f:(string -> string) -> t -> t
Rename all Pvars according to the function f
. WARNING: You want to rename pvars before you combine expressions from different symbolic states, which you RARELY want to.
val fold_captured : f:('a -> t -> 'a ) -> t -> 'a -> 'a
Fold over the expressions captured by this expression.
val pp_diff : ?print_types:bool -> IStdlib.Pp.env -> F .formatter -> t -> unit
val pp : F .formatter -> t -> unit
val pp_closure : F .formatter -> closure -> unit
val to_string : t -> string
val d_exp : t -> unit
dump an expression.
val pp_texp : IStdlib.Pp.env -> F .formatter -> t -> unit
Pretty print a type.
val pp_texp_full : IStdlib.Pp.env -> F .formatter -> t -> unit
Pretty print a type with all the details.
val d_texp_full : t -> unit
Dump a type expression with all the details.
val d_list : t list -> unit
Dump a list of expressions.
val is_objc_block_closure : t -> bool
val zero_of_type : Typ.t -> t option
Returns the zero value of a type, for int, float and ptr types
val zero_of_type_exn : Typ.t -> t
val ignore_cast : t -> t
val ignore_integer_cast : t -> t
val get_java_class_initializer : Tenv.t -> t -> (Procname.t * Pvar.t * Fieldname.t * Typ.t ) option
Returns the class initializer of the given expression in Java
\ No newline at end of file
+Exp (infer.IR.Exp) The Smallfoot Intermediate Language: Expressions
NOTE: For doing substitutionson expressions, there are some functions in Sil
.
type closure
=
{
}
and sizeof_data
=
{
typ : Typ.t ;
nbytes : int option ;
dynamic_length : t option ;
subtype : Subtype.t ;
}
This records information about a sizeof(typ)
expression.
nbytes
represents the result of the evaluation of sizeof(typ)
if it is statically known.
If typ
is of the form Tarray elt (Some static_length)
, then dynamic_length
is the number of elements of type elt
in the array. The dynamic_length
, tracked by symbolic execution, may differ from the static_length
obtained from the type definition, e.g. when an array is over-allocated.
If typ
is a struct type, the dynamic_length
is that of the final extensible array, if any.
and t
=
|
Var of Ident.t
Pure variable: it is not an lvalue
|
UnOp of Unop.t * t * Typ.t option
Unary operator with type of the result if known
|
BinOp of Binop.t * t * t
Binary operator
|
Exn of t
Exception
|
Closure of closure
Anonymous function
|
Const of Const.t
Constants
|
Cast of Typ.t * t
Type cast
|
Lvar of Pvar.t
The address of a program variable
|
Lfield of t * Fieldname.t * Typ.t
A field offset, the type is the surrounding struct type
|
Lindex of t * t
An array index offset: exp1[exp2]
|
Sizeof of sizeof_data
Program expressions.
val equal : t -> t -> bool
Equality for expressions.
module Set : IStdlib.IStd .Caml.Set.S with type Set .elt = t
Set of expressions.
module Map : IStdlib.IStd .Caml.Map.S with type Map .key = t
Map with expression keys.
module Hash : IStdlib.IStd .Caml.Hashtbl.S with type Hash .key = t
Hashtable with expression keys.
val is_null_literal : t -> bool
val is_this : t -> bool
return true if exp
is the special this/self expression
val is_zero : t -> bool
val is_const : t -> bool
Utility Functions for Expressionsval texp_to_typ : Typ.t option -> t -> Typ.t
Turn an expression representing a type into the type it represents If not a sizeof, return the default type if given, otherwise raise an exception
val root_of_lexp : t -> t
Return the root of lexp
.
val get_undefined : bool -> t
Get an expression "undefined", the boolean indicates whether the undefined value goest into the footprint
val pointer_arith : t -> bool
Checks whether an expression denotes a location using pointer arithmetic. Currently, catches array - indexing expressions such as ai
only.
val has_local_addr : t -> bool
returns true if the expression operates on address of local variable
val zero : t
Integer constant 0
val null : t
Null constant
val one : t
Integer constant 1
val minus_one : t
Integer constant -1
val int : IntLit.t -> t
Create integer constant
val float : float -> t
Create float constant
val bool : bool -> t
Create integer constant corresponding to the boolean value
val eq : t -> t -> t
Create expression e1 == e2
val ne : t -> t -> t
Create expression e1 != e2
val le : t -> t -> t
Create expression e1 <= e2
val lt : t -> t -> t
Create expression e1 < e2
val free_vars : t -> Ident.t IStdlib.IStd .Sequence.t
all the idents appearing in the expression
val gen_free_vars : t -> (unit, Ident.t ) IStdlib.IStd .Sequence.Generator.t
val ident_mem : t -> Ident.t -> bool
true if the identifier appears in the expression
val program_vars : t -> Pvar.t IStdlib.IStd .Sequence.t
all the program variables appearing in the expression
val fold_captured : f:('a -> t -> 'a ) -> t -> 'a -> 'a
Fold over the expressions captured by this expression.
val pp_diff : ?print_types:bool -> IStdlib.Pp.env -> F .formatter -> t -> unit
val pp : F .formatter -> t -> unit
val pp_closure : F .formatter -> closure -> unit
val to_string : t -> string
val d_exp : t -> unit
dump an expression.
val pp_texp : IStdlib.Pp.env -> F .formatter -> t -> unit
Pretty print a type.
val pp_texp_full : IStdlib.Pp.env -> F .formatter -> t -> unit
Pretty print a type with all the details.
val d_texp_full : t -> unit
Dump a type expression with all the details.
val d_list : t list -> unit
Dump a list of expressions.
val is_objc_block_closure : t -> bool
val zero_of_type : Typ.t -> t option
Returns the zero value of a type, for int, float and ptr types
val zero_of_type_exn : Typ.t -> t
val ignore_cast : t -> t
val ignore_integer_cast : t -> t
val get_java_class_initializer : Tenv.t -> t -> (Procname.t * Pvar.t * Fieldname.t * Typ.t ) option
Returns the class initializer of the given expression in Java
\ No newline at end of file
diff --git a/website/static/odoc/next/infer/IR/Mangled/index.html b/website/static/odoc/next/infer/IR/Mangled/index.html
index 95be3bddb..667fc5499 100644
--- a/website/static/odoc/next/infer/IR/Mangled/index.html
+++ b/website/static/odoc/next/infer/IR/Mangled/index.html
@@ -1,2 +1,2 @@
-Mangled (infer.IR.Mangled) type t
Type of mangled names
val compare : t -> t -> int
val yojson_of_t : t -> Ppx_yojson_conv_lib.Yojson.Safe.t
val equal : t -> t -> bool
Equality for mangled names
val from_string : string -> t
Convert a string to a mangled name
val mangled : string -> string -> t
Create a mangled name from a plain and mangled string
val to_string : t -> string
Convert a mangled name to a string
val to_string_full : t -> string
Convert a full mangled name to a string
val pp : Stdlib.Format.formatter -> t -> unit
Pretty print a mangled name
val this : t
val is_this : t -> bool
val self : t
val is_self : t -> bool
val rename : f:(string -> string) -> t -> t
Maps over both the plain and the mangled components.
module Set : IStdlib.PrettyPrintable.PPSet with type PPSet .elt = t
Set of Mangled.
module Map : IStdlib.PrettyPrintable.PPMap with type PPMap .key = t
Map with Mangled as key
\ No newline at end of file
+Mangled (infer.IR.Mangled) type t
Type of mangled names
val compare : t -> t -> int
val yojson_of_t : t -> Ppx_yojson_conv_lib.Yojson.Safe.t
val equal : t -> t -> bool
Equality for mangled names
val from_string : string -> t
Convert a string to a mangled name
val mangled : string -> string -> t
Create a mangled name from a plain and mangled string
val to_string : t -> string
Convert a mangled name to a string
val to_string_full : t -> string
Convert a full mangled name to a string
val pp : Stdlib.Format.formatter -> t -> unit
Pretty print a mangled name
val this : t
val is_this : t -> bool
val self : t
val is_self : t -> bool
module Set : IStdlib.PrettyPrintable.PPSet with type PPSet .elt = t
Set of Mangled.
module Map : IStdlib.PrettyPrintable.PPMap with type PPMap .key = t
Map with Mangled as key
\ No newline at end of file
diff --git a/website/static/odoc/next/infer/IR/Procdesc/index.html b/website/static/odoc/next/infer/IR/Procdesc/index.html
index 27289db28..eea1b8e62 100644
--- a/website/static/odoc/next/infer/IR/Procdesc/index.html
+++ b/website/static/odoc/next/infer/IR/Procdesc/index.html
@@ -1,2 +1,2 @@
-Procdesc (infer.IR.Procdesc) module Node : sig ... end
node of the control flow graph
module IdMap : IStdlib.PrettyPrintable.PPMap with type PPMap .key = Node.id
Map with node id keys.
module NodeHash : IStdlib.IStd .Caml.Hashtbl.S with type NodeHash .key = Node.t
Hash table with nodes as keys.
module NodeMap : IStdlib.IStd .Caml.Map.S with type NodeMap .key = Node.t
Map over nodes.
module NodeSet : IStdlib.IStd .Caml.Set.S with type NodeSet .elt = Node.t
Set of nodes.
type t
proc description
val append_locals : t -> ProcAttributes.var_data list -> unit
append a list of new local variables to the existing list of local variables
val compute_distance_to_exit_node : t -> unit
Compute the distance of each node to the exit node, if not computed already
val create_node : t -> IBase.Location.t -> Node.nodekind -> Sil.instr list -> Node.t
Create a new cfg node with the given location, kind, list of instructions, and add it to the procdesc.
val create_node_from_not_reversed : t -> IBase.Location.t -> Node.nodekind -> Instrs.not_reversed_t -> Node.t
val fold_instrs : t -> init:'accum -> f:('accum -> Node.t -> Sil.instr -> 'accum ) -> 'accum
fold over all nodes and their instructions
val find_map_instrs : t -> f:(Sil.instr -> 'a option ) -> 'a option
val from_proc_attributes : ProcAttributes.t -> t
Use Cfg.create_proc_desc
if you are adding a proc desc to a cfg
val get_access : t -> PredSymb.access
Return the visibility attribute
val get_attributes : t -> ProcAttributes.t
Get the attributes of the procedure.
val set_attributes : t -> ProcAttributes.t -> unit
val get_captured : t -> CapturedVar.t list
Return name and type of block's captured variables
val get_exit_node : t -> Node.t
val get_formals : t -> (Mangled.t * Typ.t ) list
Return name and type of formal parameters
val get_pvar_formals : t -> (Pvar.t * Typ.t ) list
Return pvar and type of formal parameters
val get_loc : t -> IBase.Location.t
Return loc information for the procedure
val get_locals : t -> ProcAttributes.var_data list
Return name and type and attributes of local variables
val get_nodes : t -> Node.t list
val get_proc_name : t -> Procname.t
val get_ret_type : t -> Typ.t
Return the return type of the procedure and type string
val has_added_return_param : t -> bool
val is_ret_type_pod : t -> bool
val get_ret_var : t -> Pvar.t
val get_start_node : t -> Node.t
val get_static_callees : t -> Procname.t list
get a list of unique static callees excluding self
val is_defined : t -> bool
Return true
iff the procedure is defined, and not just declared
val is_java_synchronized : t -> bool
Return true
if the procedure signature has the Java synchronized keyword
val is_objc_arc_on : t -> bool
Return true
iff the ObjC procedure is compiled with ARC
val iter_instrs : (Node.t -> Sil.instr -> unit) -> t -> unit
iterate over all nodes and their instructions
val replace_instrs : t -> f:(Node.t -> Sil.instr -> Sil.instr ) -> bool
Map and replace the instructions to be executed. Returns true if at least one substitution occured.
val replace_instrs_using_context : t -> f:(Node.t -> 'a -> Sil.instr -> Sil.instr ) -> update_context:('a -> Sil.instr -> 'a ) -> context_at_node:(Node.t -> 'a ) -> bool
Map and replace the instructions to be executed using a context that we built with previous instructions in the node. Returns true if at least one substitution occured.
val replace_instrs_by_using_context : t -> f:(Node.t -> 'a -> Sil.instr -> Sil.instr array ) -> update_context:('a -> Sil.instr -> 'a ) -> context_at_node:(Node.t -> 'a ) -> bool
Like replace_instrs_using_context
, but slower, and each instruction may be replaced by 0, 1, or more instructions.
val replace_instrs_by : t -> f:(Node.t -> Sil.instr -> Sil.instr array ) -> bool
Like replace_instrs
, but slower, and each instruction may be replaced by 0, 1, or more instructions.
val iter_nodes : (Node.t -> unit) -> t -> unit
iterate over all the nodes of a procedure
val fold_nodes : t -> init:'accum -> f:('accum -> Node.t -> 'accum ) -> 'accum
fold over all the nodes of a procedure
val fold_slope_range : Node.t -> Node.t -> init:'accum -> f:('accum -> Node.t -> 'accum ) -> 'accum
fold between two nodes or until we reach a branching structure
val set_succs : Node.t -> normal:Node.t list option -> exn:Node.t list option -> unit
Set the successor nodes and exception nodes, if given, and update predecessor links
val node_set_succs : t -> Node.t -> normal:Node.t list -> exn:Node.t list -> unit
Set the successor nodes and exception nodes, and update predecessor links
val set_exit_node : t -> Node.t -> unit
Set the exit node of the procedure
val set_start_node : t -> Node.t -> unit
val get_wto : t -> Node.t WeakTopologicalOrder.Partition.t
val is_loop_head : t -> Node.t -> bool
val pp_signature : Stdlib.Format.formatter -> t -> unit
val pp_local : Stdlib.Format.formatter -> ProcAttributes.var_data -> unit
val is_specialized : t -> bool
val is_captured_pvar : t -> Pvar.t -> bool
true if pvar is a captured variable of a cpp lambda or obcj block
val is_captured_var : t -> Var.t -> bool
true if var is a captured variable of a cpp lambda or obcj block
val has_modify_in_block_attr : t -> Pvar.t -> bool
val shallow_copy_code_from_pdesc : orig_pdesc:t -> dest_pdesc:t -> unit
module SQLite : IBase.SqliteUtils.Data with type t = t option
per-procedure CFGs are stored in the SQLite "procedures" table as NULL if the procedure has no CFG
val load : Procname.t -> t option
\ No newline at end of file
+Procdesc (infer.IR.Procdesc) module Node : sig ... end
node of the control flow graph
module IdMap : IStdlib.PrettyPrintable.PPMap with type PPMap .key = Node.id
Map with node id keys.
module NodeHash : IStdlib.IStd .Caml.Hashtbl.S with type NodeHash .key = Node.t
Hash table with nodes as keys.
module NodeMap : IStdlib.IStd .Caml.Map.S with type NodeMap .key = Node.t
Map over nodes.
module NodeSet : IStdlib.IStd .Caml.Set.S with type NodeSet .elt = Node.t
Set of nodes.
type t
proc description
val append_locals : t -> ProcAttributes.var_data list -> unit
append a list of new local variables to the existing list of local variables
val compute_distance_to_exit_node : t -> unit
Compute the distance of each node to the exit node, if not computed already
val create_node : t -> IBase.Location.t -> Node.nodekind -> Sil.instr list -> Node.t
Create a new cfg node with the given location, kind, list of instructions, and add it to the procdesc.
val create_node_from_not_reversed : t -> IBase.Location.t -> Node.nodekind -> Instrs.not_reversed_t -> Node.t
val fold_instrs : t -> init:'accum -> f:('accum -> Node.t -> Sil.instr -> 'accum ) -> 'accum
fold over all nodes and their instructions
val find_map_instrs : t -> f:(Sil.instr -> 'a option ) -> 'a option
val from_proc_attributes : ProcAttributes.t -> t
Use Cfg.create_proc_desc
if you are adding a proc desc to a cfg
val get_access : t -> PredSymb.access
Return the visibility attribute
val get_attributes : t -> ProcAttributes.t
Get the attributes of the procedure.
val set_attributes : t -> ProcAttributes.t -> unit
val get_captured : t -> CapturedVar.t list
Return name and type of block's captured variables
val get_exit_node : t -> Node.t
val get_formals : t -> (Mangled.t * Typ.t ) list
Return name and type of formal parameters
val get_pvar_formals : t -> (Pvar.t * Typ.t ) list
Return pvar and type of formal parameters
val get_loc : t -> IBase.Location.t
Return loc information for the procedure
val get_locals : t -> ProcAttributes.var_data list
Return name and type and attributes of local variables
val get_nodes : t -> Node.t list
val get_proc_name : t -> Procname.t
val get_ret_type : t -> Typ.t
Return the return type of the procedure and type string
val has_added_return_param : t -> bool
val is_ret_type_pod : t -> bool
val get_ret_var : t -> Pvar.t
val get_start_node : t -> Node.t
val get_static_callees : t -> Procname.t list
get a list of unique static callees excluding self
val is_defined : t -> bool
Return true
iff the procedure is defined, and not just declared
val is_java_synchronized : t -> bool
Return true
if the procedure signature has the Java synchronized keyword
val is_objc_arc_on : t -> bool
Return true
iff the ObjC procedure is compiled with ARC
val iter_instrs : (Node.t -> Sil.instr -> unit) -> t -> unit
iterate over all nodes and their instructions
val replace_instrs : t -> f:(Node.t -> Sil.instr -> Sil.instr ) -> bool
Map and replace the instructions to be executed. Returns true if at least one substitution occured.
val replace_instrs_using_context : t -> f:(Node.t -> 'a -> Sil.instr -> Sil.instr ) -> update_context:('a -> Sil.instr -> 'a ) -> context_at_node:(Node.t -> 'a ) -> bool
Map and replace the instructions to be executed using a context that we built with previous instructions in the node. Returns true if at least one substitution occured.
val replace_instrs_by_using_context : t -> f:(Node.t -> 'a -> Sil.instr -> Sil.instr array ) -> update_context:('a -> Sil.instr -> 'a ) -> context_at_node:(Node.t -> 'a ) -> bool
Like replace_instrs_using_context
, but slower, and each instruction may be replaced by 0, 1, or more instructions.
val iter_nodes : (Node.t -> unit) -> t -> unit
iterate over all the nodes of a procedure
val fold_nodes : t -> init:'accum -> f:('accum -> Node.t -> 'accum ) -> 'accum
fold over all the nodes of a procedure
val fold_slope_range : Node.t -> Node.t -> init:'accum -> f:('accum -> Node.t -> 'accum ) -> 'accum
fold between two nodes or until we reach a branching structure
val set_succs : Node.t -> normal:Node.t list option -> exn:Node.t list option -> unit
Set the successor nodes and exception nodes, if given, and update predecessor links
val node_set_succs : t -> Node.t -> normal:Node.t list -> exn:Node.t list -> unit
Set the successor nodes and exception nodes, and update predecessor links
val set_exit_node : t -> Node.t -> unit
Set the exit node of the procedure
val set_start_node : t -> Node.t -> unit
val get_wto : t -> Node.t WeakTopologicalOrder.Partition.t
val is_loop_head : t -> Node.t -> bool
val pp_signature : Stdlib.Format.formatter -> t -> unit
val pp_local : Stdlib.Format.formatter -> ProcAttributes.var_data -> unit
val is_specialized : t -> bool
val is_captured_pvar : t -> Pvar.t -> bool
true if pvar is a captured variable of a cpp lambda or obcj block
val is_captured_var : t -> Var.t -> bool
true if var is a captured variable of a cpp lambda or obcj block
val has_modify_in_block_attr : t -> Pvar.t -> bool
val shallow_copy_code_from_pdesc : orig_pdesc:t -> dest_pdesc:t -> unit
module SQLite : IBase.SqliteUtils.Data with type t = t option
per-procedure CFGs are stored in the SQLite "procedures" table as NULL if the procedure has no CFG
val load : Procname.t -> t option
\ No newline at end of file
diff --git a/website/static/odoc/next/infer/IR/Pvar/index.html b/website/static/odoc/next/infer/IR/Pvar/index.html
index 8a328d0e8..b5d99d7b2 100644
--- a/website/static/odoc/next/infer/IR/Pvar/index.html
+++ b/website/static/odoc/next/infer/IR/Pvar/index.html
@@ -1,2 +1,2 @@
-Pvar (infer.IR.Pvar) type translation_unit
= IBase.SourceFile.t option
type t
Type for program variables. There are 4 kinds of variables:
local variables, used for local variables and formal parameters callee program variables, used to handle recursion (x | callee
is distinguished from x
) global variables seed variables, used to store the initial value of formal parameters val compare : t -> t -> int
val yojson_of_t : t -> Ppx_yojson_conv_lib.Yojson.Safe.t
val compare_modulo_this : t -> t -> int
Comparison considering all pvars named 'this'/'self' to be equal
val equal : t -> t -> bool
Equality for pvar's
val get_declaring_function : t -> Procname.t option
if not a global, return function declaring var
val d : t -> unit
Dump a program variable.
val get_name : t -> Mangled.t
Get the name component of a program variable.
val get_ret_pvar : Procname.t -> t
get_ret_pvar proc_name
retuns the return pvar associated with the procedure name
val get_ret_param_pvar : Procname.t -> t
get_ret_param_pvar proc_name
retuns the return_param pvar associated with the procedure name
val get_simplified_name : t -> string
Get a simplified version of the name component of a program variable.
val is_abduced : t -> bool
Check if the pvar is an abduced return var or param passed by ref
val is_callee : t -> bool
Check if the pvar is a callee var
val is_global : t -> bool
Check if the pvar is a global var or a static local var
val is_static_local : t -> bool
Check if the pvar is a static variable declared inside a function
val is_constant_array : t -> bool
Check if the pvar has a constant array type
val is_const : t -> bool
Check if the pvar has a const type
val is_local : t -> bool
Check if the pvar is a (non-static) local var
val is_seed : t -> bool
Check if the pvar is a seed var
val is_return : t -> bool
Check if the pvar is a return var
val is_this : t -> bool
Check if a pvar is the special "this" var
val is_self : t -> bool
Check if a pvar is the special "self" var
val is_frontend_tmp : t -> bool
return true if pvar
is a temporary variable generated by the frontend
val is_clang_tmp : t -> bool
return true if pvar
is a temporary variable generated by clang
val is_ssa_frontend_tmp : t -> bool
return true if pvar
is a temporary variable generated by the frontend and is only assigned once on a non-looping control-flow path
val is_cpp_temporary : t -> bool
return true if this pvar represents a C++ temporary object (see http://en.cppreference.com/w/cpp/language/lifetime)
val is_objc_static_local_of_proc_name : string -> t -> bool
Check if a pvar is a local static in objc
val is_block_pvar : t -> bool
Check if a pvar is a local pointing to a block in objc
val mk : Mangled.t -> Procname.t -> t
mk name proc_name
creates a program var with the given function name
val mk_abduced_ref_param : Procname.t -> int -> IBase.Location.t -> t
create an abduced variable for a parameter passed by reference
val mk_abduced_ret : Procname.t -> IBase.Location.t -> t
create an abduced return variable for a call to proc_name
at loc
val mk_callee : Mangled.t -> Procname.t -> t
mk_callee name proc_name
creates a program var for a callee function with the given function name
val mk_global : ?is_constexpr:bool -> ?is_ice:bool -> ?is_pod:bool -> ?is_static_local:bool -> ?is_static_global:bool -> ?is_constant_array:bool -> ?is_const:bool -> ?translation_unit:IBase.SourceFile.t -> Mangled.t -> t
create a global variable with the given name
val mk_tmp : string -> Procname.t -> t
create a fresh temporary variable local to procedure pname
. for use in the frontends only!
val pp : IStdlib.Pp.env -> F .formatter -> t -> unit
Pretty print a program variable.
val pp_value : F .formatter -> t -> unit
Pretty print a pvar which denotes a value, not an address
val pp_value_non_verbose : F .formatter -> t -> unit
Non-verbose version of pp_value
val pp_translation_unit : F .formatter -> translation_unit -> unit
val to_callee : Procname.t -> t -> t
Turn an ordinary program variable into a callee program variable
val to_seed : t -> t
Turn a pvar into a seed pvar (which stores the initial value of a stack var)
val to_string : t -> string
Convert a pvar to string.
val get_translation_unit : t -> translation_unit
Get the translation unit corresponding to a global. Raises Invalid_arg if not a global.
val is_compile_constant : t -> bool
Is the variable's value a compile-time constant? Always (potentially incorrectly) returns false
for non-globals.
val is_ice : t -> bool
Is the variable's type an integral constant expression? Always (potentially incorrectly) returns false
for non-globals.
val is_pod : t -> bool
Is the variable's type a "Plain Old Data" type (C++)? Always (potentially incorrectly) returns true
for non-globals.
val get_initializer_pname : t -> Procname.t option
Get the procname of the initializer function for the given global variable
val build_formal_from_pvar : t -> Mangled.t
build_formal_from_pvar var
Return a name that is composed of the name of var (and the name of the procname in case of locals)
val materialized_cpp_temporary : string
val swap_proc_in_local_pvar : t -> Procname.t -> t
val rename : f:(string -> string) -> t -> t
module Set : IStdlib.PrettyPrintable.PPSet with type PPSet .elt = t
Sets of pvars.
type capture_mode
=
val string_of_capture_mode : capture_mode -> string
\ No newline at end of file
+Pvar (infer.IR.Pvar) type translation_unit
= IBase.SourceFile.t option
type t
Type for program variables. There are 4 kinds of variables:
local variables, used for local variables and formal parameters callee program variables, used to handle recursion (x | callee
is distinguished from x
) global variables seed variables, used to store the initial value of formal parameters val compare : t -> t -> int
val yojson_of_t : t -> Ppx_yojson_conv_lib.Yojson.Safe.t
val compare_modulo_this : t -> t -> int
Comparison considering all pvars named 'this'/'self' to be equal
val equal : t -> t -> bool
Equality for pvar's
val get_declaring_function : t -> Procname.t option
if not a global, return function declaring var
val d : t -> unit
Dump a program variable.
val get_name : t -> Mangled.t
Get the name component of a program variable.
val get_ret_pvar : Procname.t -> t
get_ret_pvar proc_name
retuns the return pvar associated with the procedure name
val get_ret_param_pvar : Procname.t -> t
get_ret_param_pvar proc_name
retuns the return_param pvar associated with the procedure name
val get_simplified_name : t -> string
Get a simplified version of the name component of a program variable.
val is_abduced : t -> bool
Check if the pvar is an abduced return var or param passed by ref
val is_callee : t -> bool
Check if the pvar is a callee var
val is_global : t -> bool
Check if the pvar is a global var or a static local var
val is_static_local : t -> bool
Check if the pvar is a static variable declared inside a function
val is_constant_array : t -> bool
Check if the pvar has a constant array type
val is_const : t -> bool
Check if the pvar has a const type
val is_local : t -> bool
Check if the pvar is a (non-static) local var
val is_seed : t -> bool
Check if the pvar is a seed var
val is_return : t -> bool
Check if the pvar is a return var
val is_this : t -> bool
Check if a pvar is the special "this" var
val is_self : t -> bool
Check if a pvar is the special "self" var
val is_frontend_tmp : t -> bool
return true if pvar
is a temporary variable generated by the frontend
val is_clang_tmp : t -> bool
return true if pvar
is a temporary variable generated by clang
val is_ssa_frontend_tmp : t -> bool
return true if pvar
is a temporary variable generated by the frontend and is only assigned once on a non-looping control-flow path
val is_cpp_temporary : t -> bool
return true if this pvar represents a C++ temporary object (see http://en.cppreference.com/w/cpp/language/lifetime)
val is_objc_static_local_of_proc_name : string -> t -> bool
Check if a pvar is a local static in objc
val is_block_pvar : t -> bool
Check if a pvar is a local pointing to a block in objc
val mk : Mangled.t -> Procname.t -> t
mk name proc_name
creates a program var with the given function name
val mk_abduced_ref_param : Procname.t -> int -> IBase.Location.t -> t
create an abduced variable for a parameter passed by reference
val mk_abduced_ret : Procname.t -> IBase.Location.t -> t
create an abduced return variable for a call to proc_name
at loc
val mk_callee : Mangled.t -> Procname.t -> t
mk_callee name proc_name
creates a program var for a callee function with the given function name
val mk_global : ?is_constexpr:bool -> ?is_ice:bool -> ?is_pod:bool -> ?is_static_local:bool -> ?is_static_global:bool -> ?is_constant_array:bool -> ?is_const:bool -> ?translation_unit:IBase.SourceFile.t -> Mangled.t -> t
create a global variable with the given name
val mk_tmp : string -> Procname.t -> t
create a fresh temporary variable local to procedure pname
. for use in the frontends only!
val pp : IStdlib.Pp.env -> F .formatter -> t -> unit
Pretty print a program variable.
val pp_value : F .formatter -> t -> unit
Pretty print a pvar which denotes a value, not an address
val pp_value_non_verbose : F .formatter -> t -> unit
Non-verbose version of pp_value
val pp_translation_unit : F .formatter -> translation_unit -> unit
val to_callee : Procname.t -> t -> t
Turn an ordinary program variable into a callee program variable
val to_seed : t -> t
Turn a pvar into a seed pvar (which stores the initial value of a stack var)
val to_string : t -> string
Convert a pvar to string.
val get_translation_unit : t -> translation_unit
Get the translation unit corresponding to a global. Raises Invalid_arg if not a global.
val is_compile_constant : t -> bool
Is the variable's value a compile-time constant? Always (potentially incorrectly) returns false
for non-globals.
val is_ice : t -> bool
Is the variable's type an integral constant expression? Always (potentially incorrectly) returns false
for non-globals.
val is_pod : t -> bool
Is the variable's type a "Plain Old Data" type (C++)? Always (potentially incorrectly) returns true
for non-globals.
val get_initializer_pname : t -> Procname.t option
Get the procname of the initializer function for the given global variable
val build_formal_from_pvar : t -> Mangled.t
build_formal_from_pvar var
Return a name that is composed of the name of var (and the name of the procname in case of locals)
val materialized_cpp_temporary : string
val swap_proc_in_local_pvar : t -> Procname.t -> t
module Set : IStdlib.PrettyPrintable.PPSet with type PPSet .elt = t
Sets of pvars.
type capture_mode
=
val string_of_capture_mode : capture_mode -> string
\ No newline at end of file
diff --git a/website/static/odoc/next/infer/IR__Exp/index.html b/website/static/odoc/next/infer/IR__Exp/index.html
index 4870dd7e1..e9103e948 100644
--- a/website/static/odoc/next/infer/IR__Exp/index.html
+++ b/website/static/odoc/next/infer/IR__Exp/index.html
@@ -1,2 +1,2 @@
-IR__Exp (infer.IR__Exp) Up – infer » IR__ExpModule IR__Exp
The Smallfoot Intermediate Language: Expressions
NOTE: For doing substitutionson expressions, there are some functions in Sil
.
type closure
=
{
}
and sizeof_data
=
{
}
This records information about a sizeof(typ)
expression.
nbytes
represents the result of the evaluation of sizeof(typ)
if it is statically known.
If typ
is of the form Tarray elt (Some static_length)
, then dynamic_length
is the number of elements of type elt
in the array. The dynamic_length
, tracked by symbolic execution, may differ from the static_length
obtained from the type definition, e.g. when an array is over-allocated.
If typ
is a struct type, the dynamic_length
is that of the final extensible array, if any.
and t
=
Program expressions.
val equal : t -> t -> bool
Equality for expressions.
module Set : IStdlib.IStd .Caml.Set.S with type Set .elt = t
Set of expressions.
module Map : IStdlib.IStd .Caml.Map.S with type Map .key = t
Map with expression keys.
module Hash : IStdlib.IStd .Caml.Hashtbl.S with type Hash .key = t
Hashtable with expression keys.
val is_null_literal : t -> bool
val is_this : t -> bool
return true if exp
is the special this/self expression
val is_zero : t -> bool
val is_const : t -> bool
Utility Functions for Expressionsval texp_to_typ : IR.Typ.t option -> t -> IR.Typ.t
Turn an expression representing a type into the type it represents If not a sizeof, return the default type if given, otherwise raise an exception
val root_of_lexp : t -> t
Return the root of lexp
.
val get_undefined : bool -> t
Get an expression "undefined", the boolean indicates whether the undefined value goest into the footprint
val pointer_arith : t -> bool
Checks whether an expression denotes a location using pointer arithmetic. Currently, catches array - indexing expressions such as ai
only.
val has_local_addr : t -> bool
returns true if the expression operates on address of local variable
val zero : t
Integer constant 0
val null : t
Null constant
val one : t
Integer constant 1
val minus_one : t
Integer constant -1
val int : IR.IntLit.t -> t
Create integer constant
val float : float -> t
Create float constant
val bool : bool -> t
Create integer constant corresponding to the boolean value
val eq : t -> t -> t
Create expression e1 == e2
val ne : t -> t -> t
Create expression e1 != e2
val le : t -> t -> t
Create expression e1 <= e2
val lt : t -> t -> t
Create expression e1 < e2
val and_nary : t list -> t
Create expression e1 && e2 && e3 && ...
val free_vars : t -> IR.Ident.t IStdlib.IStd .Sequence.t
all the idents appearing in the expression
val gen_free_vars : t -> (unit, IR.Ident.t ) IStdlib.IStd .Sequence.Generator.t
val ident_mem : t -> IR.Ident.t -> bool
true if the identifier appears in the expression
val program_vars : t -> IR.Pvar.t IStdlib.IStd .Sequence.t
all the program variables appearing in the expression
val rename_pvars : f:(string -> string) -> t -> t
Rename all Pvars according to the function f
. WARNING: You want to rename pvars before you combine expressions from different symbolic states, which you RARELY want to.
val fold_captured : f:('a -> t -> 'a ) -> t -> 'a -> 'a
Fold over the expressions captured by this expression.
val pp_diff : ?print_types:bool -> IStdlib.Pp.env -> F .formatter -> t -> unit
val pp : F .formatter -> t -> unit
val pp_closure : F .formatter -> closure -> unit
val to_string : t -> string
val d_exp : t -> unit
dump an expression.
val pp_texp : IStdlib.Pp.env -> F .formatter -> t -> unit
Pretty print a type.
val pp_texp_full : IStdlib.Pp.env -> F .formatter -> t -> unit
Pretty print a type with all the details.
val d_texp_full : t -> unit
Dump a type expression with all the details.
val d_list : t list -> unit
Dump a list of expressions.
val is_objc_block_closure : t -> bool
val zero_of_type : IR.Typ.t -> t option
Returns the zero value of a type, for int, float and ptr types
val zero_of_type_exn : IR.Typ.t -> t
val ignore_cast : t -> t
val ignore_integer_cast : t -> t
val get_java_class_initializer : IR.Tenv.t -> t -> (IR.Procname.t * IR.Pvar.t * IR.Fieldname.t * IR.Typ.t ) option
Returns the class initializer of the given expression in Java
\ No newline at end of file
+IR__Exp (infer.IR__Exp) Up – infer » IR__ExpModule IR__Exp
The Smallfoot Intermediate Language: Expressions
NOTE: For doing substitutionson expressions, there are some functions in Sil
.
type closure
=
{
}
and sizeof_data
=
{
}
This records information about a sizeof(typ)
expression.
nbytes
represents the result of the evaluation of sizeof(typ)
if it is statically known.
If typ
is of the form Tarray elt (Some static_length)
, then dynamic_length
is the number of elements of type elt
in the array. The dynamic_length
, tracked by symbolic execution, may differ from the static_length
obtained from the type definition, e.g. when an array is over-allocated.
If typ
is a struct type, the dynamic_length
is that of the final extensible array, if any.
and t
=
Program expressions.
val equal : t -> t -> bool
Equality for expressions.
module Set : IStdlib.IStd .Caml.Set.S with type Set .elt = t
Set of expressions.
module Map : IStdlib.IStd .Caml.Map.S with type Map .key = t
Map with expression keys.
module Hash : IStdlib.IStd .Caml.Hashtbl.S with type Hash .key = t
Hashtable with expression keys.
val is_null_literal : t -> bool
val is_this : t -> bool
return true if exp
is the special this/self expression
val is_zero : t -> bool
val is_const : t -> bool
Utility Functions for Expressionsval texp_to_typ : IR.Typ.t option -> t -> IR.Typ.t
Turn an expression representing a type into the type it represents If not a sizeof, return the default type if given, otherwise raise an exception
val root_of_lexp : t -> t
Return the root of lexp
.
val get_undefined : bool -> t
Get an expression "undefined", the boolean indicates whether the undefined value goest into the footprint
val pointer_arith : t -> bool
Checks whether an expression denotes a location using pointer arithmetic. Currently, catches array - indexing expressions such as ai
only.
val has_local_addr : t -> bool
returns true if the expression operates on address of local variable
val zero : t
Integer constant 0
val null : t
Null constant
val one : t
Integer constant 1
val minus_one : t
Integer constant -1
val int : IR.IntLit.t -> t
Create integer constant
val float : float -> t
Create float constant
val bool : bool -> t
Create integer constant corresponding to the boolean value
val eq : t -> t -> t
Create expression e1 == e2
val ne : t -> t -> t
Create expression e1 != e2
val le : t -> t -> t
Create expression e1 <= e2
val lt : t -> t -> t
Create expression e1 < e2
val free_vars : t -> IR.Ident.t IStdlib.IStd .Sequence.t
all the idents appearing in the expression
val gen_free_vars : t -> (unit, IR.Ident.t ) IStdlib.IStd .Sequence.Generator.t
val ident_mem : t -> IR.Ident.t -> bool
true if the identifier appears in the expression
val program_vars : t -> IR.Pvar.t IStdlib.IStd .Sequence.t
all the program variables appearing in the expression
val fold_captured : f:('a -> t -> 'a ) -> t -> 'a -> 'a
Fold over the expressions captured by this expression.
val pp_diff : ?print_types:bool -> IStdlib.Pp.env -> F .formatter -> t -> unit
val pp : F .formatter -> t -> unit
val pp_closure : F .formatter -> closure -> unit
val to_string : t -> string
val d_exp : t -> unit
dump an expression.
val pp_texp : IStdlib.Pp.env -> F .formatter -> t -> unit
Pretty print a type.
val pp_texp_full : IStdlib.Pp.env -> F .formatter -> t -> unit
Pretty print a type with all the details.
val d_texp_full : t -> unit
Dump a type expression with all the details.
val d_list : t list -> unit
Dump a list of expressions.
val is_objc_block_closure : t -> bool
val zero_of_type : IR.Typ.t -> t option
Returns the zero value of a type, for int, float and ptr types
val zero_of_type_exn : IR.Typ.t -> t
val ignore_cast : t -> t
val ignore_integer_cast : t -> t
val get_java_class_initializer : IR.Tenv.t -> t -> (IR.Procname.t * IR.Pvar.t * IR.Fieldname.t * IR.Typ.t ) option
Returns the class initializer of the given expression in Java
\ No newline at end of file
diff --git a/website/static/odoc/next/infer/IR__Mangled/index.html b/website/static/odoc/next/infer/IR__Mangled/index.html
index 489d0505a..1cca99e33 100644
--- a/website/static/odoc/next/infer/IR__Mangled/index.html
+++ b/website/static/odoc/next/infer/IR__Mangled/index.html
@@ -1,2 +1,2 @@
-IR__Mangled (infer.IR__Mangled) Up – infer » IR__MangledModule IR__Mangled
type t
Type of mangled names
val compare : t -> t -> int
val yojson_of_t : t -> Ppx_yojson_conv_lib.Yojson.Safe.t
val equal : t -> t -> bool
Equality for mangled names
val from_string : string -> t
Convert a string to a mangled name
val mangled : string -> string -> t
Create a mangled name from a plain and mangled string
val to_string : t -> string
Convert a mangled name to a string
val to_string_full : t -> string
Convert a full mangled name to a string
val pp : Stdlib.Format.formatter -> t -> unit
Pretty print a mangled name
val this : t
val is_this : t -> bool
val self : t
val is_self : t -> bool
val rename : f:(string -> string) -> t -> t
Maps over both the plain and the mangled components.
module Set : IStdlib.PrettyPrintable.PPSet with type PPSet .elt = t
Set of Mangled.
module Map : IStdlib.PrettyPrintable.PPMap with type PPMap .key = t
Map with Mangled as key
\ No newline at end of file
+IR__Mangled (infer.IR__Mangled) Up – infer » IR__MangledModule IR__Mangled
type t
Type of mangled names
val compare : t -> t -> int
val yojson_of_t : t -> Ppx_yojson_conv_lib.Yojson.Safe.t
val equal : t -> t -> bool
Equality for mangled names
val from_string : string -> t
Convert a string to a mangled name
val mangled : string -> string -> t
Create a mangled name from a plain and mangled string
val to_string : t -> string
Convert a mangled name to a string
val to_string_full : t -> string
Convert a full mangled name to a string
val pp : Stdlib.Format.formatter -> t -> unit
Pretty print a mangled name
val this : t
val is_this : t -> bool
val self : t
val is_self : t -> bool
module Set : IStdlib.PrettyPrintable.PPSet with type PPSet .elt = t
Set of Mangled.
module Map : IStdlib.PrettyPrintable.PPMap with type PPMap .key = t
Map with Mangled as key
\ No newline at end of file
diff --git a/website/static/odoc/next/infer/IR__Procdesc/index.html b/website/static/odoc/next/infer/IR__Procdesc/index.html
index b55539d64..3ddc085b6 100644
--- a/website/static/odoc/next/infer/IR__Procdesc/index.html
+++ b/website/static/odoc/next/infer/IR__Procdesc/index.html
@@ -1,2 +1,2 @@
-IR__Procdesc (infer.IR__Procdesc) Up – infer » IR__ProcdescModule IR__Procdesc
module Node : sig ... end
node of the control flow graph
module IdMap : IStdlib.PrettyPrintable.PPMap with type PPMap .key = Node.id
Map with node id keys.
module NodeHash : IStdlib.IStd .Caml.Hashtbl.S with type NodeHash .key = Node.t
Hash table with nodes as keys.
module NodeMap : IStdlib.IStd .Caml.Map.S with type NodeMap .key = Node.t
Map over nodes.
module NodeSet : IStdlib.IStd .Caml.Set.S with type NodeSet .elt = Node.t
Set of nodes.
type t
proc description
val append_locals : t -> IR.ProcAttributes.var_data list -> unit
append a list of new local variables to the existing list of local variables
val compute_distance_to_exit_node : t -> unit
Compute the distance of each node to the exit node, if not computed already
val create_node : t -> IBase.Location.t -> Node.nodekind -> IR.Sil.instr list -> Node.t
Create a new cfg node with the given location, kind, list of instructions, and add it to the procdesc.
val create_node_from_not_reversed : t -> IBase.Location.t -> Node.nodekind -> IR.Instrs.not_reversed_t -> Node.t
val fold_instrs : t -> init:'accum -> f:('accum -> Node.t -> IR.Sil.instr -> 'accum ) -> 'accum
fold over all nodes and their instructions
val find_map_instrs : t -> f:(IR.Sil.instr -> 'a option ) -> 'a option
val from_proc_attributes : IR.ProcAttributes.t -> t
Use Cfg.create_proc_desc
if you are adding a proc desc to a cfg
val get_access : t -> IR.PredSymb.access
Return the visibility attribute
val get_attributes : t -> IR.ProcAttributes.t
Get the attributes of the procedure.
val set_attributes : t -> IR.ProcAttributes.t -> unit
val get_captured : t -> IR.CapturedVar.t list
Return name and type of block's captured variables
val get_exit_node : t -> Node.t
val get_formals : t -> (IR.Mangled.t * IR.Typ.t ) list
Return name and type of formal parameters
val get_pvar_formals : t -> (IR.Pvar.t * IR.Typ.t ) list
Return pvar and type of formal parameters
val get_loc : t -> IBase.Location.t
Return loc information for the procedure
val get_locals : t -> IR.ProcAttributes.var_data list
Return name and type and attributes of local variables
val get_nodes : t -> Node.t list
val get_proc_name : t -> IR.Procname.t
val get_ret_type : t -> IR.Typ.t
Return the return type of the procedure and type string
val has_added_return_param : t -> bool
val is_ret_type_pod : t -> bool
val get_ret_var : t -> IR.Pvar.t
val get_start_node : t -> Node.t
val get_static_callees : t -> IR.Procname.t list
get a list of unique static callees excluding self
val is_defined : t -> bool
Return true
iff the procedure is defined, and not just declared
val is_java_synchronized : t -> bool
Return true
if the procedure signature has the Java synchronized keyword
val is_objc_arc_on : t -> bool
Return true
iff the ObjC procedure is compiled with ARC
val iter_instrs : (Node.t -> IR.Sil.instr -> unit) -> t -> unit
iterate over all nodes and their instructions
val replace_instrs : t -> f:(Node.t -> IR.Sil.instr -> IR.Sil.instr ) -> bool
Map and replace the instructions to be executed. Returns true if at least one substitution occured.
val replace_instrs_using_context : t -> f:(Node.t -> 'a -> IR.Sil.instr -> IR.Sil.instr ) -> update_context:('a -> IR.Sil.instr -> 'a ) -> context_at_node:(Node.t -> 'a ) -> bool
Map and replace the instructions to be executed using a context that we built with previous instructions in the node. Returns true if at least one substitution occured.
val replace_instrs_by_using_context : t -> f:(Node.t -> 'a -> IR.Sil.instr -> IR.Sil.instr array ) -> update_context:('a -> IR.Sil.instr -> 'a ) -> context_at_node:(Node.t -> 'a ) -> bool
Like replace_instrs_using_context
, but slower, and each instruction may be replaced by 0, 1, or more instructions.
val replace_instrs_by : t -> f:(Node.t -> IR.Sil.instr -> IR.Sil.instr array ) -> bool
Like replace_instrs
, but slower, and each instruction may be replaced by 0, 1, or more instructions.
val iter_nodes : (Node.t -> unit) -> t -> unit
iterate over all the nodes of a procedure
val fold_nodes : t -> init:'accum -> f:('accum -> Node.t -> 'accum ) -> 'accum
fold over all the nodes of a procedure
val fold_slope_range : Node.t -> Node.t -> init:'accum -> f:('accum -> Node.t -> 'accum ) -> 'accum
fold between two nodes or until we reach a branching structure
val set_succs : Node.t -> normal:Node.t list option -> exn:Node.t list option -> unit
Set the successor nodes and exception nodes, if given, and update predecessor links
val node_set_succs : t -> Node.t -> normal:Node.t list -> exn:Node.t list -> unit
Set the successor nodes and exception nodes, and update predecessor links
val set_exit_node : t -> Node.t -> unit
Set the exit node of the procedure
val set_start_node : t -> Node.t -> unit
val get_wto : t -> Node.t IR.WeakTopologicalOrder.Partition.t
val is_loop_head : t -> Node.t -> bool
val pp_signature : Stdlib.Format.formatter -> t -> unit
val pp_local : Stdlib.Format.formatter -> IR.ProcAttributes.var_data -> unit
val is_specialized : t -> bool
val is_captured_pvar : t -> IR.Pvar.t -> bool
true if pvar is a captured variable of a cpp lambda or obcj block
val is_captured_var : t -> IR.Var.t -> bool
true if var is a captured variable of a cpp lambda or obcj block
val has_modify_in_block_attr : t -> IR.Pvar.t -> bool
val shallow_copy_code_from_pdesc : orig_pdesc:t -> dest_pdesc:t -> unit
module SQLite : IBase.SqliteUtils.Data with type t = t option
per-procedure CFGs are stored in the SQLite "procedures" table as NULL if the procedure has no CFG
val load : IR.Procname.t -> t option
\ No newline at end of file
+IR__Procdesc (infer.IR__Procdesc) Up – infer » IR__ProcdescModule IR__Procdesc
module Node : sig ... end
node of the control flow graph
module IdMap : IStdlib.PrettyPrintable.PPMap with type PPMap .key = Node.id
Map with node id keys.
module NodeHash : IStdlib.IStd .Caml.Hashtbl.S with type NodeHash .key = Node.t
Hash table with nodes as keys.
module NodeMap : IStdlib.IStd .Caml.Map.S with type NodeMap .key = Node.t
Map over nodes.
module NodeSet : IStdlib.IStd .Caml.Set.S with type NodeSet .elt = Node.t
Set of nodes.
type t
proc description
val append_locals : t -> IR.ProcAttributes.var_data list -> unit
append a list of new local variables to the existing list of local variables
val compute_distance_to_exit_node : t -> unit
Compute the distance of each node to the exit node, if not computed already
val create_node : t -> IBase.Location.t -> Node.nodekind -> IR.Sil.instr list -> Node.t
Create a new cfg node with the given location, kind, list of instructions, and add it to the procdesc.
val create_node_from_not_reversed : t -> IBase.Location.t -> Node.nodekind -> IR.Instrs.not_reversed_t -> Node.t
val fold_instrs : t -> init:'accum -> f:('accum -> Node.t -> IR.Sil.instr -> 'accum ) -> 'accum
fold over all nodes and their instructions
val find_map_instrs : t -> f:(IR.Sil.instr -> 'a option ) -> 'a option
val from_proc_attributes : IR.ProcAttributes.t -> t
Use Cfg.create_proc_desc
if you are adding a proc desc to a cfg
val get_access : t -> IR.PredSymb.access
Return the visibility attribute
val get_attributes : t -> IR.ProcAttributes.t
Get the attributes of the procedure.
val set_attributes : t -> IR.ProcAttributes.t -> unit
val get_captured : t -> IR.CapturedVar.t list
Return name and type of block's captured variables
val get_exit_node : t -> Node.t
val get_formals : t -> (IR.Mangled.t * IR.Typ.t ) list
Return name and type of formal parameters
val get_pvar_formals : t -> (IR.Pvar.t * IR.Typ.t ) list
Return pvar and type of formal parameters
val get_loc : t -> IBase.Location.t
Return loc information for the procedure
val get_locals : t -> IR.ProcAttributes.var_data list
Return name and type and attributes of local variables
val get_nodes : t -> Node.t list
val get_proc_name : t -> IR.Procname.t
val get_ret_type : t -> IR.Typ.t
Return the return type of the procedure and type string
val has_added_return_param : t -> bool
val is_ret_type_pod : t -> bool
val get_ret_var : t -> IR.Pvar.t
val get_start_node : t -> Node.t
val get_static_callees : t -> IR.Procname.t list
get a list of unique static callees excluding self
val is_defined : t -> bool
Return true
iff the procedure is defined, and not just declared
val is_java_synchronized : t -> bool
Return true
if the procedure signature has the Java synchronized keyword
val is_objc_arc_on : t -> bool
Return true
iff the ObjC procedure is compiled with ARC
val iter_instrs : (Node.t -> IR.Sil.instr -> unit) -> t -> unit
iterate over all nodes and their instructions
val replace_instrs : t -> f:(Node.t -> IR.Sil.instr -> IR.Sil.instr ) -> bool
Map and replace the instructions to be executed. Returns true if at least one substitution occured.
val replace_instrs_using_context : t -> f:(Node.t -> 'a -> IR.Sil.instr -> IR.Sil.instr ) -> update_context:('a -> IR.Sil.instr -> 'a ) -> context_at_node:(Node.t -> 'a ) -> bool
Map and replace the instructions to be executed using a context that we built with previous instructions in the node. Returns true if at least one substitution occured.
val replace_instrs_by_using_context : t -> f:(Node.t -> 'a -> IR.Sil.instr -> IR.Sil.instr array ) -> update_context:('a -> IR.Sil.instr -> 'a ) -> context_at_node:(Node.t -> 'a ) -> bool
Like replace_instrs_using_context
, but slower, and each instruction may be replaced by 0, 1, or more instructions.
val iter_nodes : (Node.t -> unit) -> t -> unit
iterate over all the nodes of a procedure
val fold_nodes : t -> init:'accum -> f:('accum -> Node.t -> 'accum ) -> 'accum
fold over all the nodes of a procedure
val fold_slope_range : Node.t -> Node.t -> init:'accum -> f:('accum -> Node.t -> 'accum ) -> 'accum
fold between two nodes or until we reach a branching structure
val set_succs : Node.t -> normal:Node.t list option -> exn:Node.t list option -> unit
Set the successor nodes and exception nodes, if given, and update predecessor links
val node_set_succs : t -> Node.t -> normal:Node.t list -> exn:Node.t list -> unit
Set the successor nodes and exception nodes, and update predecessor links
val set_exit_node : t -> Node.t -> unit
Set the exit node of the procedure
val set_start_node : t -> Node.t -> unit
val get_wto : t -> Node.t IR.WeakTopologicalOrder.Partition.t
val is_loop_head : t -> Node.t -> bool
val pp_signature : Stdlib.Format.formatter -> t -> unit
val pp_local : Stdlib.Format.formatter -> IR.ProcAttributes.var_data -> unit
val is_specialized : t -> bool
val is_captured_pvar : t -> IR.Pvar.t -> bool
true if pvar is a captured variable of a cpp lambda or obcj block
val is_captured_var : t -> IR.Var.t -> bool
true if var is a captured variable of a cpp lambda or obcj block
val has_modify_in_block_attr : t -> IR.Pvar.t -> bool
val shallow_copy_code_from_pdesc : orig_pdesc:t -> dest_pdesc:t -> unit
module SQLite : IBase.SqliteUtils.Data with type t = t option
per-procedure CFGs are stored in the SQLite "procedures" table as NULL if the procedure has no CFG
val load : IR.Procname.t -> t option
\ No newline at end of file
diff --git a/website/static/odoc/next/infer/IR__Pvar/index.html b/website/static/odoc/next/infer/IR__Pvar/index.html
index 88c26575b..938b6249d 100644
--- a/website/static/odoc/next/infer/IR__Pvar/index.html
+++ b/website/static/odoc/next/infer/IR__Pvar/index.html
@@ -1,2 +1,2 @@
-IR__Pvar (infer.IR__Pvar) Up – infer » IR__PvarModule IR__Pvar
Program variables.
type translation_unit
= IBase.SourceFile.t option
type t
Type for program variables. There are 4 kinds of variables:
local variables, used for local variables and formal parameters callee program variables, used to handle recursion (x | callee
is distinguished from x
) global variables seed variables, used to store the initial value of formal parameters val compare : t -> t -> int
val yojson_of_t : t -> Ppx_yojson_conv_lib.Yojson.Safe.t
val compare_modulo_this : t -> t -> int
Comparison considering all pvars named 'this'/'self' to be equal
val equal : t -> t -> bool
Equality for pvar's
val get_declaring_function : t -> IR.Procname.t option
if not a global, return function declaring var
val d : t -> unit
Dump a program variable.
val get_name : t -> IR.Mangled.t
Get the name component of a program variable.
val get_ret_pvar : IR.Procname.t -> t
get_ret_pvar proc_name
retuns the return pvar associated with the procedure name
val get_ret_param_pvar : IR.Procname.t -> t
get_ret_param_pvar proc_name
retuns the return_param pvar associated with the procedure name
val get_simplified_name : t -> string
Get a simplified version of the name component of a program variable.
val is_abduced : t -> bool
Check if the pvar is an abduced return var or param passed by ref
val is_callee : t -> bool
Check if the pvar is a callee var
val is_global : t -> bool
Check if the pvar is a global var or a static local var
val is_static_local : t -> bool
Check if the pvar is a static variable declared inside a function
val is_constant_array : t -> bool
Check if the pvar has a constant array type
val is_const : t -> bool
Check if the pvar has a const type
val is_local : t -> bool
Check if the pvar is a (non-static) local var
val is_seed : t -> bool
Check if the pvar is a seed var
val is_return : t -> bool
Check if the pvar is a return var
val is_this : t -> bool
Check if a pvar is the special "this" var
val is_self : t -> bool
Check if a pvar is the special "self" var
val is_frontend_tmp : t -> bool
return true if pvar
is a temporary variable generated by the frontend
val is_clang_tmp : t -> bool
return true if pvar
is a temporary variable generated by clang
val is_ssa_frontend_tmp : t -> bool
return true if pvar
is a temporary variable generated by the frontend and is only assigned once on a non-looping control-flow path
val is_cpp_temporary : t -> bool
return true if this pvar represents a C++ temporary object (see http://en.cppreference.com/w/cpp/language/lifetime)
val is_objc_static_local_of_proc_name : string -> t -> bool
Check if a pvar is a local static in objc
val is_block_pvar : t -> bool
Check if a pvar is a local pointing to a block in objc
val mk : IR.Mangled.t -> IR.Procname.t -> t
mk name proc_name
creates a program var with the given function name
val mk_abduced_ref_param : IR.Procname.t -> int -> IBase.Location.t -> t
create an abduced variable for a parameter passed by reference
val mk_abduced_ret : IR.Procname.t -> IBase.Location.t -> t
create an abduced return variable for a call to proc_name
at loc
val mk_callee : IR.Mangled.t -> IR.Procname.t -> t
mk_callee name proc_name
creates a program var for a callee function with the given function name
val mk_global : ?is_constexpr:bool -> ?is_ice:bool -> ?is_pod:bool -> ?is_static_local:bool -> ?is_static_global:bool -> ?is_constant_array:bool -> ?is_const:bool -> ?translation_unit:IBase.SourceFile.t -> IR.Mangled.t -> t
create a global variable with the given name
val mk_tmp : string -> IR.Procname.t -> t
create a fresh temporary variable local to procedure pname
. for use in the frontends only!
val pp : IStdlib.Pp.env -> F .formatter -> t -> unit
Pretty print a program variable.
val pp_value : F .formatter -> t -> unit
Pretty print a pvar which denotes a value, not an address
val pp_value_non_verbose : F .formatter -> t -> unit
Non-verbose version of pp_value
val pp_translation_unit : F .formatter -> translation_unit -> unit
val to_callee : IR.Procname.t -> t -> t
Turn an ordinary program variable into a callee program variable
val to_seed : t -> t
Turn a pvar into a seed pvar (which stores the initial value of a stack var)
val to_string : t -> string
Convert a pvar to string.
val get_translation_unit : t -> translation_unit
Get the translation unit corresponding to a global. Raises Invalid_arg if not a global.
val is_compile_constant : t -> bool
Is the variable's value a compile-time constant? Always (potentially incorrectly) returns false
for non-globals.
val is_ice : t -> bool
Is the variable's type an integral constant expression? Always (potentially incorrectly) returns false
for non-globals.
val is_pod : t -> bool
Is the variable's type a "Plain Old Data" type (C++)? Always (potentially incorrectly) returns true
for non-globals.
val get_initializer_pname : t -> IR.Procname.t option
Get the procname of the initializer function for the given global variable
val build_formal_from_pvar : t -> IR.Mangled.t
build_formal_from_pvar var
Return a name that is composed of the name of var (and the name of the procname in case of locals)
val materialized_cpp_temporary : string
val swap_proc_in_local_pvar : t -> IR.Procname.t -> t
val rename : f:(string -> string) -> t -> t
module Set : IStdlib.PrettyPrintable.PPSet with type PPSet .elt = t
Sets of pvars.
type capture_mode
=
val string_of_capture_mode : capture_mode -> string
\ No newline at end of file
+IR__Pvar (infer.IR__Pvar) Up – infer » IR__PvarModule IR__Pvar
Program variables.
type translation_unit
= IBase.SourceFile.t option
type t
Type for program variables. There are 4 kinds of variables:
local variables, used for local variables and formal parameters callee program variables, used to handle recursion (x | callee
is distinguished from x
) global variables seed variables, used to store the initial value of formal parameters val compare : t -> t -> int
val yojson_of_t : t -> Ppx_yojson_conv_lib.Yojson.Safe.t
val compare_modulo_this : t -> t -> int
Comparison considering all pvars named 'this'/'self' to be equal
val equal : t -> t -> bool
Equality for pvar's
val get_declaring_function : t -> IR.Procname.t option
if not a global, return function declaring var
val d : t -> unit
Dump a program variable.
val get_name : t -> IR.Mangled.t
Get the name component of a program variable.
val get_ret_pvar : IR.Procname.t -> t
get_ret_pvar proc_name
retuns the return pvar associated with the procedure name
val get_ret_param_pvar : IR.Procname.t -> t
get_ret_param_pvar proc_name
retuns the return_param pvar associated with the procedure name
val get_simplified_name : t -> string
Get a simplified version of the name component of a program variable.
val is_abduced : t -> bool
Check if the pvar is an abduced return var or param passed by ref
val is_callee : t -> bool
Check if the pvar is a callee var
val is_global : t -> bool
Check if the pvar is a global var or a static local var
val is_static_local : t -> bool
Check if the pvar is a static variable declared inside a function
val is_constant_array : t -> bool
Check if the pvar has a constant array type
val is_const : t -> bool
Check if the pvar has a const type
val is_local : t -> bool
Check if the pvar is a (non-static) local var
val is_seed : t -> bool
Check if the pvar is a seed var
val is_return : t -> bool
Check if the pvar is a return var
val is_this : t -> bool
Check if a pvar is the special "this" var
val is_self : t -> bool
Check if a pvar is the special "self" var
val is_frontend_tmp : t -> bool
return true if pvar
is a temporary variable generated by the frontend
val is_clang_tmp : t -> bool
return true if pvar
is a temporary variable generated by clang
val is_ssa_frontend_tmp : t -> bool
return true if pvar
is a temporary variable generated by the frontend and is only assigned once on a non-looping control-flow path
val is_cpp_temporary : t -> bool
return true if this pvar represents a C++ temporary object (see http://en.cppreference.com/w/cpp/language/lifetime)
val is_objc_static_local_of_proc_name : string -> t -> bool
Check if a pvar is a local static in objc
val is_block_pvar : t -> bool
Check if a pvar is a local pointing to a block in objc
val mk : IR.Mangled.t -> IR.Procname.t -> t
mk name proc_name
creates a program var with the given function name
val mk_abduced_ref_param : IR.Procname.t -> int -> IBase.Location.t -> t
create an abduced variable for a parameter passed by reference
val mk_abduced_ret : IR.Procname.t -> IBase.Location.t -> t
create an abduced return variable for a call to proc_name
at loc
val mk_callee : IR.Mangled.t -> IR.Procname.t -> t
mk_callee name proc_name
creates a program var for a callee function with the given function name
val mk_global : ?is_constexpr:bool -> ?is_ice:bool -> ?is_pod:bool -> ?is_static_local:bool -> ?is_static_global:bool -> ?is_constant_array:bool -> ?is_const:bool -> ?translation_unit:IBase.SourceFile.t -> IR.Mangled.t -> t
create a global variable with the given name
val mk_tmp : string -> IR.Procname.t -> t
create a fresh temporary variable local to procedure pname
. for use in the frontends only!
val pp : IStdlib.Pp.env -> F .formatter -> t -> unit
Pretty print a program variable.
val pp_value : F .formatter -> t -> unit
Pretty print a pvar which denotes a value, not an address
val pp_value_non_verbose : F .formatter -> t -> unit
Non-verbose version of pp_value
val pp_translation_unit : F .formatter -> translation_unit -> unit
val to_callee : IR.Procname.t -> t -> t
Turn an ordinary program variable into a callee program variable
val to_seed : t -> t
Turn a pvar into a seed pvar (which stores the initial value of a stack var)
val to_string : t -> string
Convert a pvar to string.
val get_translation_unit : t -> translation_unit
Get the translation unit corresponding to a global. Raises Invalid_arg if not a global.
val is_compile_constant : t -> bool
Is the variable's value a compile-time constant? Always (potentially incorrectly) returns false
for non-globals.
val is_ice : t -> bool
Is the variable's type an integral constant expression? Always (potentially incorrectly) returns false
for non-globals.
val is_pod : t -> bool
Is the variable's type a "Plain Old Data" type (C++)? Always (potentially incorrectly) returns true
for non-globals.
val get_initializer_pname : t -> IR.Procname.t option
Get the procname of the initializer function for the given global variable
val build_formal_from_pvar : t -> IR.Mangled.t
build_formal_from_pvar var
Return a name that is composed of the name of var (and the name of the procname in case of locals)
val materialized_cpp_temporary : string
val swap_proc_in_local_pvar : t -> IR.Procname.t -> t
module Set : IStdlib.PrettyPrintable.PPSet with type PPSet .elt = t
Sets of pvars.
type capture_mode
=
val string_of_capture_mode : capture_mode -> string
\ No newline at end of file
diff --git a/website/static/odoc/next/infer/Pulselib/PulseCItv/index.html b/website/static/odoc/next/infer/Pulselib/PulseCItv/index.html
index 960617d4a..0d2316fc1 100644
--- a/website/static/odoc/next/infer/Pulselib/PulseCItv/index.html
+++ b/website/static/odoc/next/infer/Pulselib/PulseCItv/index.html
@@ -1,2 +1,2 @@
-PulseCItv (infer.Pulselib.PulseCItv) type t
val compare : t -> t -> int
val equal : t -> t -> bool
val equal_to : IR.IntLit.t -> t
val is_equal_to_zero : t -> bool
val is_not_equal_to_zero : t -> bool
whether this is literally ≠0
val as_int : t -> int option
as_int v
returns Some x
if v
is known to be x
val pp : F .formatter -> t -> unit
type abduction_result
=
|
Unsatisfiable
the assertion is never true given the parameters
|
Satisfiable of t option * t option
the assertion is satisfiable and when it is true then the lhs and rhs can be optionally refined to the given new intervals
val abduce_binop_is_true : negated:bool -> IR.Binop.t -> t option -> t option -> abduction_result
given arith_lhs_opt bop arith_rhs_opt
and if not negated
, return either
Unsatisfiable
iff lhs bop rhs = ∅Satisfiable (abduced_lhs_opt,abduced_rhs_opt)
iff lhs bop rhs ≠ ∅, such that (taking lhs=true if lhs_opt is None
, same for rhs) abduced_lhs_opt=Some alhs
if (lhs bop rhs ≠ ∅ => alhs⇔lhs) (and similarly for rhs)If negated
then imagine a similar explanation replacing "= ∅" with "≠ ∅" and vice-versa.
val binop : IR.Binop.t -> t -> t -> t option
val unop : IR.Unop.t -> t -> t option
val zero_inf : t
val ge_to : IR.IntLit.t -> t
\ No newline at end of file
+PulseCItv (infer.Pulselib.PulseCItv) type t
val compare : t -> t -> int
val equal : t -> t -> bool
val equal_to : IR.IntLit.t -> t
val is_equal_to_zero : t -> bool
val is_not_equal_to_zero : t -> bool
whether this is literally ≠0
val pp : F .formatter -> t -> unit
type abduction_result
=
|
Unsatisfiable
the assertion is never true given the parameters
|
Satisfiable of t option * t option
the assertion is satisfiable and when it is true then the lhs and rhs can be optionally refined to the given new intervals
val abduce_binop_is_true : negated:bool -> IR.Binop.t -> t option -> t option -> abduction_result
given arith_lhs_opt bop arith_rhs_opt
and if not negated
, return either
Unsatisfiable
iff lhs bop rhs = ∅Satisfiable (abduced_lhs_opt,abduced_rhs_opt)
iff lhs bop rhs ≠ ∅, such that (taking lhs=true if lhs_opt is None
, same for rhs) abduced_lhs_opt=Some alhs
if (lhs bop rhs ≠ ∅ => alhs⇔lhs) (and similarly for rhs)If negated
then imagine a similar explanation replacing "= ∅" with "≠ ∅" and vice-versa.
val binop : IR.Binop.t -> t -> t -> t option
val unop : IR.Unop.t -> t -> t option
val zero_inf : t
val ge_to : IR.IntLit.t -> t
\ No newline at end of file
diff --git a/website/static/odoc/next/infer/Pulselib/PulseFormula/index.html b/website/static/odoc/next/infer/Pulselib/PulseFormula/index.html
index e2ed3825f..29b64a48b 100644
--- a/website/static/odoc/next/infer/Pulselib/PulseFormula/index.html
+++ b/website/static/odoc/next/infer/Pulselib/PulseFormula/index.html
@@ -1,2 +1,2 @@
-PulseFormula (infer.Pulselib.PulseFormula) type t
val compare : t -> t -> int
val equal : t -> t -> bool
val yojson_of_t : t -> Ppx_yojson_conv_lib.Yojson.Safe.t
val pp : F .formatter -> t -> unit
val pp_with_pp_var : (F .formatter -> Var.t -> unit) -> F .formatter -> t -> unit
only used for unit tests
type operand
=
\ No newline at end of file
+PulseFormula (infer.Pulselib.PulseFormula) type t
val compare : t -> t -> int
val equal : t -> t -> bool
val yojson_of_t : t -> Ppx_yojson_conv_lib.Yojson.Safe.t
val pp : F .formatter -> t -> unit
val pp_with_pp_var : (F .formatter -> Var.t -> unit) -> F .formatter -> t -> unit
only used for unit tests
type operand
=
\ No newline at end of file
diff --git a/website/static/odoc/next/infer/Pulselib/PulsePathCondition/index.html b/website/static/odoc/next/infer/Pulselib/PulsePathCondition/index.html
index d718ac6d6..eb921df14 100644
--- a/website/static/odoc/next/infer/Pulselib/PulsePathCondition/index.html
+++ b/website/static/odoc/next/infer/Pulselib/PulsePathCondition/index.html
@@ -1,2 +1,2 @@
-PulsePathCondition (infer.Pulselib.PulsePathCondition) Up – infer » Pulselib » PulsePathConditionModule Pulselib.PulsePathCondition
module ValueHistory = PulseValueHistory
type t
val compare : t -> t -> int
val equal : t -> t -> bool
val yojson_of_t : t -> Ppx_yojson_conv_lib.Yojson.Safe.t
val true_ : t
val false_ : t
val pp : F .formatter -> t -> unit
type new_eqs
= PulseFormula.new_eqs
val is_known_zero : t -> AbstractValue.t -> bool
is_known_zero phi t
returns true
if phi |- t = 0
, false
if we don't know for sure
val is_known_not_equal_zero : t -> AbstractValue.t -> bool
is_known_not_equal_zero phi t
returns true
if phi |- t != 0
, false
if we don't know for sure
val is_unsat_cheap : t -> bool
whether the state contains a contradiction, call this as often as you want
val is_unsat_expensive : IR.Tenv.t -> get_dynamic_type:(AbstractValue.t -> IR.Typ.t option ) -> t -> t * bool * new_eqs
whether the state contains a contradiction, only call this when you absolutely have to
val as_int : t -> AbstractValue.t -> int option
as_int phi t
returns an integer x such that phi |- t = x
, if known for sure; see also is_known_zero
val has_no_assumptions : t -> bool
whether the current path is independent of any calling context
val get_var_repr : t -> AbstractValue.t -> AbstractValue.t
get the canonical representative for the variable according to the equality relation
\ No newline at end of file
+PulsePathCondition (infer.Pulselib.PulsePathCondition) Up – infer » Pulselib » PulsePathConditionModule Pulselib.PulsePathCondition
module ValueHistory = PulseValueHistory
type t
val compare : t -> t -> int
val equal : t -> t -> bool
val yojson_of_t : t -> Ppx_yojson_conv_lib.Yojson.Safe.t
val true_ : t
val false_ : t
val pp : F .formatter -> t -> unit
type new_eqs
= PulseFormula.new_eqs
val is_known_zero : t -> AbstractValue.t -> bool
is_known_zero phi t
returns true
if phi |- t = 0
, false
if we don't know for sure
val is_known_not_equal_zero : t -> AbstractValue.t -> bool
is_known_not_equal_zero phi t
returns true
if phi |- t != 0
, false
if we don't know for sure
val is_unsat_cheap : t -> bool
whether the state contains a contradiction, call this as often as you want
val is_unsat_expensive : IR.Tenv.t -> get_dynamic_type:(AbstractValue.t -> IR.Typ.t option ) -> t -> t * bool * new_eqs
whether the state contains a contradiction, only call this when you absolutely have to
val has_no_assumptions : t -> bool
whether the current path is independent of any calling context
val get_var_repr : t -> AbstractValue.t -> AbstractValue.t
get the canonical representative for the variable according to the equality relation
\ No newline at end of file
diff --git a/website/static/odoc/next/infer/Pulselib/PulseToplShallow/index.html b/website/static/odoc/next/infer/Pulselib/PulseToplShallow/index.html
deleted file mode 100644
index 73ae9f2ab..000000000
--- a/website/static/odoc/next/infer/Pulselib/PulseToplShallow/index.html
+++ /dev/null
@@ -1,2 +0,0 @@
-
-PulseToplShallow (infer.Pulselib.PulseToplShallow) val analyze : PulseSummary.t TOPLlib.Topl.analysis_transformer
Run pulse with Topl instrumentation if active. Inserts calls to the Topl automaton. Mutates the arguments: it is the caller's responsibility to instrument procedures at most once.
\ No newline at end of file
diff --git a/website/static/odoc/next/infer/Pulselib/index.html b/website/static/odoc/next/infer/Pulselib/index.html
index 45ace60da..ae27d03ca 100644
--- a/website/static/odoc/next/infer/Pulselib/index.html
+++ b/website/static/odoc/next/infer/Pulselib/index.html
@@ -1,2 +1,2 @@
-Pulselib (infer.Pulselib) Up – infer » PulselibModule Pulselib
module Pulse : sig ... end
module PulseAbductiveDomain : sig ... end
module PulseAbstractValue : sig ... end
module PulseAccessResult : sig ... end
module PulseArithmetic : sig ... end
module PulseAttribute : sig ... end
module PulseBaseAddressAttributes : sig ... end
module PulseBaseDomain : sig ... end
module PulseBaseMemory : sig ... end
module PulseBaseStack : sig ... end
module PulseBasicInterface : sig ... end
module PulseCItv : sig ... end
module PulseCallEvent : sig ... end
module PulseCallOperations : sig ... end
module PulseDiagnostic : sig ... end
module PulseDomainInterface : sig ... end
module PulseExecutionDomain : sig ... end
module PulseFormula : sig ... end
module PulseInterproc : sig ... end
module PulseInvalidation : sig ... end
module PulseLatentIssue : sig ... end
module PulseModels : sig ... end
module PulseObjectiveCSummary : sig ... end
module PulseOperations : sig ... end
module PulsePathCondition : sig ... end
module PulseReport : sig ... end
module PulseSatUnsat : sig ... end
module PulseSkippedCalls : sig ... end
module PulseSummary : sig ... end
module PulseTopl : sig ... end
module PulseToplShallow : sig ... end
module PulseTrace : sig ... end
module PulseUninitBlocklist : sig ... end
module PulseValueHistory : sig ... end
\ No newline at end of file
+Pulselib (infer.Pulselib) Up – infer » PulselibModule Pulselib
module Pulse : sig ... end
module PulseAbductiveDomain : sig ... end
module PulseAbstractValue : sig ... end
module PulseAccessResult : sig ... end
module PulseArithmetic : sig ... end
module PulseAttribute : sig ... end
module PulseBaseAddressAttributes : sig ... end
module PulseBaseDomain : sig ... end
module PulseBaseMemory : sig ... end
module PulseBaseStack : sig ... end
module PulseBasicInterface : sig ... end
module PulseCItv : sig ... end
module PulseCallEvent : sig ... end
module PulseCallOperations : sig ... end
module PulseDiagnostic : sig ... end
module PulseDomainInterface : sig ... end
module PulseExecutionDomain : sig ... end
module PulseFormula : sig ... end
module PulseInterproc : sig ... end
module PulseInvalidation : sig ... end
module PulseLatentIssue : sig ... end
module PulseModels : sig ... end
module PulseObjectiveCSummary : sig ... end
module PulseOperations : sig ... end
module PulsePathCondition : sig ... end
module PulseReport : sig ... end
module PulseSatUnsat : sig ... end
module PulseSkippedCalls : sig ... end
module PulseSummary : sig ... end
module PulseTopl : sig ... end
module PulseTrace : sig ... end
module PulseUninitBlocklist : sig ... end
module PulseValueHistory : sig ... end
\ No newline at end of file
diff --git a/website/static/odoc/next/infer/Pulselib__PulseCItv/index.html b/website/static/odoc/next/infer/Pulselib__PulseCItv/index.html
index a8f0c4d3e..dad45a791 100644
--- a/website/static/odoc/next/infer/Pulselib__PulseCItv/index.html
+++ b/website/static/odoc/next/infer/Pulselib__PulseCItv/index.html
@@ -1,2 +1,2 @@
-Pulselib__PulseCItv (infer.Pulselib__PulseCItv) Up – infer » Pulselib__PulseCItvModule Pulselib__PulseCItv
type t
val compare : t -> t -> int
val equal : t -> t -> bool
val equal_to : IR.IntLit.t -> t
val is_equal_to_zero : t -> bool
val is_not_equal_to_zero : t -> bool
whether this is literally ≠0
val as_int : t -> int option
as_int v
returns Some x
if v
is known to be x
val pp : F .formatter -> t -> unit
type abduction_result
=
|
Unsatisfiable
the assertion is never true given the parameters
|
Satisfiable of t option * t option
the assertion is satisfiable and when it is true then the lhs and rhs can be optionally refined to the given new intervals
val abduce_binop_is_true : negated:bool -> IR.Binop.t -> t option -> t option -> abduction_result
given arith_lhs_opt bop arith_rhs_opt
and if not negated
, return either
Unsatisfiable
iff lhs bop rhs = ∅Satisfiable (abduced_lhs_opt,abduced_rhs_opt)
iff lhs bop rhs ≠ ∅, such that (taking lhs=true if lhs_opt is None
, same for rhs) abduced_lhs_opt=Some alhs
if (lhs bop rhs ≠ ∅ => alhs⇔lhs) (and similarly for rhs)If negated
then imagine a similar explanation replacing "= ∅" with "≠ ∅" and vice-versa.
val binop : IR.Binop.t -> t -> t -> t option
val unop : IR.Unop.t -> t -> t option
val zero_inf : t
val ge_to : IR.IntLit.t -> t
\ No newline at end of file
+Pulselib__PulseCItv (infer.Pulselib__PulseCItv) Up – infer » Pulselib__PulseCItvModule Pulselib__PulseCItv
type t
val compare : t -> t -> int
val equal : t -> t -> bool
val equal_to : IR.IntLit.t -> t
val is_equal_to_zero : t -> bool
val is_not_equal_to_zero : t -> bool
whether this is literally ≠0
val pp : F .formatter -> t -> unit
type abduction_result
=
|
Unsatisfiable
the assertion is never true given the parameters
|
Satisfiable of t option * t option
the assertion is satisfiable and when it is true then the lhs and rhs can be optionally refined to the given new intervals
val abduce_binop_is_true : negated:bool -> IR.Binop.t -> t option -> t option -> abduction_result
given arith_lhs_opt bop arith_rhs_opt
and if not negated
, return either
Unsatisfiable
iff lhs bop rhs = ∅Satisfiable (abduced_lhs_opt,abduced_rhs_opt)
iff lhs bop rhs ≠ ∅, such that (taking lhs=true if lhs_opt is None
, same for rhs) abduced_lhs_opt=Some alhs
if (lhs bop rhs ≠ ∅ => alhs⇔lhs) (and similarly for rhs)If negated
then imagine a similar explanation replacing "= ∅" with "≠ ∅" and vice-versa.
val binop : IR.Binop.t -> t -> t -> t option
val unop : IR.Unop.t -> t -> t option
val zero_inf : t
val ge_to : IR.IntLit.t -> t
\ No newline at end of file
diff --git a/website/static/odoc/next/infer/Pulselib__PulseFormula/index.html b/website/static/odoc/next/infer/Pulselib__PulseFormula/index.html
index b4d1c11a6..3402a1837 100644
--- a/website/static/odoc/next/infer/Pulselib__PulseFormula/index.html
+++ b/website/static/odoc/next/infer/Pulselib__PulseFormula/index.html
@@ -1,2 +1,2 @@
-Pulselib__PulseFormula (infer.Pulselib__PulseFormula) Up – infer » Pulselib__PulseFormulaModule Pulselib__PulseFormula
type t
val compare : t -> t -> int
val equal : t -> t -> bool
val yojson_of_t : t -> Ppx_yojson_conv_lib.Yojson.Safe.t
val pp : F .formatter -> t -> unit
val pp_with_pp_var : (F .formatter -> Var.t -> unit) -> F .formatter -> t -> unit
only used for unit tests
type operand
=
\ No newline at end of file
+Pulselib__PulseFormula (infer.Pulselib__PulseFormula) Up – infer » Pulselib__PulseFormulaModule Pulselib__PulseFormula
type t
val compare : t -> t -> int
val equal : t -> t -> bool
val yojson_of_t : t -> Ppx_yojson_conv_lib.Yojson.Safe.t
val pp : F .formatter -> t -> unit
val pp_with_pp_var : (F .formatter -> Var.t -> unit) -> F .formatter -> t -> unit
only used for unit tests
type operand
=
\ No newline at end of file
diff --git a/website/static/odoc/next/infer/Pulselib__PulsePathCondition/index.html b/website/static/odoc/next/infer/Pulselib__PulsePathCondition/index.html
index d2bd0fc97..d6e3f3725 100644
--- a/website/static/odoc/next/infer/Pulselib__PulsePathCondition/index.html
+++ b/website/static/odoc/next/infer/Pulselib__PulsePathCondition/index.html
@@ -1,2 +1,2 @@
-Pulselib__PulsePathCondition (infer.Pulselib__PulsePathCondition) Up – infer » Pulselib__PulsePathConditionModule Pulselib__PulsePathCondition
type t
val compare : t -> t -> int
val equal : t -> t -> bool
val yojson_of_t : t -> Ppx_yojson_conv_lib.Yojson.Safe.t
val true_ : t
val false_ : t
val pp : F .formatter -> t -> unit
type new_eqs
= Pulselib.PulseFormula.new_eqs
val is_known_zero : t -> AbstractValue.t -> bool
is_known_zero phi t
returns true
if phi |- t = 0
, false
if we don't know for sure
val is_known_not_equal_zero : t -> AbstractValue.t -> bool
is_known_not_equal_zero phi t
returns true
if phi |- t != 0
, false
if we don't know for sure
val is_unsat_cheap : t -> bool
whether the state contains a contradiction, call this as often as you want
val is_unsat_expensive : IR.Tenv.t -> get_dynamic_type:(AbstractValue.t -> IR.Typ.t option ) -> t -> t * bool * new_eqs
whether the state contains a contradiction, only call this when you absolutely have to
val as_int : t -> AbstractValue.t -> int option
as_int phi t
returns an integer x such that phi |- t = x
, if known for sure; see also is_known_zero
val has_no_assumptions : t -> bool
whether the current path is independent of any calling context
val get_var_repr : t -> AbstractValue.t -> AbstractValue.t
get the canonical representative for the variable according to the equality relation
\ No newline at end of file
+Pulselib__PulsePathCondition (infer.Pulselib__PulsePathCondition) Up – infer » Pulselib__PulsePathConditionModule Pulselib__PulsePathCondition
type t
val compare : t -> t -> int
val equal : t -> t -> bool
val yojson_of_t : t -> Ppx_yojson_conv_lib.Yojson.Safe.t
val true_ : t
val false_ : t
val pp : F .formatter -> t -> unit
type new_eqs
= Pulselib.PulseFormula.new_eqs
val is_known_zero : t -> AbstractValue.t -> bool
is_known_zero phi t
returns true
if phi |- t = 0
, false
if we don't know for sure
val is_known_not_equal_zero : t -> AbstractValue.t -> bool
is_known_not_equal_zero phi t
returns true
if phi |- t != 0
, false
if we don't know for sure
val is_unsat_cheap : t -> bool
whether the state contains a contradiction, call this as often as you want
val is_unsat_expensive : IR.Tenv.t -> get_dynamic_type:(AbstractValue.t -> IR.Typ.t option ) -> t -> t * bool * new_eqs
whether the state contains a contradiction, only call this when you absolutely have to
val has_no_assumptions : t -> bool
whether the current path is independent of any calling context
val get_var_repr : t -> AbstractValue.t -> AbstractValue.t
get the canonical representative for the variable according to the equality relation
\ No newline at end of file
diff --git a/website/static/odoc/next/infer/Pulselib__PulseToplShallow/.dune-keep b/website/static/odoc/next/infer/Pulselib__PulseToplShallow/.dune-keep
deleted file mode 100644
index e69de29bb..000000000
diff --git a/website/static/odoc/next/infer/Pulselib__PulseToplShallow/index.html b/website/static/odoc/next/infer/Pulselib__PulseToplShallow/index.html
deleted file mode 100644
index a0ce4f22d..000000000
--- a/website/static/odoc/next/infer/Pulselib__PulseToplShallow/index.html
+++ /dev/null
@@ -1,2 +0,0 @@
-
-Pulselib__PulseToplShallow (infer.Pulselib__PulseToplShallow) Up – infer » Pulselib__PulseToplShallowModule Pulselib__PulseToplShallow
val analyze : Pulselib.PulseSummary.t TOPLlib.Topl.analysis_transformer
Run pulse with Topl instrumentation if active. Inserts calls to the Topl automaton. Mutates the arguments: it is the caller's responsibility to instrument procedures at most once.
\ No newline at end of file
diff --git a/website/static/odoc/next/infer/TOPLlib/Topl/index.html b/website/static/odoc/next/infer/TOPLlib/Topl/index.html
index 1135a0f16..5bcf21866 100644
--- a/website/static/odoc/next/infer/TOPLlib/Topl/index.html
+++ b/website/static/odoc/next/infer/TOPLlib/Topl/index.html
@@ -1,2 +1,2 @@
-Topl (infer.TOPLlib.Topl) val automaton : unit -> ToplAutomaton.t
Return the automaton representing all Topl properties.
val is_shallow_active : unit -> bool
Return whether the Topl based on Sil instrumentation is active.
val is_deep_active : unit -> bool
Return whether PulseTopl is active.
val get_proc_attr : IR.Procname.t -> IR.ProcAttributes.t option
get_proc_attr proc_name
returns the attributes of get_proc_desc proc_name
val get_proc_desc : IR.Procname.t -> IR.Procdesc.t option
Return a synthesized Procdesc.t, when it corresponds to instrumentation for a TOPL property.
val sourcefile : unit -> IBase.SourceFile.t
The (fake) sourcefile in which synthesized code resides. This function has a side-effect, because that's how SourceFile
works, so do NOT call when Topl is inactive.
val cfg : unit -> IR.Cfg.t
The CFG of the synthesized code. This function has a side-effect, because that's how Cfg
works, so do NOT call when Topl is inactive.
type 'summary analysis
= 'summary Absint.InterproceduralAnalysis.t -> 'summary option
type 'summary postprocess
= 'summary Absint.InterproceduralAnalysis.t -> 'summary -> unit
type 'summary analysis_transformer
= 'summary analysis -> 'summary analysis
val analyze_with : 'summary postprocess -> 'summary analysis_transformer
analyze_with analyze postprocess analysis_data
calls analyze
and then postprocess
on analysis_data
val analyze_with_biabduction : Biabduction.BiabductionSummary.t analysis_transformer
Run biabduction with Topl instrumentation if active. Inserts calls to the TOPL automaton. Mutates the arguments: it is the caller's responsibility to instrument procedures at most once.
\ No newline at end of file
+Topl (infer.TOPLlib.Topl) val automaton : unit -> ToplAutomaton.t
Return the automaton representing all Topl properties.
val is_active : unit -> bool
Return whether PulseTopl is active.
\ No newline at end of file
diff --git a/website/static/odoc/next/infer/TOPLlib/ToplAutomaton/index.html b/website/static/odoc/next/infer/TOPLlib/ToplAutomaton/index.html
index ddb9d1ca0..03d7de994 100644
--- a/website/static/odoc/next/infer/TOPLlib/ToplAutomaton/index.html
+++ b/website/static/odoc/next/infer/TOPLlib/ToplAutomaton/index.html
@@ -1,2 +1,2 @@
-ToplAutomaton (infer.TOPLlib.ToplAutomaton) type t
type vindex
= int
from 0 to vcount()-1, inclusive
type tindex
= int
from 0 to tcount()-1, inclusive
type transition
=
{
}
val make : ToplAst.t list -> t
val outgoing : t -> vindex -> tindex list
val is_nondet : t -> vindex -> bool
val vcount : t -> int
val transition : t -> tindex -> transition
val tfilter_map : t -> f:(transition -> 'a option ) -> 'a list
val is_skip : t -> tindex -> bool
A transition is *skip* when it has no action, its guard is implied by all other guards, and its target equals its source. is_skip automaton t
returns true when it can prove that t
is skip.
val tcount : t -> int
val max_args : t -> int
val get_start_error_pairs : t -> (vindex * vindex ) list
Return pairs (i,j)
of vertex indices corresponding to pairs ((p, "start"), (p, "error"))
of vertex names, where p
ranges over property names. POST: no vertex index occurs more than once in the result.
val registers : t -> ToplAst.register_name list
val pp_message_of_state : Stdlib.Format.formatter -> (t * tindex ) -> unit
Print "property P reaches state E".
val is_start : t -> vindex -> bool
val is_error : t -> vindex -> bool
val pp_transition : Stdlib.Format.formatter -> transition -> unit
\ No newline at end of file
+ToplAutomaton (infer.TOPLlib.ToplAutomaton) type t
type vindex
= int
from 0 to vcount()-1, inclusive
type tindex
= int
from 0 to tcount()-1, inclusive
type transition
=
{
}
val make : ToplAst.t list -> t
val vcount : t -> int
val tfilter_map : t -> f:(transition -> 'a option ) -> 'a list
val registers : t -> ToplAst.register_name list
val pp_message_of_state : Stdlib.Format.formatter -> (t * tindex ) -> unit
Print "property P reaches state E".
val is_start : t -> vindex -> bool
val is_error : t -> vindex -> bool
val pp_transition : Stdlib.Format.formatter -> transition -> unit
\ No newline at end of file
diff --git a/website/static/odoc/next/infer/TOPLlib/ToplMonitor/index.html b/website/static/odoc/next/infer/TOPLlib/ToplMonitor/index.html
deleted file mode 100644
index e938cf5e5..000000000
--- a/website/static/odoc/next/infer/TOPLlib/ToplMonitor/index.html
+++ /dev/null
@@ -1,2 +0,0 @@
-
-ToplMonitor (infer.TOPLlib.ToplMonitor) val generate : ToplAutomaton.t -> IR.Procname.t -> IR.Procdesc.t option
generate automaton proc_name
returns a CFG, provided that proc_name
is a recognized procedure name
val sourcefile : unit -> IBase.SourceFile.t
For debug.
val cfg : unit -> IR.Cfg.t
For debug. This datastructure accumulates all the procedures that were synthesized by the current process. If the implementation is correct, then different processes synthesize the same procedures, given the same set of Topl properties. However, for debug, we print the datastructure in a filename that contains the PID, which is why sourcefile
is exposed.
\ No newline at end of file
diff --git a/website/static/odoc/next/infer/TOPLlib/ToplName/index.html b/website/static/odoc/next/infer/TOPLlib/ToplName/index.html
deleted file mode 100644
index 6680490c2..000000000
--- a/website/static/odoc/next/infer/TOPLlib/ToplName/index.html
+++ /dev/null
@@ -1,2 +0,0 @@
-
-ToplName (infer.TOPLlib.ToplName) type t
= string
val topl_property : t
val transition : int -> t
val arg : int -> t
val saved_arg : int -> t
val reg : string -> t
val state : t
val maybe : t
val execute : t
val execute_state : int -> t
val save_args : t
\ No newline at end of file
diff --git a/website/static/odoc/next/infer/TOPLlib/ToplUtils/index.html b/website/static/odoc/next/infer/TOPLlib/ToplUtils/index.html
deleted file mode 100644
index 7569ca667..000000000
--- a/website/static/odoc/next/infer/TOPLlib/ToplUtils/index.html
+++ /dev/null
@@ -1,2 +0,0 @@
-
-ToplUtils (infer.TOPLlib.ToplUtils) val any_type : IR.Typ.t
For now, Topl is untyped. The "any" type is simulated with "java.lang.Object".
val topl_class_name : IR.Typ.Name.t
val topl_class_typ : IR.Typ.t
val topl_class_pvar : IR.Pvar.t
val static_var : string -> IR.Exp.t
val local_var : IR.Procname.t -> string -> IR.Exp.t
val constant_int : int -> IR.Exp.t
val topl_call : IR.Ident.t -> IR.Typ.desc -> IBase.Location.t -> string -> (IR.Exp.t * IR.Typ.t ) list -> IR.Sil.instr
Call a TOPL function; that is, a static member of "topl.Property" with java.lang.Object arguments and return ret_id
of type ret_typ
.
val is_synthesized : IR.Procname.t -> bool
val debug : ('a , Stdlib.Format.formatter, unit) IStdlib.IStd .format -> 'a
val make_field : string -> IR.Fieldname.t
val binop_to : ToplAst.binop -> IR.Binop.t
\ No newline at end of file
diff --git a/website/static/odoc/next/infer/TOPLlib/index.html b/website/static/odoc/next/infer/TOPLlib/index.html
index 899fbc577..0a7c49a9c 100644
--- a/website/static/odoc/next/infer/TOPLlib/index.html
+++ b/website/static/odoc/next/infer/TOPLlib/index.html
@@ -1,2 +1,2 @@
-TOPLlib (infer.TOPLlib) module Topl : sig ... end
module ToplAst : sig ... end
module ToplAstOps : sig ... end
module ToplAutomaton : sig ... end
module ToplLexer : sig ... end
module ToplMonitor : sig ... end
module ToplName : sig ... end
module ToplParser : sig ... end
module ToplUtils : sig ... end
\ No newline at end of file
+TOPLlib (infer.TOPLlib) module Topl : sig ... end
module ToplAst : sig ... end
module ToplAstOps : sig ... end
module ToplAutomaton : sig ... end
module ToplLexer : sig ... end
module ToplParser : sig ... end
\ No newline at end of file
diff --git a/website/static/odoc/next/infer/TOPLlib__Topl/index.html b/website/static/odoc/next/infer/TOPLlib__Topl/index.html
index ec6eee2ed..da4a841e1 100644
--- a/website/static/odoc/next/infer/TOPLlib__Topl/index.html
+++ b/website/static/odoc/next/infer/TOPLlib__Topl/index.html
@@ -1,2 +1,2 @@
-TOPLlib__Topl (infer.TOPLlib__Topl) Up – infer » TOPLlib__ToplModule TOPLlib__Topl
val automaton : unit -> TOPLlib.ToplAutomaton.t
Return the automaton representing all Topl properties.
val is_shallow_active : unit -> bool
Return whether the Topl based on Sil instrumentation is active.
val is_deep_active : unit -> bool
Return whether PulseTopl is active.
val get_proc_attr : IR.Procname.t -> IR.ProcAttributes.t option
get_proc_attr proc_name
returns the attributes of get_proc_desc proc_name
val get_proc_desc : IR.Procname.t -> IR.Procdesc.t option
Return a synthesized Procdesc.t, when it corresponds to instrumentation for a TOPL property.
val sourcefile : unit -> IBase.SourceFile.t
The (fake) sourcefile in which synthesized code resides. This function has a side-effect, because that's how SourceFile
works, so do NOT call when Topl is inactive.
val cfg : unit -> IR.Cfg.t
The CFG of the synthesized code. This function has a side-effect, because that's how Cfg
works, so do NOT call when Topl is inactive.
type 'summary analysis
= 'summary Absint.InterproceduralAnalysis.t -> 'summary option
type 'summary postprocess
= 'summary Absint.InterproceduralAnalysis.t -> 'summary -> unit
type 'summary analysis_transformer
= 'summary analysis -> 'summary analysis
val analyze_with : 'summary postprocess -> 'summary analysis_transformer
analyze_with analyze postprocess analysis_data
calls analyze
and then postprocess
on analysis_data
val analyze_with_biabduction : Biabduction.BiabductionSummary.t analysis_transformer
Run biabduction with Topl instrumentation if active. Inserts calls to the TOPL automaton. Mutates the arguments: it is the caller's responsibility to instrument procedures at most once.
\ No newline at end of file
+TOPLlib__Topl (infer.TOPLlib__Topl) Up – infer » TOPLlib__ToplModule TOPLlib__Topl
val automaton : unit -> TOPLlib.ToplAutomaton.t
Return the automaton representing all Topl properties.
val is_active : unit -> bool
Return whether PulseTopl is active.
\ No newline at end of file
diff --git a/website/static/odoc/next/infer/TOPLlib__ToplAutomaton/index.html b/website/static/odoc/next/infer/TOPLlib__ToplAutomaton/index.html
index cb698c6b9..1f02add1b 100644
--- a/website/static/odoc/next/infer/TOPLlib__ToplAutomaton/index.html
+++ b/website/static/odoc/next/infer/TOPLlib__ToplAutomaton/index.html
@@ -1,2 +1,2 @@
-TOPLlib__ToplAutomaton (infer.TOPLlib__ToplAutomaton) Up – infer » TOPLlib__ToplAutomatonModule TOPLlib__ToplAutomaton
type t
type vindex
= int
from 0 to vcount()-1, inclusive
type tindex
= int
from 0 to tcount()-1, inclusive
type transition
=
{
}
val make : TOPLlib.ToplAst.t list -> t
val outgoing : t -> vindex -> tindex list
val is_nondet : t -> vindex -> bool
val vcount : t -> int
val transition : t -> tindex -> transition
val tfilter_map : t -> f:(transition -> 'a option ) -> 'a list
val is_skip : t -> tindex -> bool
A transition is *skip* when it has no action, its guard is implied by all other guards, and its target equals its source. is_skip automaton t
returns true when it can prove that t
is skip.
val tcount : t -> int
val max_args : t -> int
val get_start_error_pairs : t -> (vindex * vindex ) list
Return pairs (i,j)
of vertex indices corresponding to pairs ((p, "start"), (p, "error"))
of vertex names, where p
ranges over property names. POST: no vertex index occurs more than once in the result.
val registers : t -> TOPLlib.ToplAst.register_name list
val pp_message_of_state : Stdlib.Format.formatter -> (t * tindex ) -> unit
Print "property P reaches state E".
val is_start : t -> vindex -> bool
val is_error : t -> vindex -> bool
val pp_transition : Stdlib.Format.formatter -> transition -> unit
\ No newline at end of file
+TOPLlib__ToplAutomaton (infer.TOPLlib__ToplAutomaton) Up – infer » TOPLlib__ToplAutomatonModule TOPLlib__ToplAutomaton
type t
type vindex
= int
from 0 to vcount()-1, inclusive
type tindex
= int
from 0 to tcount()-1, inclusive
type transition
=
{
}
val make : TOPLlib.ToplAst.t list -> t
val vcount : t -> int
val tfilter_map : t -> f:(transition -> 'a option ) -> 'a list
val registers : t -> TOPLlib.ToplAst.register_name list
val pp_message_of_state : Stdlib.Format.formatter -> (t * tindex ) -> unit
Print "property P reaches state E".
val is_start : t -> vindex -> bool
val is_error : t -> vindex -> bool
val pp_transition : Stdlib.Format.formatter -> transition -> unit
\ No newline at end of file
diff --git a/website/static/odoc/next/infer/TOPLlib__ToplMonitor/.dune-keep b/website/static/odoc/next/infer/TOPLlib__ToplMonitor/.dune-keep
deleted file mode 100644
index e69de29bb..000000000
diff --git a/website/static/odoc/next/infer/TOPLlib__ToplMonitor/index.html b/website/static/odoc/next/infer/TOPLlib__ToplMonitor/index.html
deleted file mode 100644
index 028444ceb..000000000
--- a/website/static/odoc/next/infer/TOPLlib__ToplMonitor/index.html
+++ /dev/null
@@ -1,2 +0,0 @@
-
-TOPLlib__ToplMonitor (infer.TOPLlib__ToplMonitor) Up – infer » TOPLlib__ToplMonitorModule TOPLlib__ToplMonitor
val generate : TOPLlib.ToplAutomaton.t -> IR.Procname.t -> IR.Procdesc.t option
generate automaton proc_name
returns a CFG, provided that proc_name
is a recognized procedure name
val sourcefile : unit -> IBase.SourceFile.t
For debug.
val cfg : unit -> IR.Cfg.t
For debug. This datastructure accumulates all the procedures that were synthesized by the current process. If the implementation is correct, then different processes synthesize the same procedures, given the same set of Topl properties. However, for debug, we print the datastructure in a filename that contains the PID, which is why sourcefile
is exposed.
\ No newline at end of file
diff --git a/website/static/odoc/next/infer/TOPLlib__ToplName/.dune-keep b/website/static/odoc/next/infer/TOPLlib__ToplName/.dune-keep
deleted file mode 100644
index e69de29bb..000000000
diff --git a/website/static/odoc/next/infer/TOPLlib__ToplName/index.html b/website/static/odoc/next/infer/TOPLlib__ToplName/index.html
deleted file mode 100644
index 39fd7ea9b..000000000
--- a/website/static/odoc/next/infer/TOPLlib__ToplName/index.html
+++ /dev/null
@@ -1,2 +0,0 @@
-
-TOPLlib__ToplName (infer.TOPLlib__ToplName) Up – infer » TOPLlib__ToplNameModule TOPLlib__ToplName
type t
= string
val topl_property : t
val transition : int -> t
val arg : int -> t
val saved_arg : int -> t
val reg : string -> t
val state : t
val maybe : t
val execute : t
val execute_state : int -> t
val save_args : t
\ No newline at end of file
diff --git a/website/static/odoc/next/infer/TOPLlib__ToplUtils/.dune-keep b/website/static/odoc/next/infer/TOPLlib__ToplUtils/.dune-keep
deleted file mode 100644
index e69de29bb..000000000
diff --git a/website/static/odoc/next/infer/TOPLlib__ToplUtils/index.html b/website/static/odoc/next/infer/TOPLlib__ToplUtils/index.html
deleted file mode 100644
index 38f3c81b9..000000000
--- a/website/static/odoc/next/infer/TOPLlib__ToplUtils/index.html
+++ /dev/null
@@ -1,2 +0,0 @@
-
-TOPLlib__ToplUtils (infer.TOPLlib__ToplUtils) Up – infer » TOPLlib__ToplUtilsModule TOPLlib__ToplUtils
val any_type : IR.Typ.t
For now, Topl is untyped. The "any" type is simulated with "java.lang.Object".
val topl_class_name : IR.Typ.Name.t
val topl_class_typ : IR.Typ.t
val topl_class_pvar : IR.Pvar.t
val static_var : string -> IR.Exp.t
val local_var : IR.Procname.t -> string -> IR.Exp.t
val constant_int : int -> IR.Exp.t
val topl_call : IR.Ident.t -> IR.Typ.desc -> IBase.Location.t -> string -> (IR.Exp.t * IR.Typ.t ) list -> IR.Sil.instr
Call a TOPL function; that is, a static member of "topl.Property" with java.lang.Object arguments and return ret_id
of type ret_typ
.
val is_synthesized : IR.Procname.t -> bool
val debug : ('a , Stdlib.Format.formatter, unit) IStdlib.IStd .format -> 'a
val make_field : string -> IR.Fieldname.t
val binop_to : TOPLlib.ToplAst.binop -> IR.Binop.t
\ No newline at end of file