diff --git a/infer/documentation/checkers/Topl.md b/infer/documentation/checkers/Topl.md new file mode 100644 index 000000000..1d4223fcf --- /dev/null +++ b/infer/documentation/checkers/Topl.md @@ -0,0 +1,97 @@ +# Topl + +## What is it? + +Topl is an analysis framework, built on top of Infer, for statically finding violations of temporal properties. Many analyses can be encoded as temporal properties supported by Topl, such as taint analysis. As a simple example, suppose that we don't want a value returned by method `source()` to be sent as an argument to a method `sink()`. This can be specified as follows: + +``` +property Taint + prefix "Main" + start -> start: * + start -> tracking: source(Ret) => x := Ret + tracking -> error: sink(Arg, VoidRet) when x == Arg +``` + +This specifies an automaton called `Taint` that has three states (`start`, `tracking`, `error`). Two of those states (`start` and `error`) have special meaning; other states (`tracking`) can have any names. The first transition (`start → tracking`) is taken when a method called `source()` is called, and its return value is stored in a register called `x`; the second transition (`tracking → error`) is taken when a method called `sink()` is called, but only if its argument equals what was previously saved in register `x`. +This property is violated in the following Java code: + +``` +public class Main { + static void f() { g(tito(source())); } + static void g(Object x) { h(x); } + static void h(Object x) { sink(x); } + static Object tito(Object x) { return x; } + static Object source() { return "dirty"; } + static void sink(Object x) {} +} +``` + +Note that `source()` and `sink()` are not called from the same method, and that the “dirty” object is passed around a few times before finally reaching the sink. Assuming that the property is in a file `taint.topl` and the Java code in a file `Main.java`, you can invoke Infer with the following command: + +``` +infer --topl --topl-properties taint.topl -- javac Main.java +``` + +It will display the following error: + +``` +Main.java:2: error: Topl Error + property Taint reaches state error. + 1. public class Main { + 2. > static void f() { g(tito(source())); } + 3. static void g(Object x) { h(x); } + 4. static void h(Object x) { sink(x); } +``` + +To get a full trace, use the command + +``` +infer explore +``` + +## Specifying Properties + +A property is a nondeterministic automaton that can remember values in registers. An execution that drives the automaton from the start state to the error state will make Infer report an issue, and the trace that it produces will indicate which parts of the program drive which transitions of the automaton. + +The general form of a property is the following: + +``` +property *Name +* message "Optional error message" // This line can be missing + prefix "Prefix" // There can be zero, one, or more prefix declarations + sourceState -> targetState: *Pattern*(Arg1,...,ArgN,Ret) when *Condition* => *Action* +``` + +The property name and the optional error message are used for reporting issues. The prefix declarations are used to simplify Patterns. The core of the property is the list of transitions. + +Each transition has a source state and a target state. The special transition label * means that the transition is always taken. Typically, there is a transition + +``` + start -> start: * +``` + +meaning that the property can start anywhere, not just at the beginning of a method. + +Otherwise, the label on a transition contains: + +* a *Pattern*, which indicates what kind of instruction in the program drives this transition; +* a list of transition variable bindings (above named Arg1, ..., but any identifier starting with uppercase letters works); +* possibly a boolean Condition, which can refer to transition variables and to registers; +* possibly and Action, which is a list sequence of assignments of the form *register* := *TransitionVariable* (registers do not need to be declared, and any identifier starting with a lowercase letter works). + +There are two types of patterns: + +* a regex that matches method names + * if the regex uses non-letters (such as dots) it must be within double-quotes; otherwise, double quotes are optional + * the prefix declarations are used to add potential prefixes to the regex. The combine regex is essentially “(prefix_regex_a | prefix_regex_b) transition_pattern_regex“ + * for a method with n arguments, there must be n+1 transition variables to get a match. The first n transition variables get bound to the argument values, and the last transition variable gets bound to the return value. *This is true even for the case in which the return type is void*. +* the special keyword **#ArrayWrite**. In that case, there should be two transition variables like “(Array, Index)” — Array gets bound to the array object, and Index gets bound to the index at which the write happens. + +For several examples, see https://github.com/facebook/infer/tree/master/infer/tests/codetoanalyze/java/topl + +## Limitations + +* By design, some problems may be missed. Topl is built on Pulse, which attempts to minimize false positives, at the cost of sometimes having false negatives. +* Analysis time increases exponentially with the number of registers used in properties. + * In theory, there should be no significant slowdown if registers belong to different properties, but the implementation is not yet optimized. + * If there are many registers within the same property, then the slowdown is unavoidable (without some significant breakthrough). However, the maximum number of registers we ever used for one practical property was 3. diff --git a/infer/man/man1/infer-analyze.txt b/infer/man/man1/infer-analyze.txt index 2eb933640..ae94c8cd8 100644 --- a/infer/man/man1/infer-analyze.txt +++ b/infer/man/man1/infer-analyze.txt @@ -411,9 +411,9 @@ OPTIONS (Conversely: --no-starvation-only) --topl - Activates: checker topl: Detects errors based on user-provided - state machines describing multi-object monitors. (Conversely: - --no-topl) + Activates: checker topl: Detect errors based on user-provided + state machines describing temporal properties over multiple + objects. (Conversely: --no-topl) --topl-only Activates: Enable topl and disable all other checkers (Conversely: diff --git a/infer/man/man1/infer-full.txt b/infer/man/man1/infer-full.txt index e36b7f5b8..22ccadece 100644 --- a/infer/man/man1/infer-full.txt +++ b/infer/man/man1/infer-full.txt @@ -1257,9 +1257,9 @@ OPTIONS @ThreadSafe See also infer-analyze(1). --topl - Activates: checker topl: Detects errors based on user-provided - state machines describing multi-object monitors. (Conversely: - --no-topl) See also infer-analyze(1). + Activates: checker topl: Detect errors based on user-provided + state machines describing temporal properties over multiple + objects. (Conversely: --no-topl) See also infer-analyze(1). --topl-only Activates: Enable topl and disable all other checkers (Conversely: @@ -2126,7 +2126,7 @@ INTERNAL OPTIONS scheduler. (Conversely: --no-trace-ondemand) --trace-topl - Activates: Detailed tracing information during TOPL analysis + Activates: Detailed tracing information during Topl analysis (Conversely: --no-trace-topl) --tv-commit commit diff --git a/infer/man/man1/infer.txt b/infer/man/man1/infer.txt index 7ae210822..0c81d300f 100644 --- a/infer/man/man1/infer.txt +++ b/infer/man/man1/infer.txt @@ -1257,9 +1257,9 @@ OPTIONS @ThreadSafe See also infer-analyze(1). --topl - Activates: checker topl: Detects errors based on user-provided - state machines describing multi-object monitors. (Conversely: - --no-topl) See also infer-analyze(1). + Activates: checker topl: Detect errors based on user-provided + state machines describing temporal properties over multiple + objects. (Conversely: --no-topl) See also infer-analyze(1). --topl-only Activates: Enable topl and disable all other checkers (Conversely: diff --git a/infer/src/backend/dune b/infer/src/backend/dune index d22d2e752..9907a6b7b 100644 --- a/infer/src/backend/dune +++ b/infer/src/backend/dune @@ -10,9 +10,9 @@ (:standard -open Core -open IStdlib -open IStd -open OpenSource -open ATDGenerated -open IBase -open IR -open Absint -open Biabduction -open BO -open Nullsafe -open Pulselib -open Checkers -open Costlib -open Quandary - -open TOPLlib -open Concurrency -open Labs -open Dotnet)) + -open Topllib -open Concurrency -open Labs -open Dotnet)) (libraries core memtrace IStdlib ATDGenerated IBase IR Absint Biabduction - Nullsafe BO Checkers Costlib Quandary TOPLlib Concurrency Labs Dotnet) + Nullsafe BO Checkers Costlib Quandary Topllib Concurrency Labs Dotnet) (preprocess (pps ppx_compare ppx_fields_conv ppx_yojson_conv))) diff --git a/infer/src/base/Checker.ml b/infer/src/base/Checker.ml index 9aff84f05..d5b06a309 100644 --- a/infer/src/base/Checker.ml +++ b/infer/src/base/Checker.ml @@ -37,7 +37,7 @@ type t = | SIOF | SelfInBlock | Starvation - | TOPL + | Topl | Uninit [@@deriving equal, enumerate] @@ -409,12 +409,14 @@ let config_unsafe checker = ; cli_flags= Some {deprecated= []; show_in_help= true} ; enabled_by_default= true ; activates= [] } - | TOPL -> + | Topl -> { id= "topl" - ; kind= UserFacing {title= "TOPL"; markdown_body= ""} + ; kind= + UserFacing {title= "Topl"; markdown_body= [%blob "../../documentation/checkers/Topl.md"]} ; support= supports_clang_and_java_experimental ; short_documentation= - "Detects errors based on user-provided state machines describing multi-object monitors." + "Detect errors based on user-provided state machines describing temporal properties over \ + multiple objects." ; cli_flags= Some {deprecated= []; show_in_help= true} ; enabled_by_default= false ; activates= [Pulse] } diff --git a/infer/src/base/Checker.mli b/infer/src/base/Checker.mli index 1258183f2..c4ece90dd 100644 --- a/infer/src/base/Checker.mli +++ b/infer/src/base/Checker.mli @@ -36,7 +36,7 @@ type t = | SIOF | SelfInBlock | Starvation - | TOPL + | Topl | Uninit [@@deriving equal, enumerate] diff --git a/infer/src/base/Config.ml b/infer/src/base/Config.ml index fc458d5f4..f6f9982d2 100644 --- a/infer/src/base/Config.ml +++ b/infer/src/base/Config.ml @@ -2500,7 +2500,7 @@ and trace_ondemand = and trace_topl = - CLOpt.mk_bool ~long:"trace-topl" "Detailed tracing information during TOPL analysis" + CLOpt.mk_bool ~long:"trace-topl" "Detailed tracing information during Topl analysis" and tv_commit = diff --git a/infer/src/base/IssueType.ml b/infer/src/base/IssueType.ml index 02fe7007d..a7ef49cb1 100644 --- a/infer/src/base/IssueType.ml +++ b/infer/src/base/IssueType.ml @@ -920,7 +920,10 @@ let complexity_increase ~kind ~is_on_ui_thread = register_cost ~kind ~is_on_ui_thread "%s_COMPLEXITY_INCREASE" -let topl_error = register ~id:"TOPL_ERROR" Error TOPL ~user_documentation:"Experimental." +let topl_error = + register ~id:"TOPL_ERROR" Error Topl + ~user_documentation:"A violation of a Topl property (user-specified)." + let uninitialized_value = register ~id:"UNINITIALIZED_VALUE" Error Uninit diff --git a/infer/src/dune.in b/infer/src/dune.in index 014b2c927..77912c2cd 100644 --- a/infer/src/dune.in +++ b/infer/src/dune.in @@ -99,7 +99,7 @@ let infertop_stanza = (modes byte_complete) (modules Infertop) (flags (:standard -open Core -open IStdlib -open IStd)) - (libraries %s utop Absint ASTLanguage ATDGenerated Backend IBase Biabduction BO Checkers Concurrency Costlib CStubs IR IStdlib Labs Dotnet Nullsafe Pulselib Quandary Integration TestDeterminators TOPLlib UnitTests) + (libraries %s utop Absint ASTLanguage ATDGenerated Backend IBase Biabduction BO Checkers Concurrency Costlib CStubs IR IStdlib Labs Dotnet Nullsafe Pulselib Quandary Integration TestDeterminators Topllib UnitTests) (link_flags (-linkall -warn-error -31)) (preprocess (pps ppx_compare)) (promote (until-clean) (into ../bin)) diff --git a/infer/src/pulse/PulseAbductiveDomain.ml b/infer/src/pulse/PulseAbductiveDomain.ml index 4a80da29b..905cd04cc 100644 --- a/infer/src/pulse/PulseAbductiveDomain.ml +++ b/infer/src/pulse/PulseAbductiveDomain.ml @@ -99,7 +99,7 @@ type t = [@@deriving compare, equal, yojson_of] let pp f {post; pre; topl; path_condition; skipped_calls} = - F.fprintf f "@[%a@;%a@;PRE=[%a]@;skipped_calls=%a@;TOPL=%a@]" PathCondition.pp path_condition + F.fprintf f "@[%a@;%a@;PRE=[%a]@;skipped_calls=%a@;Topl=%a@]" PathCondition.pp path_condition PostDomain.pp post PreDomain.pp pre SkippedCalls.pp skipped_calls PulseTopl.pp_state topl diff --git a/infer/src/pulse/PulseTopl.ml b/infer/src/pulse/PulseTopl.ml index 09bbcdacf..98cd95ff9 100644 --- a/infer/src/pulse/PulseTopl.ml +++ b/infer/src/pulse/PulseTopl.ml @@ -246,7 +246,7 @@ let get env x = | Some v -> v | None -> - L.die InternalError "TOPL: Cannot find %s. Should be caught by static checks" x + L.die InternalError "Topl: Cannot find %s. Should be caught by static checks" x let set = List.Assoc.add ~equal:String.equal @@ -378,7 +378,7 @@ let dummy_tenv = Tenv.create () let is_unsat_expensive path_condition pruned = let _path_condition, unsat, _new_eqs = - (* Not enabling dynamic type reasoning in TOPL for now *) + (* Not enabling dynamic type reasoning in Topl for now *) PathCondition.is_unsat_expensive dummy_tenv ~get_dynamic_type:(fun _ -> None) (Constraint.prune_path pruned path_condition) @@ -614,6 +614,6 @@ let report_errors proc_desc err_log state = let loc = Procdesc.get_loc proc_desc in let ltr = make_trace 0 [] q in let message = Format.asprintf "%a" ToplAutomaton.pp_message_of_state (a, q.post.vertex) in - Reporting.log_issue proc_desc err_log ~loc ~ltr TOPL IssueType.topl_error message + Reporting.log_issue proc_desc err_log ~loc ~ltr Topl IssueType.topl_error message in List.iter ~f:report_simple_state state diff --git a/infer/src/pulse/dune b/infer/src/pulse/dune index 3f3af65fe..1e9e3c9eb 100644 --- a/infer/src/pulse/dune +++ b/infer/src/pulse/dune @@ -8,7 +8,7 @@ (public_name infer.Pulselib) (flags (:standard -open Core -open IR -open IStdlib -open IStd -open ATDGenerated - -open IBase -open Absint -open BO -open TOPLlib -open Nullsafe)) - (libraries core IStdlib ATDGenerated IBase IR Absint BO TOPLlib Nullsafe) + -open IBase -open Absint -open BO -open Topllib -open Nullsafe)) + (libraries core IStdlib ATDGenerated IBase IR Absint BO Topllib Nullsafe) (preprocess (pps ppx_yojson_conv ppx_compare ppx_variants_conv))) diff --git a/infer/src/topl/Topl.ml b/infer/src/topl/Topl.ml index e2f0cd75d..8b14b1b40 100644 --- a/infer/src/topl/Topl.ml +++ b/infer/src/topl/Topl.ml @@ -25,4 +25,4 @@ let properties = lazy (List.concat_map ~f:parse Config.topl_properties) let automaton () = ToplAutomaton.make (Lazy.force properties) -let is_active () = Config.is_checker_enabled TOPL && not (List.is_empty (Lazy.force properties)) +let is_active () = Config.is_checker_enabled Topl && not (List.is_empty (Lazy.force properties)) diff --git a/infer/src/topl/ToplAutomaton.mli b/infer/src/topl/ToplAutomaton.mli index 7a601f42d..4a8b73bf5 100644 --- a/infer/src/topl/ToplAutomaton.mli +++ b/infer/src/topl/ToplAutomaton.mli @@ -7,7 +7,7 @@ open! IStd -(* An automaton is a different representation for a set of TOPL properties: states and transitions +(* An automaton is a different representation for a set of Topl properties: states and transitions are identified by nonnegative integers; and transitions are grouped by their source. Also, the meaning of transition labels does not depend on context (e.g., prefixes are now included). diff --git a/infer/src/topl/dune b/infer/src/topl/dune index 65d998b12..0f1ca015a 100644 --- a/infer/src/topl/dune +++ b/infer/src/topl/dune @@ -10,8 +10,8 @@ (modules ToplParser)) (library - (name TOPLlib) - (public_name infer.TOPLlib) + (name Topllib) + (public_name infer.Topllib) (flags (:standard -open Core -open IR -open IStdlib -open IStd -open ATDGenerated -open IBase -open Absint -open Biabduction)) diff --git a/scripts/toplevel_init b/scripts/toplevel_init index 0350bbde2..593b77963 100644 --- a/scripts/toplevel_init +++ b/scripts/toplevel_init @@ -29,7 +29,7 @@ open Pulselib;; open Checkers;; open Costlib;; open Quandary;; -open TOPLlib;; +open Topllib;; open Concurrency;; open Labs;; open OpenSource;; diff --git a/website/docs/all-issue-types.md b/website/docs/all-issue-types.md index 84e7b3262..9939adb1c 100644 --- a/website/docs/all-issue-types.md +++ b/website/docs/all-issue-types.md @@ -2230,7 +2230,7 @@ These annotations can be found at `com.facebook.infer.annotation.*`. Reported as "Topl Error" by [topl](/docs/next/checker-topl). -Experimental. +A violation of a Topl property (user-specified). ## UNINITIALIZED_VALUE Reported as "Uninitialized Value" by [uninit](/docs/next/checker-uninit). diff --git a/website/docs/checker-topl.md b/website/docs/checker-topl.md index 2a3d62a2c..c777c2c56 100644 --- a/website/docs/checker-topl.md +++ b/website/docs/checker-topl.md @@ -1,9 +1,9 @@ --- -title: "TOPL" -description: "Detects errors based on user-provided state machines describing multi-object monitors." +title: "Topl" +description: "Detect errors based on user-provided state machines describing temporal properties over multiple objects." --- -Detects errors based on user-provided state machines describing multi-object monitors. +Detect errors based on user-provided state machines describing temporal properties over multiple objects. Activate with `--topl`. @@ -12,6 +12,103 @@ Supported languages: - Java: Experimental - C#/.Net: Experimental +# Topl + +## What is it? + +Topl is an analysis framework, built on top of Infer, for statically finding violations of temporal properties. Many analyses can be encoded as temporal properties supported by Topl, such as taint analysis. As a simple example, suppose that we don't want a value returned by method `source()` to be sent as an argument to a method `sink()`. This can be specified as follows: + +``` +property Taint + prefix "Main" + start -> start: * + start -> tracking: source(Ret) => x := Ret + tracking -> error: sink(Arg, VoidRet) when x == Arg +``` + +This specifies an automaton called `Taint` that has three states (`start`, `tracking`, `error`). Two of those states (`start` and `error`) have special meaning; other states (`tracking`) can have any names. The first transition (`start → tracking`) is taken when a method called `source()` is called, and its return value is stored in a register called `x`; the second transition (`tracking → error`) is taken when a method called `sink()` is called, but only if its argument equals what was previously saved in register `x`. +This property is violated in the following Java code: + +``` +public class Main { + static void f() { g(tito(source())); } + static void g(Object x) { h(x); } + static void h(Object x) { sink(x); } + static Object tito(Object x) { return x; } + static Object source() { return "dirty"; } + static void sink(Object x) {} +} +``` + +Note that `source()` and `sink()` are not called from the same method, and that the “dirty” object is passed around a few times before finally reaching the sink. Assuming that the property is in a file `taint.topl` and the Java code in a file `Main.java`, you can invoke Infer with the following command: + +``` +infer --topl --topl-properties taint.topl -- javac Main.java +``` + +It will display the following error: + +``` +Main.java:2: error: Topl Error + property Taint reaches state error. + 1. public class Main { + 2. > static void f() { g(tito(source())); } + 3. static void g(Object x) { h(x); } + 4. static void h(Object x) { sink(x); } +``` + +To get a full trace, use the command + +``` +infer explore +``` + +## Specifying Properties + +A property is a nondeterministic automaton that can remember values in registers. An execution that drives the automaton from the start state to the error state will make Infer report an issue, and the trace that it produces will indicate which parts of the program drive which transitions of the automaton. + +The general form of a property is the following: + +``` +property *Name +* message "Optional error message" // This line can be missing + prefix "Prefix" // There can be zero, one, or more prefix declarations + sourceState -> targetState: *Pattern*(Arg1,...,ArgN,Ret) when *Condition* => *Action* +``` + +The property name and the optional error message are used for reporting issues. The prefix declarations are used to simplify Patterns. The core of the property is the list of transitions. + +Each transition has a source state and a target state. The special transition label * means that the transition is always taken. Typically, there is a transition + +``` + start -> start: * +``` + +meaning that the property can start anywhere, not just at the beginning of a method. + +Otherwise, the label on a transition contains: + +* a *Pattern*, which indicates what kind of instruction in the program drives this transition; +* a list of transition variable bindings (above named Arg1, ..., but any identifier starting with uppercase letters works); +* possibly a boolean Condition, which can refer to transition variables and to registers; +* possibly and Action, which is a list sequence of assignments of the form *register* := *TransitionVariable* (registers do not need to be declared, and any identifier starting with a lowercase letter works). + +There are two types of patterns: + +* a regex that matches method names + * if the regex uses non-letters (such as dots) it must be within double-quotes; otherwise, double quotes are optional + * the prefix declarations are used to add potential prefixes to the regex. The combine regex is essentially “(prefix_regex_a | prefix_regex_b) transition_pattern_regex“ + * for a method with n arguments, there must be n+1 transition variables to get a match. The first n transition variables get bound to the argument values, and the last transition variable gets bound to the return value. *This is true even for the case in which the return type is void*. +* the special keyword **#ArrayWrite**. In that case, there should be two transition variables like “(Array, Index)” — Array gets bound to the array object, and Index gets bound to the index at which the write happens. + +For several examples, see https://github.com/facebook/infer/tree/master/infer/tests/codetoanalyze/java/topl + +## Limitations + +* By design, some problems may be missed. Topl is built on Pulse, which attempts to minimize false positives, at the cost of sometimes having false negatives. +* Analysis time increases exponentially with the number of registers used in properties. + * In theory, there should be no significant slowdown if registers belong to different properties, but the implementation is not yet optimized. + * If there are many registers within the same property, then the slowdown is unavoidable (without some significant breakthrough). However, the maximum number of registers we ever used for one practical property was 3. ## List of Issue Types diff --git a/website/static/man/next/infer-analyze.1.html b/website/static/man/next/infer-analyze.1.html index 3059ff096..fd85729f3 100644 --- a/website/static/man/next/infer-analyze.1.html +++ b/website/static/man/next/infer-analyze.1.html @@ -720,9 +720,9 @@ and disable all other checkers (Conversely:

