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)

Module 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)

Module 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)

Module 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)

Module 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)

Module Biabduction.Predicates

module F = Stdlib.Format
type offset =
| Off_fld of IR.Fieldname.t * IR.Typ.t
| Off_index of IR.Exp.t

Offset for an lvalue.

Components of Propositions

type atom =
| Aeq of IR.Exp.t * IR.Exp.t

equality

| Aneq of IR.Exp.t * IR.Exp.t

disequality

| Apred of IR.PredSymb.t * IR.Exp.t list

predicate symbol applied to exps

| Anpred of IR.PredSymb.t * IR.Exp.t list

negated predicate symbol applied to exps

an atom is a pure atomic formula

val compare_atom : atom -> atom -> int
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 compare_lseg_kind : lseg_kind -> lseg_kind -> int
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 =
| Iabstraction
| Iactual_precondition
| Ialloc
| Iformal of zero_flag * null_case_flag
| Iinitial
| Ilookup
| Inone
| Inullify
| Irearrange of zero_flag * null_case_flag * int * IR.PredSymb.path_pos
| Itaint
| Iupdate of zero_flag * null_case_flag * int * IR.PredSymb.path_pos
| Ireturn_from_call of int

instrumentation of heap values

val compare_inst : inst -> inst -> int
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 = {
root : IR.Ident.t;
next : IR.Ident.t;
svars : IR.Ident.t list;
evars : IR.Ident.t list;
body : 'inst hpred0 list;
}
and 'inst hpara_dll0 = {
cell : IR.Ident.t;

address cell

svars_dll : IR.Ident.t list;
evars_dll : IR.Ident.t list;
body_dll : 'inst hpred0 list;
}

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

Compaction

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 Functions

val 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

Functions for traversing SIL data types

val strexp_expmap : ((IR.Exp.t * inst option) -> IR.Exp.t * inst option) -> strexp -> strexp

Change exps in strexp using f. WARNING: the result might not be normalized.

val hpred_expmap : ((IR.Exp.t * inst option) -> IR.Exp.t * inst option) -> hpred -> hpred

Change exps in hpred by f. WARNING: the result might not be normalized.

val hpred_instmap : (inst -> inst) -> hpred -> hpred

Change instrumentations in hpred using f.

val hpred_list_expmap : ((IR.Exp.t * inst option) -> IR.Exp.t * inst option) -> hpred list -> hpred list

Change exps in hpred list by f. WARNING: the result might not be normalized.

val atom_expmap : (IR.Exp.t -> IR.Exp.t) -> atom -> atom

Change exps in atom by f. WARNING: the result might not be normalized.

val hpred_list_get_lexps : (IR.Exp.t -> bool) -> hpred list -> IR.Exp.t list
val hpred_entries : hpred -> IR.Exp.t list
val atom_free_vars : atom -> IR.Ident.t IStdlib.IStd.Sequence.t
val atom_gen_free_vars : atom -> (unit, IR.Ident.t) IStdlib.IStd.Sequence.Generator.t
val hpred_free_vars : hpred -> IR.Ident.t IStdlib.IStd.Sequence.t
val hpred_gen_free_vars : hpred -> (unit, IR.Ident.t) IStdlib.IStd.Sequence.Generator.t
val hpara_shallow_free_vars : hpara -> IR.Ident.t IStdlib.IStd.Sequence.t
val hpara_dll_shallow_free_vars : hpara_dll -> IR.Ident.t IStdlib.IStd.Sequence.t

Variables in hpara_dll, excluding bound vars in the body

Substitution

type subst = private (IR.Ident.t * IR.Exp.t) list
val compare_subst : subst -> subst -> int
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 replacing occurrences of expressions.

val exp_replace_exp : (IR.Exp.t * IR.Exp.t) list -> IR.Exp.t -> IR.Exp.t
val atom_replace_exp : (IR.Exp.t * IR.Exp.t) list -> atom -> atom
val hpred_replace_exp : (IR.Exp.t * IR.Exp.t) list -> hpred -> hpred

Functions for constructing or destructing entities in this module

val 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)

Module Biabduction.Predicates

module F = Stdlib.Format
type offset =
| Off_fld of IR.Fieldname.t * IR.Typ.t
| Off_index of IR.Exp.t

Offset for an lvalue.

Components of Propositions

type atom =
| Aeq of IR.Exp.t * IR.Exp.t

equality

| Aneq of IR.Exp.t * IR.Exp.t

disequality

| Apred of IR.PredSymb.t * IR.Exp.t list

predicate symbol applied to exps

| Anpred of IR.PredSymb.t * IR.Exp.t list

negated predicate symbol applied to exps

an atom is a pure atomic formula

val compare_atom : atom -> atom -> int
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 compare_lseg_kind : lseg_kind -> lseg_kind -> int
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 =
| Iabstraction
| Iactual_precondition
| Ialloc
| Iformal of zero_flag * null_case_flag
| Iinitial
| Ilookup
| Inone
| Inullify
| Irearrange of zero_flag * null_case_flag * int * IR.PredSymb.path_pos
| Itaint
| Iupdate of zero_flag * null_case_flag * int * IR.PredSymb.path_pos
| Ireturn_from_call of int

instrumentation of heap values

val compare_inst : inst -> inst -> int
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 = {
root : IR.Ident.t;
next : IR.Ident.t;
svars : IR.Ident.t list;
evars : IR.Ident.t list;
body : 'inst hpred0 list;
}
and 'inst hpara_dll0 = {
cell : IR.Ident.t;

address cell

svars_dll : IR.Ident.t list;
evars_dll : IR.Ident.t list;
body_dll : 'inst hpred0 list;
}

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

Compaction

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 Functions

val 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

Functions for traversing SIL data types

val strexp_expmap : ((IR.Exp.t * inst option) -> IR.Exp.t * inst option) -> strexp -> strexp

Change exps in strexp using f. WARNING: the result might not be normalized.

val hpred_expmap : ((IR.Exp.t * inst option) -> IR.Exp.t * inst option) -> hpred -> hpred

Change exps in hpred by f. WARNING: the result might not be normalized.

val hpred_instmap : (inst -> inst) -> hpred -> hpred

Change instrumentations in hpred using f.

val hpred_list_expmap : ((IR.Exp.t * inst option) -> IR.Exp.t * inst option) -> hpred list -> hpred list

Change exps in hpred list by f. WARNING: the result might not be normalized.

val atom_expmap : (IR.Exp.t -> IR.Exp.t) -> atom -> atom

Change exps in atom by f. WARNING: the result might not be normalized.

val hpred_list_get_lexps : (IR.Exp.t -> bool) -> hpred list -> IR.Exp.t list
val hpred_entries : hpred -> IR.Exp.t list
val atom_free_vars : atom -> IR.Ident.t IStdlib.IStd.Sequence.t
val atom_gen_free_vars : atom -> (unit, IR.Ident.t) IStdlib.IStd.Sequence.Generator.t
val hpred_free_vars : hpred -> IR.Ident.t IStdlib.IStd.Sequence.t
val hpred_gen_free_vars : hpred -> (unit, IR.Ident.t) IStdlib.IStd.Sequence.Generator.t
val hpara_shallow_free_vars : hpara -> IR.Ident.t IStdlib.IStd.Sequence.t
val hpara_dll_shallow_free_vars : hpara_dll -> IR.Ident.t IStdlib.IStd.Sequence.t

Variables in hpara_dll, excluding bound vars in the body

Substitution

type subst = private (IR.Ident.t * IR.Exp.t) list
val compare_subst : subst -> subst -> int
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 replacing occurrences of expressions.

val atom_replace_exp : (IR.Exp.t * IR.Exp.t) list -> atom -> atom
val hpred_replace_exp : (IR.Exp.t * IR.Exp.t) list -> hpred -> hpred

Functions for constructing or destructing entities in this module

val 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)

Module Biabduction__Predicates

module F = Stdlib.Format
type offset =
| Off_fld of IR.Fieldname.t * IR.Typ.t
| Off_index of IR.Exp.t

Offset for an lvalue.

Components of Propositions

type atom =
| Aeq of IR.Exp.t * IR.Exp.t

equality

| Aneq of IR.Exp.t * IR.Exp.t

disequality

| Apred of IR.PredSymb.t * IR.Exp.t list

predicate symbol applied to exps

| Anpred of IR.PredSymb.t * IR.Exp.t list

negated predicate symbol applied to exps

an atom is a pure atomic formula

val compare_atom : atom -> atom -> int
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 compare_lseg_kind : lseg_kind -> lseg_kind -> int
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 =
| Iabstraction
| Iactual_precondition
| Ialloc
| Iformal of zero_flag * null_case_flag
| Iinitial
| Ilookup
| Inone
| Inullify
| Irearrange of zero_flag * null_case_flag * int * IR.PredSymb.path_pos
| Itaint
| Iupdate of zero_flag * null_case_flag * int * IR.PredSymb.path_pos
| Ireturn_from_call of int

instrumentation of heap values

val compare_inst : inst -> inst -> int
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 = {
root : IR.Ident.t;
next : IR.Ident.t;
svars : IR.Ident.t list;
evars : IR.Ident.t list;
body : 'inst hpred0 list;
}
and 'inst hpara_dll0 = {
cell : IR.Ident.t;

address cell

svars_dll : IR.Ident.t list;
evars_dll : IR.Ident.t list;
body_dll : 'inst hpred0 list;
}

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

Compaction

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 Functions

val 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

Functions for traversing SIL data types

val strexp_expmap : ((IR.Exp.t * inst option) -> IR.Exp.t * inst option) -> strexp -> strexp

Change exps in strexp using f. WARNING: the result might not be normalized.

val hpred_expmap : ((IR.Exp.t * inst option) -> IR.Exp.t * inst option) -> hpred -> hpred

Change exps in hpred by f. WARNING: the result might not be normalized.

val hpred_instmap : (inst -> inst) -> hpred -> hpred

Change instrumentations in hpred using f.

val hpred_list_expmap : ((IR.Exp.t * inst option) -> IR.Exp.t * inst option) -> hpred list -> hpred list

Change exps in hpred list by f. WARNING: the result might not be normalized.

val atom_expmap : (IR.Exp.t -> IR.Exp.t) -> atom -> atom

Change exps in atom by f. WARNING: the result might not be normalized.

val hpred_list_get_lexps : (IR.Exp.t -> bool) -> hpred list -> IR.Exp.t list
val hpred_entries : hpred -> IR.Exp.t list
val atom_free_vars : atom -> IR.Ident.t IStdlib.IStd.Sequence.t
val atom_gen_free_vars : atom -> (unit, IR.Ident.t) IStdlib.IStd.Sequence.Generator.t
val hpred_free_vars : hpred -> IR.Ident.t IStdlib.IStd.Sequence.t
val hpred_gen_free_vars : hpred -> (unit, IR.Ident.t) IStdlib.IStd.Sequence.Generator.t
val hpara_shallow_free_vars : hpara -> IR.Ident.t IStdlib.IStd.Sequence.t
val hpara_dll_shallow_free_vars : hpara_dll -> IR.Ident.t IStdlib.IStd.Sequence.t

Variables in hpara_dll, excluding bound vars in the body

Substitution

type subst = private (IR.Ident.t * IR.Exp.t) list
val compare_subst : subst -> subst -> int
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 replacing occurrences of expressions.