--topl

-

Activates: checker topl: -Detects errors based on user-provided state machines -describing multi-object monitors. (Conversely: +

Activates: checker topl: Detect +errors based on user-provided state machines describing +temporal properties over multiple objects. (Conversely: --no-topl)

--topl-only

diff --git a/website/static/man/next/infer.1.html b/website/static/man/next/infer.1.html index a985f4fd7..919becb98 100644 --- a/website/static/man/next/infer.1.html +++ b/website/static/man/next/infer.1.html @@ -2176,9 +2176,9 @@ should be considered aliases of @ThreadSafe

infer-analyze(1).
--topl

-

Activates: checker topl: -Detects errors based on user-provided state machines -describing multi-object monitors. (Conversely: +

Activates: checker topl: Detect +errors based on user-provided state machines describing +temporal properties over multiple objects. (Conversely: --no-topl)

See also diff --git a/website/static/odoc/next/infer/IBase/Checker/index.html b/website/static/odoc/next/infer/IBase/Checker/index.html index b2ad7db3d..db0ed01a5 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
| 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 +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__Checker/index.html b/website/static/odoc/next/infer/IBase__Checker/index.html index aa332d53b..5028bf776 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
| 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 +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/IR/Procdesc/index.html b/website/static/odoc/next/infer/IR/Procdesc/index.html index eea1b8e62..e7fa23f11 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 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_ret_param_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__Procdesc/index.html b/website/static/odoc/next/infer/IR__Procdesc/index.html index 3ddc085b6..6426f6962 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 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_ret_param_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/TOPLlib/.dune-keep b/website/static/odoc/next/infer/Topllib/.dune-keep similarity index 100% rename from website/static/odoc/next/infer/TOPLlib/.dune-keep rename to website/static/odoc/next/infer/Topllib/.dune-keep diff --git a/website/static/odoc/next/infer/TOPLlib/Topl/index.html b/website/static/odoc/next/infer/Topllib/Topl/index.html similarity index 81% rename from website/static/odoc/next/infer/TOPLlib/Topl/index.html rename to website/static/odoc/next/infer/Topllib/Topl/index.html index 5bcf21866..4a2ade1ed 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_active : unit -> bool

Return whether PulseTopl is active.

\ 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/ToplAst/index.html b/website/static/odoc/next/infer/Topllib/ToplAst/index.html similarity index 98% rename from website/static/odoc/next/infer/TOPLlib/ToplAst/index.html rename to website/static/odoc/next/infer/Topllib/ToplAst/index.html index 0e86ff35d..3638b54d1 100644 --- a/website/static/odoc/next/infer/TOPLlib/ToplAst/index.html +++ b/website/static/odoc/next/infer/Topllib/ToplAst/index.html @@ -1,2 +1,2 @@ -ToplAst (infer.TOPLlib.ToplAst)

Module TOPLlib.ToplAst

type property_name = string
val compare_property_name : property_name -> property_name -> int
val hash_fold_property_name : Ppx_hash_lib.Std.Hash.state -> property_name -> Ppx_hash_lib.Std.Hash.state
val hash_property_name : property_name -> Ppx_hash_lib.Std.Hash.hash_value
val property_name_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> property_name
val sexp_of_property_name : property_name -> Ppx_sexp_conv_lib.Sexp.t
type register_name = string
val compare_register_name : register_name -> register_name -> int
type variable_name = string
type constant =
| LiteralInt of int
type value =
| Constant of constant
| Register of register_name
| Binding of variable_name
type binop =
| OpEq
| OpNe
| OpGe
| OpGt
| OpLe
| OpLt
type predicate =
| Binop of binop * value * value
| Value of value
type condition = predicate list
type assignment = register_name * variable_name
type procedure_name_pattern = string

a regular expression

type label_pattern =
| ArrayWritePattern
| ProcedureNamePattern of procedure_name_pattern
type label = {
arguments : variable_name list option;
condition : condition;
action : assignment list;
pattern : label_pattern;
}
type vertex = string
val compare_vertex : vertex -> vertex -> int
val hash_fold_vertex : Ppx_hash_lib.Std.Hash.state -> vertex -> Ppx_hash_lib.Std.Hash.state
val hash_vertex : vertex -> Ppx_hash_lib.Std.Hash.hash_value
val vertex_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> vertex
val sexp_of_vertex : vertex -> Ppx_sexp_conv_lib.Sexp.t
type transition = {
source : vertex;
target : vertex;
label : label option;
}
type t = {
name : property_name;
message : string option;
prefixes : string list;
nondet : string list;
transitions : transition list;
}
\ No newline at end of file +ToplAst (infer.Topllib.ToplAst)

Module Topllib.ToplAst

type property_name = string
val compare_property_name : property_name -> property_name -> int
val hash_fold_property_name : Ppx_hash_lib.Std.Hash.state -> property_name -> Ppx_hash_lib.Std.Hash.state
val hash_property_name : property_name -> Ppx_hash_lib.Std.Hash.hash_value
val property_name_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> property_name
val sexp_of_property_name : property_name -> Ppx_sexp_conv_lib.Sexp.t
type register_name = string
val compare_register_name : register_name -> register_name -> int
type variable_name = string
type constant =
| LiteralInt of int
type value =
| Constant of constant
| Register of register_name
| Binding of variable_name
type binop =
| OpEq
| OpNe
| OpGe
| OpGt
| OpLe
| OpLt
type predicate =
| Binop of binop * value * value
| Value of value
type condition = predicate list
type assignment = register_name * variable_name
type procedure_name_pattern = string

a regular expression

type label_pattern =
| ArrayWritePattern
| ProcedureNamePattern of procedure_name_pattern
type label = {
arguments : variable_name list option;
condition : condition;
action : assignment list;
pattern : label_pattern;
}
type vertex = string
val compare_vertex : vertex -> vertex -> int
val hash_fold_vertex : Ppx_hash_lib.Std.Hash.state -> vertex -> Ppx_hash_lib.Std.Hash.state
val hash_vertex : vertex -> Ppx_hash_lib.Std.Hash.hash_value
val vertex_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> vertex
val sexp_of_vertex : vertex -> Ppx_sexp_conv_lib.Sexp.t
type transition = {
source : vertex;
target : vertex;
label : label option;
}
type t = {
name : property_name;
message : string option;
prefixes : string list;
nondet : string list;
transitions : transition list;
}
\ No newline at end of file diff --git a/website/static/odoc/next/infer/TOPLlib/ToplAstOps/index.html b/website/static/odoc/next/infer/Topllib/ToplAstOps/index.html similarity index 80% rename from website/static/odoc/next/infer/TOPLlib/ToplAstOps/index.html rename to website/static/odoc/next/infer/Topllib/ToplAstOps/index.html index a660e3661..078b385e0 100644 --- a/website/static/odoc/next/infer/TOPLlib/ToplAstOps/index.html +++ b/website/static/odoc/next/infer/Topllib/ToplAstOps/index.html @@ -1,2 +1,2 @@ -ToplAstOps (infer.TOPLlib.ToplAstOps)

Module TOPLlib.ToplAstOps

val pp_label : Stdlib.Format.formatter -> ToplAst.label option -> unit
\ No newline at end of file +ToplAstOps (infer.Topllib.ToplAstOps)

Module Topllib.ToplAstOps

val pp_label : Stdlib.Format.formatter -> ToplAst.label option -> unit
\ 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 similarity index 94% rename from website/static/odoc/next/infer/TOPLlib/ToplAutomaton/index.html rename to website/static/odoc/next/infer/Topllib/ToplAutomaton/index.html index 03d7de994..3c4ae66da 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 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 +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/ToplLexer/index.html b/website/static/odoc/next/infer/Topllib/ToplLexer/index.html similarity index 92% rename from website/static/odoc/next/infer/TOPLlib/ToplLexer/index.html rename to website/static/odoc/next/infer/Topllib/ToplLexer/index.html index 74e05374e..b83b85ec8 100644 --- a/website/static/odoc/next/infer/TOPLlib/ToplLexer/index.html +++ b/website/static/odoc/next/infer/Topllib/ToplLexer/index.html @@ -1,2 +1,2 @@ -ToplLexer (infer.TOPLlib.ToplLexer)

Module TOPLlib.ToplLexer

module L = IBase.Logging
val new_line : string -> string -> Stdlib.Lexing.lexbuf -> ToplParser.token
val quoted : Str.regexp
val unquote : string -> string
val __ocaml_lex_tables : IStdlib.IStd.Caml.Lexing.lex_tables
val raw_token : IStdlib.IStd.Caml.Lexing.lexbuf -> ToplParser.token
val __ocaml_lex_raw_token_rec : IStdlib.IStd.Caml.Lexing.lexbuf -> int -> ToplParser.token
val token : unit -> IStdlib.IStd.Caml.Lexing.lexbuf -> ToplParser.token
\ No newline at end of file +ToplLexer (infer.Topllib.ToplLexer)

Module Topllib.ToplLexer

module L = IBase.Logging
val new_line : string -> string -> Stdlib.Lexing.lexbuf -> ToplParser.token
val quoted : Str.regexp
val unquote : string -> string
val __ocaml_lex_tables : IStdlib.IStd.Caml.Lexing.lex_tables
val raw_token : IStdlib.IStd.Caml.Lexing.lexbuf -> ToplParser.token
val __ocaml_lex_raw_token_rec : IStdlib.IStd.Caml.Lexing.lexbuf -> int -> ToplParser.token
val token : unit -> IStdlib.IStd.Caml.Lexing.lexbuf -> ToplParser.token
\ No newline at end of file diff --git a/website/static/odoc/next/infer/TOPLlib/ToplParser/index.html b/website/static/odoc/next/infer/Topllib/ToplParser/index.html similarity index 96% rename from website/static/odoc/next/infer/TOPLlib/ToplParser/index.html rename to website/static/odoc/next/infer/Topllib/ToplParser/index.html index a1b670a3b..63173571e 100644 --- a/website/static/odoc/next/infer/TOPLlib/ToplParser/index.html +++ b/website/static/odoc/next/infer/Topllib/ToplParser/index.html @@ -1,2 +1,2 @@ -ToplParser (infer.TOPLlib.ToplParser)

Module TOPLlib.ToplParser

type token =
| WHEN
| UID of string
| STRING of string
| STAR
| SEMI
| RP
| RC
| PROPERTY
| PREFIX
| NONDET
| NE
| MESSAGE
| LT
| LP
| LID of string
| LE
| LC
| INTEGER of int
| INDENT of int
| GT
| GE
| EQ
| EOF
| COMMA
| COLONEQ
| COLON
| ARROWARROW
| ARROW
| ARRAYWRITE
| AND
exception Error
val properties : (Stdlib.Lexing.lexbuf -> token) -> Stdlib.Lexing.lexbuf -> ToplAst.t list
\ No newline at end of file +ToplParser (infer.Topllib.ToplParser)

Module Topllib.ToplParser

type token =
| WHEN
| UID of string
| STRING of string
| STAR
| SEMI
| RP
| RC
| PROPERTY
| PREFIX
| NONDET
| NE
| MESSAGE
| LT
| LP
| LID of string
| LE
| LC
| INTEGER of int
| INDENT of int
| GT
| GE
| EQ
| EOF
| COMMA
| COLONEQ
| COLON
| ARROWARROW
| ARROW
| ARRAYWRITE
| AND
exception Error
val properties : (Stdlib.Lexing.lexbuf -> token) -> Stdlib.Lexing.lexbuf -> ToplAst.t list
\ 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 similarity index 88% rename from website/static/odoc/next/infer/TOPLlib/index.html rename to website/static/odoc/next/infer/Topllib/index.html index 0a7c49a9c..92ca68c2a 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 ToplParser : 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/.dune-keep b/website/static/odoc/next/infer/Topllib__Topl/.dune-keep similarity index 100% rename from website/static/odoc/next/infer/TOPLlib__Topl/.dune-keep rename to website/static/odoc/next/infer/Topllib__Topl/.dune-keep diff --git a/website/static/odoc/next/infer/TOPLlib__Topl/index.html b/website/static/odoc/next/infer/Topllib__Topl/index.html similarity index 66% rename from website/static/odoc/next/infer/TOPLlib__Topl/index.html rename to website/static/odoc/next/infer/Topllib__Topl/index.html index da4a841e1..050c483a9 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_active : unit -> bool

Return whether PulseTopl is active.

\ 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__ToplAst/.dune-keep b/website/static/odoc/next/infer/Topllib__ToplAst/.dune-keep similarity index 100% rename from website/static/odoc/next/infer/TOPLlib__ToplAst/.dune-keep rename to website/static/odoc/next/infer/Topllib__ToplAst/.dune-keep diff --git a/website/static/odoc/next/infer/TOPLlib__ToplAst/index.html b/website/static/odoc/next/infer/Topllib__ToplAst/index.html similarity index 97% rename from website/static/odoc/next/infer/TOPLlib__ToplAst/index.html rename to website/static/odoc/next/infer/Topllib__ToplAst/index.html index d9b371cac..2149d7ecd 100644 --- a/website/static/odoc/next/infer/TOPLlib__ToplAst/index.html +++ b/website/static/odoc/next/infer/Topllib__ToplAst/index.html @@ -1,2 +1,2 @@ -TOPLlib__ToplAst (infer.TOPLlib__ToplAst)

Module TOPLlib__ToplAst

type property_name = string
val compare_property_name : property_name -> property_name -> int
val hash_fold_property_name : Ppx_hash_lib.Std.Hash.state -> property_name -> Ppx_hash_lib.Std.Hash.state
val hash_property_name : property_name -> Ppx_hash_lib.Std.Hash.hash_value
val property_name_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> property_name
val sexp_of_property_name : property_name -> Ppx_sexp_conv_lib.Sexp.t
type register_name = string
val compare_register_name : register_name -> register_name -> int
type variable_name = string
type constant =
| LiteralInt of int
type value =
| Constant of constant
| Register of register_name
| Binding of variable_name
type binop =
| OpEq
| OpNe
| OpGe
| OpGt
| OpLe
| OpLt
type predicate =
| Binop of binop * value * value
| Value of value
type condition = predicate list
type assignment = register_name * variable_name
type procedure_name_pattern = string

a regular expression

type label_pattern =
| ArrayWritePattern
| ProcedureNamePattern of procedure_name_pattern
type label = {
arguments : variable_name list option;
condition : condition;
action : assignment list;
pattern : label_pattern;
}
type vertex = string
val compare_vertex : vertex -> vertex -> int
val hash_fold_vertex : Ppx_hash_lib.Std.Hash.state -> vertex -> Ppx_hash_lib.Std.Hash.state
val hash_vertex : vertex -> Ppx_hash_lib.Std.Hash.hash_value
val vertex_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> vertex
val sexp_of_vertex : vertex -> Ppx_sexp_conv_lib.Sexp.t
type transition = {
source : vertex;
target : vertex;
label : label option;
}
type t = {
name : property_name;
message : string option;
prefixes : string list;
nondet : string list;
transitions : transition list;
}
\ No newline at end of file +Topllib__ToplAst (infer.Topllib__ToplAst)

Module Topllib__ToplAst

type property_name = string
val compare_property_name : property_name -> property_name -> int
val hash_fold_property_name : Ppx_hash_lib.Std.Hash.state -> property_name -> Ppx_hash_lib.Std.Hash.state
val hash_property_name : property_name -> Ppx_hash_lib.Std.Hash.hash_value
val property_name_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> property_name
val sexp_of_property_name : property_name -> Ppx_sexp_conv_lib.Sexp.t
type register_name = string
val compare_register_name : register_name -> register_name -> int
type variable_name = string
type constant =
| LiteralInt of int
type value =
| Constant of constant
| Register of register_name
| Binding of variable_name
type binop =
| OpEq
| OpNe
| OpGe
| OpGt
| OpLe
| OpLt
type predicate =
| Binop of binop * value * value
| Value of value
type condition = predicate list
type assignment = register_name * variable_name
type procedure_name_pattern = string

a regular expression

type label_pattern =
| ArrayWritePattern
| ProcedureNamePattern of procedure_name_pattern
type label = {
arguments : variable_name list option;
condition : condition;
action : assignment list;
pattern : label_pattern;
}
type vertex = string
val compare_vertex : vertex -> vertex -> int
val hash_fold_vertex : Ppx_hash_lib.Std.Hash.state -> vertex -> Ppx_hash_lib.Std.Hash.state
val hash_vertex : vertex -> Ppx_hash_lib.Std.Hash.hash_value
val vertex_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> vertex
val sexp_of_vertex : vertex -> Ppx_sexp_conv_lib.Sexp.t
type transition = {
source : vertex;
target : vertex;
label : label option;
}
type t = {
name : property_name;
message : string option;
prefixes : string list;
nondet : string list;
transitions : transition list;
}
\ No newline at end of file diff --git a/website/static/odoc/next/infer/TOPLlib__ToplAstOps/.dune-keep b/website/static/odoc/next/infer/Topllib__ToplAstOps/.dune-keep similarity index 100% rename from website/static/odoc/next/infer/TOPLlib__ToplAstOps/.dune-keep rename to website/static/odoc/next/infer/Topllib__ToplAstOps/.dune-keep diff --git a/website/static/odoc/next/infer/TOPLlib__ToplAstOps/index.html b/website/static/odoc/next/infer/Topllib__ToplAstOps/index.html similarity index 61% rename from website/static/odoc/next/infer/TOPLlib__ToplAstOps/index.html rename to website/static/odoc/next/infer/Topllib__ToplAstOps/index.html index 494cc2c88..9816c8e48 100644 --- a/website/static/odoc/next/infer/TOPLlib__ToplAstOps/index.html +++ b/website/static/odoc/next/infer/Topllib__ToplAstOps/index.html @@ -1,2 +1,2 @@ -TOPLlib__ToplAstOps (infer.TOPLlib__ToplAstOps)

Module TOPLlib__ToplAstOps

val pp_label : Stdlib.Format.formatter -> TOPLlib.ToplAst.label option -> unit
\ No newline at end of file +Topllib__ToplAstOps (infer.Topllib__ToplAstOps)

Module Topllib__ToplAstOps

val pp_label : Stdlib.Format.formatter -> Topllib.ToplAst.label option -> unit
\ No newline at end of file diff --git a/website/static/odoc/next/infer/TOPLlib__ToplAutomaton/.dune-keep b/website/static/odoc/next/infer/Topllib__ToplAutomaton/.dune-keep similarity index 100% rename from website/static/odoc/next/infer/TOPLlib__ToplAutomaton/.dune-keep rename to website/static/odoc/next/infer/Topllib__ToplAutomaton/.dune-keep diff --git a/website/static/odoc/next/infer/TOPLlib__ToplAutomaton/index.html b/website/static/odoc/next/infer/Topllib__ToplAutomaton/index.html similarity index 89% rename from website/static/odoc/next/infer/TOPLlib__ToplAutomaton/index.html rename to website/static/odoc/next/infer/Topllib__ToplAutomaton/index.html index 1f02add1b..34e143c56 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 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 +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__ToplLexer/.dune-keep b/website/static/odoc/next/infer/Topllib__ToplLexer/.dune-keep similarity index 100% rename from website/static/odoc/next/infer/TOPLlib__ToplLexer/.dune-keep rename to website/static/odoc/next/infer/Topllib__ToplLexer/.dune-keep diff --git a/website/static/odoc/next/infer/TOPLlib__ToplLexer/index.html b/website/static/odoc/next/infer/Topllib__ToplLexer/index.html similarity index 76% rename from website/static/odoc/next/infer/TOPLlib__ToplLexer/index.html rename to website/static/odoc/next/infer/Topllib__ToplLexer/index.html index e96203445..dd19a513e 100644 --- a/website/static/odoc/next/infer/TOPLlib__ToplLexer/index.html +++ b/website/static/odoc/next/infer/Topllib__ToplLexer/index.html @@ -1,2 +1,2 @@ -TOPLlib__ToplLexer (infer.TOPLlib__ToplLexer)

Module TOPLlib__ToplLexer

module L = IBase.Logging
val new_line : string -> string -> Stdlib.Lexing.lexbuf -> TOPLlib.ToplParser.token
val quoted : Str.regexp
val unquote : string -> string
val __ocaml_lex_tables : IStdlib.IStd.Caml.Lexing.lex_tables
val raw_token : IStdlib.IStd.Caml.Lexing.lexbuf -> TOPLlib.ToplParser.token
val __ocaml_lex_raw_token_rec : IStdlib.IStd.Caml.Lexing.lexbuf -> int -> TOPLlib.ToplParser.token
val token : unit -> IStdlib.IStd.Caml.Lexing.lexbuf -> TOPLlib.ToplParser.token
\ No newline at end of file +Topllib__ToplLexer (infer.Topllib__ToplLexer)

Module Topllib__ToplLexer

module L = IBase.Logging
val new_line : string -> string -> Stdlib.Lexing.lexbuf -> Topllib.ToplParser.token
val quoted : Str.regexp
val unquote : string -> string
val __ocaml_lex_tables : IStdlib.IStd.Caml.Lexing.lex_tables
val raw_token : IStdlib.IStd.Caml.Lexing.lexbuf -> Topllib.ToplParser.token
val __ocaml_lex_raw_token_rec : IStdlib.IStd.Caml.Lexing.lexbuf -> int -> Topllib.ToplParser.token
val token : unit -> IStdlib.IStd.Caml.Lexing.lexbuf -> Topllib.ToplParser.token
\ No newline at end of file diff --git a/website/static/odoc/next/infer/TOPLlib__ToplParser/.dune-keep b/website/static/odoc/next/infer/Topllib__ToplParser/.dune-keep similarity index 100% rename from website/static/odoc/next/infer/TOPLlib__ToplParser/.dune-keep rename to website/static/odoc/next/infer/Topllib__ToplParser/.dune-keep diff --git a/website/static/odoc/next/infer/TOPLlib__ToplParser/index.html b/website/static/odoc/next/infer/Topllib__ToplParser/index.html similarity index 95% rename from website/static/odoc/next/infer/TOPLlib__ToplParser/index.html rename to website/static/odoc/next/infer/Topllib__ToplParser/index.html index b939e5d73..53316c218 100644 --- a/website/static/odoc/next/infer/TOPLlib__ToplParser/index.html +++ b/website/static/odoc/next/infer/Topllib__ToplParser/index.html @@ -1,2 +1,2 @@ -TOPLlib__ToplParser (infer.TOPLlib__ToplParser)

Module TOPLlib__ToplParser

type token =
| WHEN
| UID of string
| STRING of string
| STAR
| SEMI
| RP
| RC
| PROPERTY
| PREFIX
| NONDET
| NE
| MESSAGE
| LT
| LP
| LID of string
| LE
| LC
| INTEGER of int
| INDENT of int
| GT
| GE
| EQ
| EOF
| COMMA
| COLONEQ
| COLON
| ARROWARROW
| ARROW
| ARRAYWRITE
| AND
exception Error
val properties : (Stdlib.Lexing.lexbuf -> token) -> Stdlib.Lexing.lexbuf -> TOPLlib.ToplAst.t list
\ No newline at end of file +Topllib__ToplParser (infer.Topllib__ToplParser)

Module Topllib__ToplParser

type token =
| WHEN
| UID of string
| STRING of string
| STAR
| SEMI
| RP
| RC
| PROPERTY
| PREFIX
| NONDET
| NE
| MESSAGE
| LT
| LP
| LID of string
| LE
| LC
| INTEGER of int
| INDENT of int
| GT
| GE
| EQ
| EOF
| COMMA
| COLONEQ
| COLON
| ARROWARROW
| ARROW
| ARRAYWRITE
| AND
exception Error
val properties : (Stdlib.Lexing.lexbuf -> token) -> Stdlib.Lexing.lexbuf -> Topllib.ToplAst.t list
\ No newline at end of file diff --git a/website/static/odoc/next/infer/index.html b/website/static/odoc/next/infer/index.html index 0d7360b44..2fbc418b5 100644 --- a/website/static/odoc/next/infer/index.html +++ b/website/static/odoc/next/infer/index.html @@ -1,2 +1,2 @@ -index (infer.index)

infer index

Library infer.ASTLanguage

The entry point of this library is the module: ASTLanguage.

Library infer.ATDGenerated

The entry point of this library is the module: ATDGenerated.

Library infer.Absint

The entry point of this library is the module: Absint.

Library infer.BO

The entry point of this library is the module: BO.

Library infer.Backend

The entry point of this library is the module: Backend.

Library infer.Biabduction

The entry point of this library is the module: Biabduction.

Library infer.CStubs

The entry point of this library is the module: CStubs.

Library infer.Checkers

The entry point of this library is the module: Checkers.

Library infer.ClangFrontend

The entry point of this library is the module: ClangFrontend.

Library infer.ClangUnitTests

The entry point of this library is the module: ClangUnitTests.

Library infer.Concurrency

The entry point of this library is the module: Concurrency.

Library infer.Costlib

The entry point of this library is the module: Costlib.

Library infer.Dotnet

The entry point of this library is the module: Dotnet.

Library infer.IBase

The entry point of this library is the module: IBase.

Library infer.IR

The entry point of this library is the module: IR.

Library infer.IStdlib

The entry point of this library is the module: IStdlib.

Library infer.Integration

The entry point of this library is the module: Integration.

Library infer.JavaFrontend

The entry point of this library is the module: JavaFrontend.

Library infer.Labs

The entry point of this library is the module: Labs.

Library infer.Nullsafe

The entry point of this library is the module: Nullsafe.

Library infer.NullsafeUnitTests

The entry point of this library is the module: NullsafeUnitTests.

Library infer.OpenSource

The entry point of this library is the module: OpenSource.

Library infer.Pulselib

The entry point of this library is the module: Pulselib.

Library infer.Quandary

The entry point of this library is the module: Quandary.

Library infer.TOPLlib

The entry point of this library is the module: TOPLlib.

Library infer.TestDeterminators

The entry point of this library is the module: TestDeterminators.

Library infer.UnitTests

The entry point of this library is the module: UnitTests.

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

infer index

Library infer.ASTLanguage

The entry point of this library is the module: ASTLanguage.

Library infer.ATDGenerated

The entry point of this library is the module: ATDGenerated.

Library infer.Absint

The entry point of this library is the module: Absint.

Library infer.BO

The entry point of this library is the module: BO.

Library infer.Backend

The entry point of this library is the module: Backend.

Library infer.Biabduction

The entry point of this library is the module: Biabduction.

Library infer.CStubs

The entry point of this library is the module: CStubs.

Library infer.Checkers

The entry point of this library is the module: Checkers.

Library infer.ClangFrontend

The entry point of this library is the module: ClangFrontend.

Library infer.ClangUnitTests

The entry point of this library is the module: ClangUnitTests.

Library infer.Concurrency

The entry point of this library is the module: Concurrency.

Library infer.Costlib

The entry point of this library is the module: Costlib.

Library infer.Dotnet

The entry point of this library is the module: Dotnet.

Library infer.IBase

The entry point of this library is the module: IBase.

Library infer.IR

The entry point of this library is the module: IR.

Library infer.IStdlib

The entry point of this library is the module: IStdlib.

Library infer.Integration

The entry point of this library is the module: Integration.

Library infer.JavaFrontend

The entry point of this library is the module: JavaFrontend.

Library infer.Labs

The entry point of this library is the module: Labs.

Library infer.Nullsafe

The entry point of this library is the module: Nullsafe.

Library infer.NullsafeUnitTests

The entry point of this library is the module: NullsafeUnitTests.

Library infer.OpenSource

The entry point of this library is the module: OpenSource.

Library infer.Pulselib

The entry point of this library is the module: Pulselib.

Library infer.Quandary

The entry point of this library is the module: Quandary.

Library infer.TestDeterminators

The entry point of this library is the module: TestDeterminators.

Library infer.Topllib

The entry point of this library is the module: Topllib.

Library infer.UnitTests

The entry point of this library is the module: UnitTests.

\ No newline at end of file