val exp_replace_exp : (IR.Exp.t * IR.Exp.t) list -> IR.Exp.t -> IR.Exp.t
val atom_replace_exp : (IR.Exp.t * IR.Exp.t) list -> atom -> atom
val hpred_replace_exp : (IR.Exp.t * IR.Exp.t) list -> hpred -> hpred

Functions for constructing or destructing entities in this module

val 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)

Module Biabduction__Predicates

module F = Stdlib.Format
type offset =
| Off_fld of IR.Fieldname.t * IR.Typ.t
| Off_index of IR.Exp.t

Offset for an lvalue.

Components of Propositions

type atom =
| Aeq of IR.Exp.t * IR.Exp.t

equality

| Aneq of IR.Exp.t * IR.Exp.t

disequality

| Apred of IR.PredSymb.t * IR.Exp.t list

predicate symbol applied to exps

| Anpred of IR.PredSymb.t * IR.Exp.t list

negated predicate symbol applied to exps

an atom is a pure atomic formula

val compare_atom : atom -> atom -> int
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 compare_lseg_kind : lseg_kind -> lseg_kind -> int
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 =
| Iabstraction
| Iactual_precondition
| Ialloc
| Iformal of zero_flag * null_case_flag
| Iinitial
| Ilookup
| Inone
| Inullify
| Irearrange of zero_flag * null_case_flag * int * IR.PredSymb.path_pos
| Itaint
| Iupdate of zero_flag * null_case_flag * int * IR.PredSymb.path_pos
| Ireturn_from_call of int

instrumentation of heap values

val compare_inst : inst -> inst -> int
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 = {
root : IR.Ident.t;
next : IR.Ident.t;
svars : IR.Ident.t list;
evars : IR.Ident.t list;
body : 'inst hpred0 list;
}
and 'inst hpara_dll0 = {
cell : IR.Ident.t;

address cell

svars_dll : IR.Ident.t list;
evars_dll : IR.Ident.t list;
body_dll : 'inst hpred0 list;
}

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

Compaction

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 Functions

val 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

Functions for traversing SIL data types

val strexp_expmap : ((IR.Exp.t * inst option) -> IR.Exp.t * inst option) -> strexp -> strexp

Change exps in strexp using f. WARNING: the result might not be normalized.

val hpred_expmap : ((IR.Exp.t * inst option) -> IR.Exp.t * inst option) -> hpred -> hpred

Change exps in hpred by f. WARNING: the result might not be normalized.

val hpred_instmap : (inst -> inst) -> hpred -> hpred

Change instrumentations in hpred using f.

val hpred_list_expmap : ((IR.Exp.t * inst option) -> IR.Exp.t * inst option) -> hpred list -> hpred list

Change exps in hpred list by f. WARNING: the result might not be normalized.

val atom_expmap : (IR.Exp.t -> IR.Exp.t) -> atom -> atom

Change exps in atom by f. WARNING: the result might not be normalized.

val hpred_list_get_lexps : (IR.Exp.t -> bool) -> hpred list -> IR.Exp.t list
val hpred_entries : hpred -> IR.Exp.t list
val atom_free_vars : atom -> IR.Ident.t IStdlib.IStd.Sequence.t
val atom_gen_free_vars : atom -> (unit, IR.Ident.t) IStdlib.IStd.Sequence.Generator.t
val hpred_free_vars : hpred -> IR.Ident.t IStdlib.IStd.Sequence.t
val hpred_gen_free_vars : hpred -> (unit, IR.Ident.t) IStdlib.IStd.Sequence.Generator.t
val hpara_shallow_free_vars : hpara -> IR.Ident.t IStdlib.IStd.Sequence.t
val hpara_dll_shallow_free_vars : hpara_dll -> IR.Ident.t IStdlib.IStd.Sequence.t

Variables in hpara_dll, excluding bound vars in the body

Substitution

type subst = private (IR.Ident.t * IR.Exp.t) list
val compare_subst : subst -> subst -> int
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 replacing occurrences of expressions.

val atom_replace_exp : (IR.Exp.t * IR.Exp.t) list -> atom -> atom
val hpred_replace_exp : (IR.Exp.t * IR.Exp.t) list -> hpred -> hpred

Functions for constructing or destructing entities in this module

val 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)

Module 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)

Module 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)

Module IBase.Config

type os_type =
| Unix
| Win32
| Cygwin
type build_system =
| BAnt
| BBuck
| BClang
| BGradle
| BJava
| BJavac
| BMake
| BMvn
| BNdk
| BXcode
type scheduler =
| File
| Restart
| SyntacticCallGraph
val equal_scheduler : scheduler -> scheduler -> bool
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 values

val 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 options

val 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_extra_flags : string list
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 only_footprint : 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 skip_translation_headers : string list
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 options

val 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 options

val clang_compilation_dbs : [ `Escaped of string | `Raw of string ] list
\ No newline at end of file +Config (infer.IBase.Config)

Module IBase.Config

type os_type =
| Unix
| Win32
| Cygwin
type build_system =
| BAnt
| BBuck
| BClang
| BGradle
| BJava
| BJavac
| BMake
| BMvn
| BNdk
| BXcode
type scheduler =
| File
| Restart
| SyntacticCallGraph
val equal_scheduler : scheduler -> scheduler -> bool
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 values

val 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 options

val 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_only_footprint : 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_extra_flags : string list
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 skip_translation_headers : string list
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 options

val 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 options

val 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)

Module 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 compare_visibility : visibility -> visibility -> int
val equal_visibility : visibility -> visibility -> bool
val string_of_visibility : visibility -> string
type severity =
| Like
| Info
| Advice
| Warning
| Error

severity of the report

val compare_severity : severity -> severity -> int
val equal_severity : severity -> severity -> bool
val all_of_severity : severity list
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 bad_footprint : 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_in_footprint : 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
module Map : IStdlib.PrettyPrintable.PPMap with type PPMap.key = t
\ No newline at end of file +IssueType (infer.IBase.IssueType)

Module 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 compare_visibility : visibility -> visibility -> int
val equal_visibility : visibility -> visibility -> bool
val string_of_visibility : visibility -> string
type severity =
| Like
| Info
| Advice
| Warning
| Error

severity of the report

val compare_severity : severity -> severity -> int
val equal_severity : severity -> severity -> bool
val all_of_severity : severity list
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 bad_footprint : 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_in_footprint : 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
module Map : IStdlib.PrettyPrintable.PPMap with type PPMap.key = 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 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)

Module 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)

Module 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)

Module IBase__Config

type os_type =
| Unix
| Win32
| Cygwin
type build_system =
| BAnt
| BBuck
| BClang
| BGradle
| BJava
| BJavac
| BMake
| BMvn
| BNdk
| BXcode
type scheduler =
| File
| Restart
| SyntacticCallGraph
val equal_scheduler : scheduler -> scheduler -> bool
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 values

val 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 options

val 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_extra_flags : string list
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 only_footprint : 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 skip_translation_headers : string list
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 options

val 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 options

val clang_compilation_dbs : [ `Escaped of string | `Raw of string ] list
\ No newline at end of file +IBase__Config (infer.IBase__Config)

Module IBase__Config

type os_type =
| Unix
| Win32
| Cygwin
type build_system =
| BAnt
| BBuck
| BClang
| BGradle
| BJava
| BJavac
| BMake
| BMvn
| BNdk
| BXcode
type scheduler =
| File
| Restart
| SyntacticCallGraph
val equal_scheduler : scheduler -> scheduler -> bool
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 values

val 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 options

val 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_only_footprint : 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_extra_flags : string list
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 skip_translation_headers : string list
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 options

val 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 options

val 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)

Module 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 compare_visibility : visibility -> visibility -> int
val equal_visibility : visibility -> visibility -> bool
val string_of_visibility : visibility -> string
type severity =
| Like
| Info
| Advice
| Warning
| Error

severity of the report

val compare_severity : severity -> severity -> int
val equal_severity : severity -> severity -> bool
val all_of_severity : severity list
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 bad_footprint : 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_in_footprint : 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
module Map : IStdlib.PrettyPrintable.PPMap with type PPMap.key = t
\ No newline at end of file +IBase__IssueType (infer.IBase__IssueType)

Module 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 compare_visibility : visibility -> visibility -> int
val equal_visibility : visibility -> visibility -> bool
val string_of_visibility : visibility -> string
type severity =
| Like
| Info
| Advice
| Warning
| Error

severity of the report

val compare_severity : severity -> severity -> int
val equal_severity : severity -> severity -> bool
val all_of_severity : severity list
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 bad_footprint : 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_in_footprint : 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
module Map : IStdlib.PrettyPrintable.PPMap with type PPMap.key = t
\ 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)

Module IR.Exp

module F = Stdlib.Format
type closure = {
name : Procname.t;
captured_vars : (t * Pvar.t * Typ.t * Pvar.capture_mode) list;
}
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 compare_closure : closure -> closure -> int
val compare_sizeof_data : sizeof_data -> sizeof_data -> int
val compare : t -> t -> int
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 Expressions

val 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)

Module IR.Exp

module F = Stdlib.Format
type closure = {
name : Procname.t;
captured_vars : (t * Pvar.t * Typ.t * Pvar.capture_mode) list;
}
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 compare_closure : closure -> closure -> int
val compare_sizeof_data : sizeof_data -> sizeof_data -> int
val compare : t -> t -> int
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 Expressions

val 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)

Module 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)

Module 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 IR.Procdesc

Per-procedure CFG

module NodeKey : sig ... end
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 IR.Procdesc

Per-procedure CFG

module NodeKey : sig ... end
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)

Module IR.Pvar

module F = Stdlib.Format
type translation_unit = IBase.SourceFile.t option
val compare_translation_unit : translation_unit -> translation_unit -> int
type t

Type for program variables. There are 4 kinds of variables:

  1. local variables, used for local variables and formal parameters
  2. callee program variables, used to handle recursion (x | callee is distinguished from x)
  3. global variables
  4. 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 =
| ByReference
| ByValue
val compare_capture_mode : capture_mode -> capture_mode -> int
val equal_capture_mode : capture_mode -> capture_mode -> bool
val string_of_capture_mode : capture_mode -> string
\ No newline at end of file +Pvar (infer.IR.Pvar)

Module IR.Pvar

module F = Stdlib.Format
type translation_unit = IBase.SourceFile.t option
val compare_translation_unit : translation_unit -> translation_unit -> int
type t

Type for program variables. There are 4 kinds of variables:

  1. local variables, used for local variables and formal parameters
  2. callee program variables, used to handle recursion (x | callee is distinguished from x)
  3. global variables
  4. 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 =
| ByReference
| ByValue
val compare_capture_mode : capture_mode -> capture_mode -> int
val equal_capture_mode : capture_mode -> capture_mode -> bool
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)

Module IR__Exp

The Smallfoot Intermediate Language: Expressions

NOTE: For doing substitutionson expressions, there are some functions in Sil.

module F = Stdlib.Format
type closure = {
name : IR.Procname.t;
captured_vars : (t * IR.Pvar.t * IR.Typ.t * IR.Pvar.capture_mode) list;
}
and sizeof_data = {
typ : IR.Typ.t;
nbytes : int option;
dynamic_length : t option;
subtype : IR.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 IR.Ident.t

Pure variable: it is not an lvalue

| UnOp of IR.Unop.t * t * IR.Typ.t option

Unary operator with type of the result if known

| BinOp of IR.Binop.t * t * t

Binary operator

| Exn of t

Exception

| Closure of closure

Anonymous function

| Const of IR.Const.t

Constants

| Cast of IR.Typ.t * t

Type cast

| Lvar of IR.Pvar.t

The address of a program variable

| Lfield of t * IR.Fieldname.t * IR.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 compare_closure : closure -> closure -> int
val compare_sizeof_data : sizeof_data -> sizeof_data -> int
val compare : t -> t -> int
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 Expressions

val 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)

Module IR__Exp

The Smallfoot Intermediate Language: Expressions

NOTE: For doing substitutionson expressions, there are some functions in Sil.

module F = Stdlib.Format
type closure = {
name : IR.Procname.t;
captured_vars : (t * IR.Pvar.t * IR.Typ.t * IR.Pvar.capture_mode) list;
}
and sizeof_data = {
typ : IR.Typ.t;
nbytes : int option;
dynamic_length : t option;
subtype : IR.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 IR.Ident.t

Pure variable: it is not an lvalue

| UnOp of IR.Unop.t * t * IR.Typ.t option

Unary operator with type of the result if known

| BinOp of IR.Binop.t * t * t

Binary operator

| Exn of t

Exception

| Closure of closure

Anonymous function

| Const of IR.Const.t

Constants

| Cast of IR.Typ.t * t

Type cast

| Lvar of IR.Pvar.t

The address of a program variable

| Lfield of t * IR.Fieldname.t * IR.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 compare_closure : closure -> closure -> int
val compare_sizeof_data : sizeof_data -> sizeof_data -> int
val compare : t -> t -> int
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 Expressions

val 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)

Module 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)

Module 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)

Module IR__Procdesc

Per-procedure CFG

module NodeKey : sig ... end
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)

Module IR__Procdesc

Per-procedure CFG

module NodeKey : sig ... end
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)

Module IR__Pvar

Program variables.

module F = Stdlib.Format
type translation_unit = IBase.SourceFile.t option
val compare_translation_unit : translation_unit -> translation_unit -> int
type t

Type for program variables. There are 4 kinds of variables:

  1. local variables, used for local variables and formal parameters
  2. callee program variables, used to handle recursion (x | callee is distinguished from x)
  3. global variables
  4. 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 =
| ByReference
| ByValue
val compare_capture_mode : capture_mode -> capture_mode -> int
val equal_capture_mode : capture_mode -> capture_mode -> bool
val string_of_capture_mode : capture_mode -> string
\ No newline at end of file +IR__Pvar (infer.IR__Pvar)

Module IR__Pvar

Program variables.

module F = Stdlib.Format
type translation_unit = IBase.SourceFile.t option
val compare_translation_unit : translation_unit -> translation_unit -> int
type t

Type for program variables. There are 4 kinds of variables:

  1. local variables, used for local variables and formal parameters
  2. callee program variables, used to handle recursion (x | callee is distinguished from x)
  3. global variables
  4. 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 =
| ByReference
| ByValue
val compare_capture_mode : capture_mode -> capture_mode -> int
val equal_capture_mode : capture_mode -> capture_mode -> bool
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)

Module Pulselib.PulseCItv

module F = Stdlib.Format
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)

Module Pulselib.PulseCItv

module F = Stdlib.Format
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)

Module Pulselib.PulseFormula

module F = Stdlib.Format
module SatUnsat = PulseSatUnsat
module Var = PulseAbstractValue

Arithmetic solver

Build formulas from SIL and tries to decide if they are (mostly un-)satisfiable.

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 =
| LiteralOperand of IR.IntLit.t
| AbstractValueOperand of Var.t

Build formulas

type new_eq =
| EqZero of Var.t
| Equal of Var.t * Var.t

some operations will return a set of new facts discovered that are relevant to communicate to the memory domain

type new_eqs = new_eq list
val ttrue : t
val and_equal : operand -> operand -> t -> (t * new_eqs) SatUnsat.t
val and_equal_instanceof : Var.t -> Var.t -> IR.Typ.t -> t -> (t * new_eqs) SatUnsat.t
val and_less_equal : operand -> operand -> t -> (t * new_eqs) SatUnsat.t
val and_less_than : operand -> operand -> t -> (t * new_eqs) SatUnsat.t
val and_equal_unop : Var.t -> IR.Unop.t -> operand -> t -> (t * new_eqs) SatUnsat.t
val and_equal_binop : Var.t -> IR.Binop.t -> operand -> operand -> t -> (t * new_eqs) SatUnsat.t
val prune_binop : negated:bool -> IR.Binop.t -> operand -> operand -> t -> (t * new_eqs) SatUnsat.t

Operations

val normalize : IR.Tenv.t -> get_dynamic_type:(Var.t -> IR.Typ.t option) -> t -> (t * new_eqs) SatUnsat.t

think a bit harder about the formula

val simplify : IR.Tenv.t -> get_dynamic_type:(Var.t -> IR.Typ.t option) -> keep:Var.Set.t -> t -> (t * new_eqs) SatUnsat.t
val and_fold_subst_variables : t -> up_to_f:t -> init:'acc -> f:('acc -> Var.t -> 'acc * Var.t) -> ('acc * t * new_eqs) SatUnsat.t
val is_known_zero : t -> Var.t -> bool
val as_int : t -> Var.t -> int option
val has_no_assumptions : t -> bool
val get_var_repr : t -> Var.t -> Var.t

get the canonical representative for the variable according to the equality relation

module DynamicTypes : sig ... end

Module for reasoning about dynamic types. *

\ No newline at end of file +PulseFormula (infer.Pulselib.PulseFormula)

Module Pulselib.PulseFormula

module F = Stdlib.Format
module SatUnsat = PulseSatUnsat
module Var = PulseAbstractValue

Arithmetic solver

Build formulas from SIL and tries to decide if they are (mostly un-)satisfiable.

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 =
| LiteralOperand of IR.IntLit.t
| AbstractValueOperand of Var.t

Build formulas

type new_eq =
| EqZero of Var.t
| Equal of Var.t * Var.t

some operations will return a set of new facts discovered that are relevant to communicate to the memory domain

type new_eqs = new_eq list
val ttrue : t
val and_equal : operand -> operand -> t -> (t * new_eqs) SatUnsat.t
val and_equal_instanceof : Var.t -> Var.t -> IR.Typ.t -> t -> (t * new_eqs) SatUnsat.t
val and_less_equal : operand -> operand -> t -> (t * new_eqs) SatUnsat.t
val and_less_than : operand -> operand -> t -> (t * new_eqs) SatUnsat.t
val and_equal_unop : Var.t -> IR.Unop.t -> operand -> t -> (t * new_eqs) SatUnsat.t
val and_equal_binop : Var.t -> IR.Binop.t -> operand -> operand -> t -> (t * new_eqs) SatUnsat.t
val prune_binop : negated:bool -> IR.Binop.t -> operand -> operand -> t -> (t * new_eqs) SatUnsat.t

Operations

val normalize : IR.Tenv.t -> get_dynamic_type:(Var.t -> IR.Typ.t option) -> t -> (t * new_eqs) SatUnsat.t

think a bit harder about the formula

val simplify : IR.Tenv.t -> get_dynamic_type:(Var.t -> IR.Typ.t option) -> keep:Var.Set.t -> t -> (t * new_eqs) SatUnsat.t
val and_fold_subst_variables : t -> up_to_f:t -> init:'acc -> f:('acc -> Var.t -> 'acc * Var.t) -> ('acc * t * new_eqs) SatUnsat.t
val is_known_zero : t -> Var.t -> bool
val has_no_assumptions : t -> bool
val get_var_repr : t -> Var.t -> Var.t

get the canonical representative for the variable according to the equality relation

module DynamicTypes : sig ... end

Module for reasoning about dynamic types. *

\ 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)

Module Pulselib.PulsePathCondition

module F = Stdlib.Format
module AbstractValue = PulseAbstractValue
module SatUnsat = PulseSatUnsat
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

Building arithmetic constraints

val and_nonnegative : AbstractValue.t -> t -> t * new_eqs

and_nonnegative v phi is phi ∧ v≥0

val and_positive : AbstractValue.t -> t -> t * new_eqs

and_positive v phi is phi ∧ v>0

val and_eq_int : AbstractValue.t -> IR.IntLit.t -> t -> t * new_eqs

and_eq_int v i phi is phi ∧ v=i

val and_eq_vars : AbstractValue.t -> AbstractValue.t -> t -> t * new_eqs
val simplify : IR.Tenv.t -> keep:AbstractValue.Set.t -> get_dynamic_type:(AbstractValue.t -> IR.Typ.t option) -> t -> (t * new_eqs) SatUnsat.t

simplify ~keep phi attempts to get rid of as many variables in fv phi but not in keep as possible

val simplify_instanceof : IR.Tenv.t -> get_dynamic_type:(AbstractValue.t -> IR.Typ.t option) -> t -> t
val and_callee : (AbstractValue.t * ValueHistory.t) AbstractValue.Map.t -> t -> callee:t -> (AbstractValue.t * ValueHistory.t) AbstractValue.Map.t * t * new_eqs

Operations

type operand =
| LiteralOperand of IR.IntLit.t
| AbstractValueOperand of AbstractValue.t
val compare_operand : operand -> operand -> int
val pp_operand : IStdlib.IStd.Formatter.t -> operand -> unit
val eval_binop : AbstractValue.t -> IR.Binop.t -> operand -> operand -> t -> t * new_eqs
val eval_unop : AbstractValue.t -> IR.Unop.t -> AbstractValue.t -> t -> t * new_eqs
val prune_binop : negated:bool -> IR.Binop.t -> operand -> operand -> t -> t * new_eqs
val and_eq_instanceof : AbstractValue.t -> AbstractValue.t -> IR.Typ.t -> t -> t * new_eqs

Queries

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)

Module Pulselib.PulsePathCondition

module F = Stdlib.Format
module AbstractValue = PulseAbstractValue
module SatUnsat = PulseSatUnsat
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

Building arithmetic constraints

val and_nonnegative : AbstractValue.t -> t -> t * new_eqs

and_nonnegative v phi is phi ∧ v≥0

val and_positive : AbstractValue.t -> t -> t * new_eqs

and_positive v phi is phi ∧ v>0

val and_eq_int : AbstractValue.t -> IR.IntLit.t -> t -> t * new_eqs

and_eq_int v i phi is phi ∧ v=i

val and_eq_vars : AbstractValue.t -> AbstractValue.t -> t -> t * new_eqs
val simplify : IR.Tenv.t -> keep:AbstractValue.Set.t -> get_dynamic_type:(AbstractValue.t -> IR.Typ.t option) -> t -> (t * new_eqs) SatUnsat.t

simplify ~keep phi attempts to get rid of as many variables in fv phi but not in keep as possible

val simplify_instanceof : IR.Tenv.t -> get_dynamic_type:(AbstractValue.t -> IR.Typ.t option) -> t -> t
val and_callee : (AbstractValue.t * ValueHistory.t) AbstractValue.Map.t -> t -> callee:t -> (AbstractValue.t * ValueHistory.t) AbstractValue.Map.t * t * new_eqs

Operations

type operand =
| LiteralOperand of IR.IntLit.t
| AbstractValueOperand of AbstractValue.t
val compare_operand : operand -> operand -> int
val pp_operand : IStdlib.IStd.Formatter.t -> operand -> unit
val eval_binop : AbstractValue.t -> IR.Binop.t -> operand -> operand -> t -> t * new_eqs
val eval_unop : AbstractValue.t -> IR.Unop.t -> AbstractValue.t -> t -> t * new_eqs
val prune_binop : negated:bool -> IR.Binop.t -> operand -> operand -> t -> t * new_eqs
val and_eq_instanceof : AbstractValue.t -> AbstractValue.t -> IR.Typ.t -> t -> t * new_eqs

Queries

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)

Module 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)

Module 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)

Module 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)

Module Pulselib__PulseCItv

module F = Stdlib.Format
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)

Module Pulselib__PulseCItv

module F = Stdlib.Format
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)

Module Pulselib__PulseFormula

module F = Stdlib.Format
module SatUnsat = Pulselib.PulseSatUnsat

Arithmetic solver

Build formulas from SIL and tries to decide if they are (mostly un-)satisfiable.

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 =
| LiteralOperand of IR.IntLit.t
| AbstractValueOperand of Var.t

Build formulas

type new_eq =
| EqZero of Var.t
| Equal of Var.t * Var.t

some operations will return a set of new facts discovered that are relevant to communicate to the memory domain

type new_eqs = new_eq list
val ttrue : t
val and_equal : operand -> operand -> t -> (t * new_eqs) SatUnsat.t
val and_equal_instanceof : Var.t -> Var.t -> IR.Typ.t -> t -> (t * new_eqs) SatUnsat.t
val and_less_equal : operand -> operand -> t -> (t * new_eqs) SatUnsat.t
val and_less_than : operand -> operand -> t -> (t * new_eqs) SatUnsat.t
val and_equal_unop : Var.t -> IR.Unop.t -> operand -> t -> (t * new_eqs) SatUnsat.t
val and_equal_binop : Var.t -> IR.Binop.t -> operand -> operand -> t -> (t * new_eqs) SatUnsat.t
val prune_binop : negated:bool -> IR.Binop.t -> operand -> operand -> t -> (t * new_eqs) SatUnsat.t

Operations

val normalize : IR.Tenv.t -> get_dynamic_type:(Var.t -> IR.Typ.t option) -> t -> (t * new_eqs) SatUnsat.t

think a bit harder about the formula

val simplify : IR.Tenv.t -> get_dynamic_type:(Var.t -> IR.Typ.t option) -> keep:Var.Set.t -> t -> (t * new_eqs) SatUnsat.t
val and_fold_subst_variables : t -> up_to_f:t -> init:'acc -> f:('acc -> Var.t -> 'acc * Var.t) -> ('acc * t * new_eqs) SatUnsat.t
val is_known_zero : t -> Var.t -> bool
val as_int : t -> Var.t -> int option
val has_no_assumptions : t -> bool
val get_var_repr : t -> Var.t -> Var.t

get the canonical representative for the variable according to the equality relation

module DynamicTypes : sig ... end

Module for reasoning about dynamic types. *

\ No newline at end of file +Pulselib__PulseFormula (infer.Pulselib__PulseFormula)

Module Pulselib__PulseFormula

module F = Stdlib.Format
module SatUnsat = Pulselib.PulseSatUnsat

Arithmetic solver

Build formulas from SIL and tries to decide if they are (mostly un-)satisfiable.

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 =
| LiteralOperand of IR.IntLit.t
| AbstractValueOperand of Var.t

Build formulas

type new_eq =
| EqZero of Var.t
| Equal of Var.t * Var.t

some operations will return a set of new facts discovered that are relevant to communicate to the memory domain

type new_eqs = new_eq list
val ttrue : t
val and_equal : operand -> operand -> t -> (t * new_eqs) SatUnsat.t
val and_equal_instanceof : Var.t -> Var.t -> IR.Typ.t -> t -> (t * new_eqs) SatUnsat.t
val and_less_equal : operand -> operand -> t -> (t * new_eqs) SatUnsat.t
val and_less_than : operand -> operand -> t -> (t * new_eqs) SatUnsat.t
val and_equal_unop : Var.t -> IR.Unop.t -> operand -> t -> (t * new_eqs) SatUnsat.t
val and_equal_binop : Var.t -> IR.Binop.t -> operand -> operand -> t -> (t * new_eqs) SatUnsat.t
val prune_binop : negated:bool -> IR.Binop.t -> operand -> operand -> t -> (t * new_eqs) SatUnsat.t

Operations

val normalize : IR.Tenv.t -> get_dynamic_type:(Var.t -> IR.Typ.t option) -> t -> (t * new_eqs) SatUnsat.t

think a bit harder about the formula

val simplify : IR.Tenv.t -> get_dynamic_type:(Var.t -> IR.Typ.t option) -> keep:Var.Set.t -> t -> (t * new_eqs) SatUnsat.t
val and_fold_subst_variables : t -> up_to_f:t -> init:'acc -> f:('acc -> Var.t -> 'acc * Var.t) -> ('acc * t * new_eqs) SatUnsat.t
val is_known_zero : t -> Var.t -> bool
val has_no_assumptions : t -> bool
val get_var_repr : t -> Var.t -> Var.t

get the canonical representative for the variable according to the equality relation

module DynamicTypes : sig ... end

Module for reasoning about dynamic types. *

\ 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)

Module Pulselib__PulsePathCondition

module F = Stdlib.Format
module AbstractValue = Pulselib.PulseAbstractValue
module SatUnsat = Pulselib.PulseSatUnsat
module ValueHistory = Pulselib.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 = Pulselib.PulseFormula.new_eqs

Building arithmetic constraints

val and_nonnegative : AbstractValue.t -> t -> t * new_eqs

and_nonnegative v phi is phi ∧ v≥0

val and_positive : AbstractValue.t -> t -> t * new_eqs

and_positive v phi is phi ∧ v>0

val and_eq_int : AbstractValue.t -> IR.IntLit.t -> t -> t * new_eqs

and_eq_int v i phi is phi ∧ v=i

val and_eq_vars : AbstractValue.t -> AbstractValue.t -> t -> t * new_eqs
val simplify : IR.Tenv.t -> keep:AbstractValue.Set.t -> get_dynamic_type:(AbstractValue.t -> IR.Typ.t option) -> t -> (t * new_eqs) SatUnsat.t

simplify ~keep phi attempts to get rid of as many variables in fv phi but not in keep as possible

val simplify_instanceof : IR.Tenv.t -> get_dynamic_type:(AbstractValue.t -> IR.Typ.t option) -> t -> t
val and_callee : (AbstractValue.t * ValueHistory.t) AbstractValue.Map.t -> t -> callee:t -> (AbstractValue.t * ValueHistory.t) AbstractValue.Map.t * t * new_eqs

Operations

type operand =
| LiteralOperand of IR.IntLit.t
| AbstractValueOperand of AbstractValue.t
val compare_operand : operand -> operand -> int
val pp_operand : IStdlib.IStd.Formatter.t -> operand -> unit
val eval_binop : AbstractValue.t -> IR.Binop.t -> operand -> operand -> t -> t * new_eqs
val eval_unop : AbstractValue.t -> IR.Unop.t -> AbstractValue.t -> t -> t * new_eqs
val prune_binop : negated:bool -> IR.Binop.t -> operand -> operand -> t -> t * new_eqs
val and_eq_instanceof : AbstractValue.t -> AbstractValue.t -> IR.Typ.t -> t -> t * new_eqs

Queries

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)

Module Pulselib__PulsePathCondition

module F = Stdlib.Format
module AbstractValue = Pulselib.PulseAbstractValue
module SatUnsat = Pulselib.PulseSatUnsat
module ValueHistory = Pulselib.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 = Pulselib.PulseFormula.new_eqs

Building arithmetic constraints

val and_nonnegative : AbstractValue.t -> t -> t * new_eqs

and_nonnegative v phi is phi ∧ v≥0

val and_positive : AbstractValue.t -> t -> t * new_eqs

and_positive v phi is phi ∧ v>0

val and_eq_int : AbstractValue.t -> IR.IntLit.t -> t -> t * new_eqs

and_eq_int v i phi is phi ∧ v=i

val and_eq_vars : AbstractValue.t -> AbstractValue.t -> t -> t * new_eqs
val simplify : IR.Tenv.t -> keep:AbstractValue.Set.t -> get_dynamic_type:(AbstractValue.t -> IR.Typ.t option) -> t -> (t * new_eqs) SatUnsat.t

simplify ~keep phi attempts to get rid of as many variables in fv phi but not in keep as possible

val simplify_instanceof : IR.Tenv.t -> get_dynamic_type:(AbstractValue.t -> IR.Typ.t option) -> t -> t
val and_callee : (AbstractValue.t * ValueHistory.t) AbstractValue.Map.t -> t -> callee:t -> (AbstractValue.t * ValueHistory.t) AbstractValue.Map.t * t * new_eqs

Operations

type operand =
| LiteralOperand of IR.IntLit.t
| AbstractValueOperand of AbstractValue.t
val compare_operand : operand -> operand -> int
val pp_operand : IStdlib.IStd.Formatter.t -> operand -> unit
val eval_binop : AbstractValue.t -> IR.Binop.t -> operand -> operand -> t -> t * new_eqs
val eval_unop : AbstractValue.t -> IR.Unop.t -> AbstractValue.t -> t -> t * new_eqs
val prune_binop : negated:bool -> IR.Binop.t -> operand -> operand -> t -> t * new_eqs
val and_eq_instanceof : AbstractValue.t -> AbstractValue.t -> IR.Typ.t -> t -> t * new_eqs

Queries

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)

Module 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)

Module 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)

Module 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)

Module TOPLlib.ToplAutomaton

type t
type vindex = int

from 0 to vcount()-1, inclusive

val compare_vindex : vindex -> vindex -> int
type tindex = int

from 0 to tcount()-1, inclusive

type transition = {
source : vindex;
target : vindex;
label : ToplAst.label option;
}
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)

Module TOPLlib.ToplAutomaton

type t
type vindex = int

from 0 to vcount()-1, inclusive

val compare_vindex : vindex -> vindex -> int
type tindex = int

from 0 to tcount()-1, inclusive

type transition = {
source : vindex;
target : vindex;
label : ToplAst.label option;
}
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)

Module 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)

Module 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)

Module 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 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 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)

Module 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)

Module 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)

Module TOPLlib__ToplAutomaton

type t
type vindex = int

from 0 to vcount()-1, inclusive

val compare_vindex : vindex -> vindex -> int
type tindex = int

from 0 to tcount()-1, inclusive

type transition = {
source : vindex;
target : vindex;
label : TOPLlib.ToplAst.label option;
}
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)

Module TOPLlib__ToplAutomaton

type t
type vindex = int

from 0 to vcount()-1, inclusive

val compare_vindex : vindex -> vindex -> int
type tindex = int

from 0 to tcount()-1, inclusive

type transition = {
source : vindex;
target : vindex;
label : TOPLlib.ToplAst.label option;
}
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)

Module 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)

Module 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)

Module 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