From c736015316c24b55f68ebfd62f8b5394e894c8e8 Mon Sep 17 00:00:00 2001
From: Gabriela Cunha Sampaio
Date: Wed, 10 Mar 2021 03:15:03 -0800
Subject: [PATCH] [pulse] Updating Pulse website
Summary: Adding more info to Pulse webpage
Reviewed By: jvillard
Differential Revision: D26884576
fbshipit-source-id: a6f13757f
---
infer/documentation/checkers/Pulse.md | 56 +++++++++
.../issues/NULLPTR_DEREFERENCE.md | 95 ++++++++++++++
.../documentation/issues/NULL_DEREFERENCE.md | 97 ---------------
infer/src/base/Checker.ml | 5 +-
infer/src/base/IssueType.ml | 4 +-
website/docs/all-issue-types.md | 116 ++++++++++++++++--
.../docs/checker-config-impact-analysis.md | 20 +++
website/docs/checker-pulse.md | 58 ++++++++-
website/docs/checker-starvation.md | 1 +
website/static/man/next/infer-report.1.html | 23 ++++
.../static/man/next/infer-reportdiff.1.html | 23 +++-
website/static/man/next/infer.1.html | 38 ++++++
.../Config_impact_data_j/index.html | 2 +
.../Config_impact_data_t/index.html | 2 +
.../infer/ATDGenerated/Jsonbug_j/index.html | 2 +-
.../infer/ATDGenerated/Jsonbug_t/index.html | 2 +-
.../.dune-keep | 0
.../index.html | 2 +
.../.dune-keep | 0
.../index.html | 2 +
.../infer/ATDGenerated__Jsonbug_j/index.html | 2 +-
.../infer/ATDGenerated__Jsonbug_t/index.html | 2 +-
.../ConfigImpactAnalysis/Summary/index.html | 2 +
.../UncheckedCallee/index.html | 2 +
.../UncheckedCallees/index.html | 2 +
.../Checkers/ConfigImpactAnalysis/index.html | 2 +
.../ExternalConfigImpactData/index.html | 2 +
.../Checkers__ConfigImpactAnalysis/.dune-keep | 0
.../Summary/index.html | 2 +
.../UncheckedCallee/index.html | 2 +
.../UncheckedCallees/index.html | 2 +
.../Checkers__ConfigImpactAnalysis/index.html | 2 +
.../.dune-keep | 0
.../index.html | 2 +
.../ClangFrontend/CGeneral_utils/index.html | 2 +-
.../ClangFrontend/CMethodSignature/index.html | 2 +-
.../ClangFrontend__CGeneral_utils/index.html | 2 +-
.../index.html | 2 +-
.../StarvationDomain/Event/index.html | 2 +-
.../Concurrency/StarvationDomain/index.html | 2 +-
.../Concurrency/StarvationModels/index.html | 2 +-
.../Event/index.html | 2 +-
.../Concurrency__StarvationDomain/index.html | 2 +-
.../Concurrency__StarvationModels/index.html | 2 +-
.../odoc/next/infer/IBase/Config/index.html | 2 +-
.../next/infer/IBase/IssueType/index.html | 2 +-
.../IBase/ResultsDirEntryName/index.html | 2 +-
.../odoc/next/infer/IBase__Config/index.html | 2 +-
.../next/infer/IBase__IssueType/index.html | 2 +-
.../IBase__ResultsDirEntryName/index.html | 2 +-
.../next/infer/IR/ProcAttributes/index.html | 2 +-
.../odoc/next/infer/IR/Procdesc/index.html | 2 +-
.../next/infer/IR__ProcAttributes/index.html | 2 +-
.../odoc/next/infer/IR__Procdesc/index.html | 2 +-
.../ConfigImpactIssuesTest/index.html | 2 +
.../infer/Integration/Differential/index.html | 2 +-
.../infer/Integration/ReportDiff/index.html | 2 +-
.../odoc/next/infer/Integration/index.html | 2 +-
.../.dune-keep | 0
.../index.html | 2 +
.../Integration__Differential/index.html | 2 +-
.../infer/Integration__ReportDiff/index.html | 2 +-
.../AddressAttributes/index.html | 2 +-
.../Pulselib/PulseAbductiveDomain/index.html | 2 +-
.../Pulselib/PulseAccessResult/index.html | 2 +
.../PulseAttribute/Attributes/index.html | 2 +-
.../infer/Pulselib/PulseAttribute/index.html | 2 +-
.../PulseBaseAddressAttributes/index.html | 2 +-
.../Pulselib/PulseDomainInterface/index.html | 2 +-
.../Pulselib/PulseExecutionDomain/index.html | 2 +-
.../PulseFormula/DynamicTypes/index.html | 2 +
.../infer/Pulselib/PulseFormula/index.html | 2 +-
.../infer/Pulselib/PulseInterproc/index.html | 2 +-
.../Pulselib/PulseLatentIssue/index.html | 2 +-
.../infer/Pulselib/PulseModels/index.html | 2 +-
.../PulseObjectiveCSummary/index.html | 2 +
.../PulseOperations/Closures/index.html | 2 +-
.../PulseOperations/Import/index.html | 2 +-
.../infer/Pulselib/PulseOperations/index.html | 2 +-
.../Pulselib/PulsePathCondition/index.html | 2 +-
.../infer/Pulselib/PulseReport/index.html | 2 +-
.../infer/Pulselib/PulseSummary/index.html | 2 +-
.../next/infer/Pulselib/PulseTopl/index.html | 2 +-
.../odoc/next/infer/Pulselib/index.html | 2 +-
.../AddressAttributes/index.html | 2 +-
.../Pulselib__PulseAbductiveDomain/index.html | 2 +-
.../Pulselib__PulseAccessResult/.dune-keep | 0
.../Pulselib__PulseAccessResult/index.html | 2 +
.../Attributes/index.html | 2 +-
.../infer/Pulselib__PulseAttribute/index.html | 2 +-
.../index.html | 2 +-
.../Pulselib__PulseDomainInterface/index.html | 2 +-
.../Pulselib__PulseExecutionDomain/index.html | 2 +-
.../DynamicTypes/index.html | 2 +
.../infer/Pulselib__PulseFormula/index.html | 2 +-
.../infer/Pulselib__PulseInterproc/index.html | 2 +-
.../Pulselib__PulseLatentIssue/index.html | 2 +-
.../infer/Pulselib__PulseModels/index.html | 2 +-
.../.dune-keep | 0
.../index.html | 2 +
.../Closures/index.html | 2 +-
.../Import/index.html | 2 +-
.../Pulselib__PulseOperations/index.html | 2 +-
.../Pulselib__PulsePathCondition/index.html | 2 +-
.../infer/Pulselib__PulseReport/index.html | 2 +-
.../infer/Pulselib__PulseSummary/index.html | 2 +-
.../next/infer/Pulselib__PulseTopl/index.html | 2 +-
.../UnitTests/DifferentialTests/index.html | 2 +-
.../UnitTests__DifferentialTests/index.html | 2 +-
109 files changed, 537 insertions(+), 179 deletions(-)
create mode 100644 infer/documentation/checkers/Pulse.md
delete mode 100644 infer/documentation/issues/NULL_DEREFERENCE.md
create mode 100644 website/docs/checker-config-impact-analysis.md
create mode 100644 website/static/odoc/next/infer/ATDGenerated/Config_impact_data_j/index.html
create mode 100644 website/static/odoc/next/infer/ATDGenerated/Config_impact_data_t/index.html
create mode 100644 website/static/odoc/next/infer/ATDGenerated__Config_impact_data_j/.dune-keep
create mode 100644 website/static/odoc/next/infer/ATDGenerated__Config_impact_data_j/index.html
create mode 100644 website/static/odoc/next/infer/ATDGenerated__Config_impact_data_t/.dune-keep
create mode 100644 website/static/odoc/next/infer/ATDGenerated__Config_impact_data_t/index.html
create mode 100644 website/static/odoc/next/infer/Checkers/ConfigImpactAnalysis/Summary/index.html
create mode 100644 website/static/odoc/next/infer/Checkers/ConfigImpactAnalysis/UncheckedCallee/index.html
create mode 100644 website/static/odoc/next/infer/Checkers/ConfigImpactAnalysis/UncheckedCallees/index.html
create mode 100644 website/static/odoc/next/infer/Checkers/ConfigImpactAnalysis/index.html
create mode 100644 website/static/odoc/next/infer/Checkers/ExternalConfigImpactData/index.html
create mode 100644 website/static/odoc/next/infer/Checkers__ConfigImpactAnalysis/.dune-keep
create mode 100644 website/static/odoc/next/infer/Checkers__ConfigImpactAnalysis/Summary/index.html
create mode 100644 website/static/odoc/next/infer/Checkers__ConfigImpactAnalysis/UncheckedCallee/index.html
create mode 100644 website/static/odoc/next/infer/Checkers__ConfigImpactAnalysis/UncheckedCallees/index.html
create mode 100644 website/static/odoc/next/infer/Checkers__ConfigImpactAnalysis/index.html
create mode 100644 website/static/odoc/next/infer/Checkers__ExternalConfigImpactData/.dune-keep
create mode 100644 website/static/odoc/next/infer/Checkers__ExternalConfigImpactData/index.html
create mode 100644 website/static/odoc/next/infer/Integration/ConfigImpactIssuesTest/index.html
create mode 100644 website/static/odoc/next/infer/Integration__ConfigImpactIssuesTest/.dune-keep
create mode 100644 website/static/odoc/next/infer/Integration__ConfigImpactIssuesTest/index.html
create mode 100644 website/static/odoc/next/infer/Pulselib/PulseAccessResult/index.html
create mode 100644 website/static/odoc/next/infer/Pulselib/PulseFormula/DynamicTypes/index.html
create mode 100644 website/static/odoc/next/infer/Pulselib/PulseObjectiveCSummary/index.html
create mode 100644 website/static/odoc/next/infer/Pulselib__PulseAccessResult/.dune-keep
create mode 100644 website/static/odoc/next/infer/Pulselib__PulseAccessResult/index.html
create mode 100644 website/static/odoc/next/infer/Pulselib__PulseFormula/DynamicTypes/index.html
create mode 100644 website/static/odoc/next/infer/Pulselib__PulseObjectiveCSummary/.dune-keep
create mode 100644 website/static/odoc/next/infer/Pulselib__PulseObjectiveCSummary/index.html
diff --git a/infer/documentation/checkers/Pulse.md b/infer/documentation/checkers/Pulse.md
new file mode 100644
index 000000000..d47cc2361
--- /dev/null
+++ b/infer/documentation/checkers/Pulse.md
@@ -0,0 +1,56 @@
+### What is Infer:Pulse?
+Pulse is an interprocedural memory safety analysis. Pulse can detect, for instance, [Null dereferences](/docs/next/all-issue-types#nullptr_dereference) in Java. Errors are only reported when all conditions on the erroneous path are true regardless of input. Pulse should gradually replace the original [biabduction](/docs/next/checker-biabduction) analysis of Infer. An example of a Null dereference found by Pulse is given below.
+
+```java
+class Person {
+ Person emergencyContact;
+ String address;
+
+ Person getEmergencyContact() {
+ return this.emergencyContact;
+ }
+}
+
+class Registry {
+ void create() {
+ Person p = new Person();
+ Person c = p.getEmergencyContact();
+ // Null dereference here
+ System.out.println(c.address);
+ }
+
+ void printContact(Person p) {
+ // No null dereference, as we don't know anything about `p`
+ System.out.println(p.getEmergencyContact().address);
+ }
+}
+```
+
+How to run pulse for Java:
+```bash
+infer run --pulse -- javac Test.java
+```
+
+Pulse reports a Null dereference on this file on `create()`, as it tries to access the field `address` of object `c`, and `c` has value `null`. In contrast, Pulse gives no report for `printContact(Person p)`, as we cannot be sure that `p.getEmergencyContact()` will return `null`. Pulse then labels this error as latent and only reports if there is a call to `printContact(Person p)` satisfying the condition for Null dereference.
+
+### Pulse x Nullsafe
+
+[Nullsafe](/docs/next/checker-eradicate) is a type checker for `@Nullable` annotations for Java. Classes following the Nullsafe discipline are annotated with `@Nullsafe`.
+
+Consider the classes `Person` and `Registry` from the previous example. Assuming that class `Person` is annotated with `@Nullsafe`. In this case, we also annotate `getEmergencyContact()` with `@Nullable`, to make explicit that this method can return the `null` value. There is still the risk that classes depending on `Person` have Null dereferences. In this case, Pulse would report a Null dereference on `Registry`. It could also be the case that class `Registry` is annotated with `@Nullsafe`. By default Pulse reports on `@Nullsafe` files too, see the `--pulse-nullsafe-report-npe` option (Facebook-specific: Pulse does not report on `@Nullsafe` files).
+
+```java
+@Nullsafe(Nullsafe.Mode.LOCAL)
+class Person {
+ Person emergencyContact;
+ String address;
+
+ @Nullable Person getEmergencyContact() {
+ return this.emergencyContact;
+ }
+}
+
+class Registry {
+ ... // Pulse reports here
+}
+```
diff --git a/infer/documentation/issues/NULLPTR_DEREFERENCE.md b/infer/documentation/issues/NULLPTR_DEREFERENCE.md
index 8b1378917..86f984485 100644
--- a/infer/documentation/issues/NULLPTR_DEREFERENCE.md
+++ b/infer/documentation/issues/NULLPTR_DEREFERENCE.md
@@ -1 +1,96 @@
+Infer reports null dereference bugs in Java, C and Objective-C. The issue is
+about a pointer that can be `null` and it is dereferenced. This leads to a crash
+in all the above languages.
+
+### Null dereference in Java
+
+Many of Infer's reports of potential NPE's come from code of the form
+
+```java
+ p = foo(); // foo() might return null
+ stuff();
+ p.goo(); // dereferencing p, potential NPE
+```
+
+If you see code of this form, then you have several options.
+
+ If you are unsure whether or not foo() will return null , you should
+ideally i. Change the code to ensure that foo() can not return null ii. Add a
+check for whether p is null, and do something other than dereferencing p when it
+is null.
+
+Sometimes, in case ii it is not obvious what you should do when p is null. One
+possibility (a last option) is to throw an exception, failing early. This can be
+done using checkNotNull as in the following code:
+
+```java
+ // code idiom for failing early
+
+ import static com.google.common.base.Preconditions.checkNotNull;
+
+ //... intervening code
+
+ p = checkNotNull(foo()); // foo() might return null
+ stuff();
+ p.goo(); // dereferencing p, potential NPE
+```
+
+The call checkNotNull(foo()) will never return null; in case foo() returns null
+it fails early by throwing an NPE.
+
+ If you are absolutely sure that foo() will not be null , then if you
+land your diff this case will no longer be reported after your diff makes it to
+master.
+
+### Null dereference in C
+
+Here is an example of an inter-procedural null dereference bug in C:
+
+```c
+struct Person {
+ int age;
+ int height;
+ int weight;
+};
+int get_age(struct Person *who) {
+ return who->age;
+}
+int null_pointer_interproc() {
+ struct Person *joe = 0;
+ return get_age(joe);
+}
+```
+
+### Null dereference in Objective-C
+
+In Objective-C, null dereferences are less common than in Java, but they still
+happen and their cause can be hidden. In general, passing a message to nil does
+not cause a crash and returns `nil`, but dereferencing a pointer directly does
+cause a crash as well as calling a `nil` block.C
+
+```objectivec
+-(void) foo:(void (^)())callback {
+ callback();
+}
+
+-(void) bar {
+ [self foo:nil]; //crash
+}
+```
+
+Moreover, there are functions from the libraries that do not allow `nil` to be
+passed as argument. Here are some examples:
+
+```objectivec
+-(void) foo {
+ NSString *str = nil;
+ NSArray *animals = @[@"horse", str, @"dolphin"]; //crash
+}
+
+-(void) bar {
+ CGColorSpaceRef colorSpace = CGColorSpaceCreateDeviceRGB(); //can return NULL
+ ...
+ CFRelease(colorSpace); //crashes if called with NULL
+}
+```
diff --git a/infer/documentation/issues/NULL_DEREFERENCE.md b/infer/documentation/issues/NULL_DEREFERENCE.md
deleted file mode 100644
index 4e3eb681a..000000000
--- a/infer/documentation/issues/NULL_DEREFERENCE.md
+++ /dev/null
@@ -1,97 +0,0 @@
-Infer reports null dereference bugs in C, Objective-C and Java. The issue is
-about a pointer that can be `null` and it is dereferenced. This leads to a crash
-in all the above languages.
-
-### Null dereference in C
-
-Here is an example of an inter-procedural null dereference bug in C:
-
-```c
-struct Person {
- int age;
- int height;
- int weight;
-};
-int get_age(struct Person *who) {
- return who->age;
-}
-int null_pointer_interproc() {
- struct Person *joe = 0;
- return get_age(joe);
-}
-```
-
-### Null dereference in Objective-C
-
-In Objective-C, null dereferences are less common than in Java, but they still
-happen and their cause can be hidden. In general, passing a message to nil does
-not cause a crash and returns `nil`, but dereferencing a pointer directly does
-cause a crash as well as calling a `nil` block.C
-
-```objectivec
--(void) foo:(void (^)())callback {
- callback();
-}
-
--(void) bar {
- [self foo:nil]; //crash
-}
-```
-
-Moreover, there are functions from the libraries that do not allow `nil` to be
-passed as argument. Here are some examples:
-
-```objectivec
--(void) foo {
- NSString *str = nil;
- NSArray *animals = @[@"horse", str, @"dolphin"]; //crash
-}
-
--(void) bar {
- CGColorSpaceRef colorSpace = CGColorSpaceCreateDeviceRGB(); //can return NULL
- ...
- CFRelease(colorSpace); //crashes if called with NULL
-}
-```
-
-### Null dereference in Java
-
-Many of Infer's reports of potential NPE's come from code of the form
-
-```java
- p = foo(); // foo() might return null
- stuff();
- p.goo(); // dereferencing p, potential NPE
-```
-
-If you see code of this form, then you have several options.
-
- If you are unsure whether or not foo() will return null , you should
-ideally i. Change the code to ensure that foo() can not return null ii. Add a
-check for whether p is null, and do something other than dereferencing p when it
-is null.
-
-Sometimes, in case ii it is not obvious what you should do when p is null. One
-possibility (a last option) is to throw an exception, failing early. This can be
-done using checkNotNull as in the following code:
-
-```java
- // code idiom for failing early
-
- import static com.google.common.base.Preconditions.checkNotNull;
-
- //... intervening code
-
- p = checkNotNull(foo()); // foo() might return null
- stuff();
- p.goo(); // dereferencing p, potential NPE
-```
-
-The call checkNotNull(foo()) will never return null; in case foo() returns null
-it fails early by throwing an NPE.
-
- If you are absolutely sure that foo() will not be null , then if you
-land your diff this case will no longer be reported after your diff makes it to
-master. In the future we might include analysis directives (hey, analyzer, p is
-not null!) like in Hack that tell the analyzer the information that you know,
-but that is for later.
diff --git a/infer/src/base/Checker.ml b/infer/src/base/Checker.ml
index a5459a1bd..f8769ee39 100644
--- a/infer/src/base/Checker.ml
+++ b/infer/src/base/Checker.ml
@@ -305,8 +305,9 @@ let config_unsafe checker =
; activates= [] }
| Pulse ->
{ id= "pulse"
- ; kind= UserFacing {title= "Pulse"; markdown_body= ""}
- ; support= (function Clang -> Support | Java -> ExperimentalSupport | CIL -> NoSupport)
+ ; kind=
+ UserFacing {title= "Pulse"; markdown_body= [%blob "../../documentation/checkers/Pulse.md"]}
+ ; support= (function Clang | Java -> Support | CIL -> NoSupport)
; short_documentation= "Memory and lifetime analysis."
; cli_flags= Some {deprecated= ["-ownership"]; show_in_help= true}
; enabled_by_default= false
diff --git a/infer/src/base/IssueType.ml b/infer/src/base/IssueType.ml
index 060f7ea6c..863bd0cb8 100644
--- a/infer/src/base/IssueType.ml
+++ b/infer/src/base/IssueType.ml
@@ -791,12 +791,12 @@ let mutable_local_variable_in_component_file =
let null_dereference =
register ~id:"NULL_DEREFERENCE" Error Biabduction
- ~user_documentation:[%blob "../../documentation/issues/NULL_DEREFERENCE.md"]
+ ~user_documentation:[%blob "../../documentation/issues/NULLPTR_DEREFERENCE.md"]
let nullptr_dereference =
register ~id:"NULLPTR_DEREFERENCE" Error Pulse
- ~user_documentation:"See [NULL_DEREFERENCE](#null_dereference)."
+ ~user_documentation:[%blob "../../documentation/issues/NULLPTR_DEREFERENCE.md"]
let optional_empty_access =
diff --git a/website/docs/all-issue-types.md b/website/docs/all-issue-types.md
index d34586962..9ee1f30e1 100644
--- a/website/docs/all-issue-types.md
+++ b/website/docs/all-issue-types.md
@@ -1138,6 +1138,11 @@ void invariant_hoist(int size) {
}
```
+## IPC_ON_UI_THREAD
+
+Reported as "Ipc On Ui Thread" by [starvation](/docs/next/checker-starvation).
+
+A blocking `Binder` IPC call occurs on the UI thread.
## IVAR_NOT_NULL_CHECKED
Reported as "Ivar Not Null Checked" by [biabduction](/docs/next/checker-biabduction).
@@ -1301,15 +1306,51 @@ Reported as "Mutable Local Variable In Component File" by [linters](/docs/next/c
Reported as "Nullptr Dereference" by [pulse](/docs/next/checker-pulse).
-See [NULL_DEREFERENCE](#null_dereference).
-## NULL_DEREFERENCE
-Reported as "Null Dereference" by [biabduction](/docs/next/checker-biabduction).
-
-Infer reports null dereference bugs in C, Objective-C and Java. The issue is
+Infer reports null dereference bugs in Java, C and Objective-C. The issue is
about a pointer that can be `null` and it is dereferenced. This leads to a crash
in all the above languages.
+### Null dereference in Java
+
+Many of Infer's reports of potential NPE's come from code of the form
+
+```java
+ p = foo(); // foo() might return null
+ stuff();
+ p.goo(); // dereferencing p, potential NPE
+```
+
+If you see code of this form, then you have several options.
+
+ If you are unsure whether or not foo() will return null , you should
+ideally i. Change the code to ensure that foo() can not return null ii. Add a
+check for whether p is null, and do something other than dereferencing p when it
+is null.
+
+Sometimes, in case ii it is not obvious what you should do when p is null. One
+possibility (a last option) is to throw an exception, failing early. This can be
+done using checkNotNull as in the following code:
+
+```java
+ // code idiom for failing early
+
+ import static com.google.common.base.Preconditions.checkNotNull;
+
+ //... intervening code
+
+ p = checkNotNull(foo()); // foo() might return null
+ stuff();
+ p.goo(); // dereferencing p, potential NPE
+```
+
+The call checkNotNull(foo()) will never return null; in case foo() returns null
+it fails early by throwing an NPE.
+
+ If you are absolutely sure that foo() will not be null , then if you
+land your diff this case will no longer be reported after your diff makes it to
+master.
+
### Null dereference in C
Here is an example of an inter-procedural null dereference bug in C:
@@ -1362,6 +1403,15 @@ passed as argument. Here are some examples:
}
```
+## NULL_DEREFERENCE
+
+Reported as "Null Dereference" by [biabduction](/docs/next/checker-biabduction).
+
+
+Infer reports null dereference bugs in Java, C and Objective-C. The issue is
+about a pointer that can be `null` and it is dereferenced. This leads to a crash
+in all the above languages.
+
### Null dereference in Java
Many of Infer's reports of potential NPE's come from code of the form
@@ -1400,9 +1450,59 @@ it fails early by throwing an NPE.
If you are absolutely sure that foo() will not be null , then if you
land your diff this case will no longer be reported after your diff makes it to
-master. In the future we might include analysis directives (hey, analyzer, p is
-not null!) like in Hack that tell the analyzer the information that you know,
-but that is for later.
+master.
+
+### Null dereference in C
+
+Here is an example of an inter-procedural null dereference bug in C:
+
+```c
+struct Person {
+ int age;
+ int height;
+ int weight;
+};
+int get_age(struct Person *who) {
+ return who->age;
+}
+int null_pointer_interproc() {
+ struct Person *joe = 0;
+ return get_age(joe);
+}
+```
+
+### Null dereference in Objective-C
+
+In Objective-C, null dereferences are less common than in Java, but they still
+happen and their cause can be hidden. In general, passing a message to nil does
+not cause a crash and returns `nil`, but dereferencing a pointer directly does
+cause a crash as well as calling a `nil` block.C
+
+```objectivec
+-(void) foo:(void (^)())callback {
+ callback();
+}
+
+-(void) bar {
+ [self foo:nil]; //crash
+}
+```
+
+Moreover, there are functions from the libraries that do not allow `nil` to be
+passed as argument. Here are some examples:
+
+```objectivec
+-(void) foo {
+ NSString *str = nil;
+ NSArray *animals = @[@"horse", str, @"dolphin"]; //crash
+}
+
+-(void) bar {
+ CGColorSpaceRef colorSpace = CGColorSpaceCreateDeviceRGB(); //can return NULL
+ ...
+ CFRelease(colorSpace); //crashes if called with NULL
+}
+```
## OPTIONAL_EMPTY_ACCESS
diff --git a/website/docs/checker-config-impact-analysis.md b/website/docs/checker-config-impact-analysis.md
new file mode 100644
index 000000000..51a2e49c3
--- /dev/null
+++ b/website/docs/checker-config-impact-analysis.md
@@ -0,0 +1,20 @@
+---
+title: "Config Impact Analysis"
+description: "[EXPERIMENTAL] Collects function that are called without config checks."
+---
+
+[EXPERIMENTAL] Collects function that are called without config checks.
+
+Activate with `--config-impact-analysis`.
+
+Supported languages:
+- C/C++/ObjC: Experimental
+- Java: Experimental
+- C#/.Net: Experimental
+
+This checker collects functions whose execution isn't gated by certain pre-defined gating functions. The set of gating functions is hardcoded and empty by default for now, so to use this checker, please modify the code directly in [FbGKInteraction.ml](https://github.com/facebook/infer/tree/master/infer/src/opensource).
+
+## List of Issue Types
+
+The following issue types are reported by this checker:
+- [CONFIG_IMPACT](/docs/next/all-issue-types#config_impact)
diff --git a/website/docs/checker-pulse.md b/website/docs/checker-pulse.md
index 67ef73d43..0c31efb99 100644
--- a/website/docs/checker-pulse.md
+++ b/website/docs/checker-pulse.md
@@ -9,9 +9,65 @@ Activate with `--pulse`.
Supported languages:
- C/C++/ObjC: Yes
-- Java: Experimental
+- Java: Yes
- C#/.Net: No
+### What is Infer:Pulse?
+Pulse is an interprocedural memory safety analysis. Pulse can detect, for instance, [Null dereferences](/docs/next/all-issue-types#nullptr_dereference) in Java. Errors are only reported when all conditions on the erroneous path are true regardless of input. Pulse should gradually replace the original [biabduction](/docs/next/checker-biabduction) analysis of Infer. An example of a Null dereference found by Pulse is given below.
+
+```java
+class Person {
+ Person emergencyContact;
+ String address;
+
+ Person getEmergencyContact() {
+ return this.emergencyContact;
+ }
+}
+
+class Registry {
+ void create() {
+ Person p = new Person();
+ Person c = p.getEmergencyContact();
+ // Null dereference here
+ System.out.println(c.address);
+ }
+
+ void printContact(Person p) {
+ // No null dereference, as we don't know anything about `p`
+ System.out.println(p.getEmergencyContact().address);
+ }
+}
+```
+
+How to run pulse for Java:
+```bash
+infer run --pulse -- javac Test.java
+```
+
+Pulse reports a Null dereference on this file on `create()`, as it tries to access the field `address` of object `c`, and `c` has value `null`. In contrast, Pulse gives no report for `printContact(Person p)`, as we cannot be sure that `p.getEmergencyContact()` will return `null`. Pulse then labels this error as latent and only reports if there is a call to `printContact(Person p)` satisfying the condition for Null dereference.
+
+### Pulse x Nullsafe
+
+[Nullsafe](/docs/next/checker-eradicate) is a type checker for `@Nullable` annotations for Java. Classes following the Nullsafe discipline are annotated with `@Nullsafe`.
+
+Consider the classes `Person` and `Registry` from the previous example. Assuming that class `Person` is annotated with `@Nullsafe`. In this case, we also annotate `getEmergencyContact()` with `@Nullable`, to make explicit that this method can return the `null` value. There is still the risk that classes depending on `Person` have Null dereferences. In this case, Pulse would report a Null dereference on `Registry`. It could also be the case that class `Registry` is annotated with `@Nullsafe`. By default Pulse reports on `@Nullsafe` files too, see the `--pulse-nullsafe-report-npe` option (Facebook-specific: Pulse does not report on `@Nullsafe` files).
+
+```java
+@Nullsafe(Nullsafe.Mode.LOCAL)
+class Person {
+ Person emergencyContact;
+ String address;
+
+ @Nullable Person getEmergencyContact() {
+ return this.emergencyContact;
+ }
+}
+
+class Registry {
+ ... // Pulse reports here
+}
+```
## List of Issue Types
diff --git a/website/docs/checker-starvation.md b/website/docs/checker-starvation.md
index 6f88cc6b5..4295b276c 100644
--- a/website/docs/checker-starvation.md
+++ b/website/docs/checker-starvation.md
@@ -24,6 +24,7 @@ Detect several kinds of "starvation" problems:
The following issue types are reported by this checker:
- [ARBITRARY_CODE_EXECUTION_UNDER_LOCK](/docs/next/all-issue-types#arbitrary_code_execution_under_lock)
- [DEADLOCK](/docs/next/all-issue-types#deadlock)
+- [IPC_ON_UI_THREAD](/docs/next/all-issue-types#ipc_on_ui_thread)
- [LOCKLESS_VIOLATION](/docs/next/all-issue-types#lockless_violation)
- [STARVATION](/docs/next/all-issue-types#starvation)
- [STRICT_MODE_VIOLATION](/docs/next/all-issue-types#strict_mode_violation)
diff --git a/website/static/man/next/infer-report.1.html b/website/static/man/next/infer-report.1.html
index c05aecd2e..41613ae9f 100644
--- a/website/static/man/next/infer-report.1.html
+++ b/website/static/man/next/infer-report.1.html
@@ -94,6 +94,21 @@ used to explain why the issue was filtered.
[ConfigImpact] Specify the file
containing the config data
+
+
--config-impact-issues-tests
+file
+
+
Write a list of config impact
+issues in a format suitable for config impact tests to
+file
+
+
+
--config-impact-max-callees-to-print
+int
+
+
Specify the maximum number of
+unchecked callees to print in the config impact checker
+
--cost-issues-testsfile
@@ -301,6 +316,7 @@ INTEGER_OVERFLOW_L5 (disabled by default),
INTEGER_OVERFLOW_U5 (disabled by default),
INTERFACE_NOT_THREAD_SAFE (enabled by default),
INVARIANT_CALL (disabled by default),
+IPC_ON_UI_THREAD (enabled by default),
IVAR_NOT_NULL_CHECKED (enabled by default),
Internal_error (enabled by default),
JAVASCRIPT_INJECTION (enabled by default),
@@ -386,6 +402,13 @@ experimental and blacklisted issue types (Conversely:
--filtering | -f)
+
Load costs analysis results
+from a config-impact-report file.
+
+
--from-json-costs-reportcosts-report.json
diff --git a/website/static/man/next/infer-reportdiff.1.html b/website/static/man/next/infer-reportdiff.1.html
index ab1eb3c5a..c4c434bdb 100644
--- a/website/static/man/next/infer-reportdiff.1.html
+++ b/website/static/man/next/infer-reportdiff.1.html
@@ -69,7 +69,28 @@ follow the same format as normal infer reports.
-
--cost-tests-only-autoreleasepool
+
--config-impact-current
+path
+
+
Config impact report of the
+latest revision
+
+
+
--config-impact-max-callees-to-print
+int
+
+
Specify the maximum number of
+unchecked callees to print in the config impact checker
+
+
+
--config-impact-previous
+path
+
+
Config impact report of the
+base revision to use for comparison
+
+
+
--cost-tests-only-autoreleasepool
Activates: [EXPERIMENTAL]
Report only autoreleasepool size results in cost tests
diff --git a/website/static/man/next/infer.1.html b/website/static/man/next/infer.1.html
index 01bdc65f4..9c7582ee7 100644
--- a/website/static/man/next/infer.1.html
+++ b/website/static/man/next/infer.1.html
@@ -472,6 +472,13 @@ config-impact-analysis and disable all other checkers
See also
infer-analyze(1).
+--config-impact-currentpath
+
+
Config impact report of the
+latest revision
+
+
See also
+infer-reportdiff(1).
--config-impact-data-filefile
[ConfigImpact] Specify the file
@@ -479,6 +486,28 @@ containing the config data
See also
infer-report(1).
+--config-impact-issues-testsfile
+
+
Write a list of config impact
+issues in a format suitable for config impact tests to
+file
+
+
See also
+infer-report(1).
+--config-impact-max-callees-to-printint
+
+
Specify the maximum number of
+unchecked callees to print in the config impact checker
+
+
See also infer-report(1)
+and infer-reportdiff(1).
+--config-impact-previouspath
+
+
Config impact report of the
+base revision to use for comparison
+
+
See also
+infer-reportdiff(1).
--continue
Activates: Continue the capture
@@ -828,6 +857,7 @@ INTEGER_OVERFLOW_L5 (disabled by default),
INTEGER_OVERFLOW_U5 (disabled by default),
INTERFACE_NOT_THREAD_SAFE (enabled by default),
INVARIANT_CALL (disabled by default),
+IPC_ON_UI_THREAD (enabled by default),
IVAR_NOT_NULL_CHECKED (enabled by default),
Internal_error (enabled by default),
JAVASCRIPT_INJECTION (enabled by default),
@@ -1006,6 +1036,14 @@ fragment-retains-view and disable all other checkers
See also
infer-analyze(1).
+--from-json-config-impact-report
+config-impact-report.json
+
+
Load costs analysis results
+from a config-impact-report file.
+
+
See also
+infer-report(1).
--from-json-costs-reportcosts-report.json
\ No newline at end of file
diff --git a/website/static/odoc/next/infer/ATDGenerated/Config_impact_data_t/index.html b/website/static/odoc/next/infer/ATDGenerated/Config_impact_data_t/index.html
new file mode 100644
index 000000000..42d674c0f
--- /dev/null
+++ b/website/static/odoc/next/infer/ATDGenerated/Config_impact_data_t/index.html
@@ -0,0 +1,2 @@
+
+Config_impact_data_t (infer.ATDGenerated.Config_impact_data_t)
\ No newline at end of file
diff --git a/website/static/odoc/next/infer/ATDGenerated/Jsonbug_j/index.html b/website/static/odoc/next/infer/ATDGenerated/Jsonbug_j/index.html
index 8cb193fcb..e51ea313f 100644
--- a/website/static/odoc/next/infer/ATDGenerated/Jsonbug_j/index.html
+++ b/website/static/odoc/next/infer/ATDGenerated/Jsonbug_j/index.html
@@ -1,2 +1,2 @@
-Jsonbug_j (infer.ATDGenerated.Jsonbug_j)
\ No newline at end of file
diff --git a/website/static/odoc/next/infer/ATDGenerated/Jsonbug_t/index.html b/website/static/odoc/next/infer/ATDGenerated/Jsonbug_t/index.html
index 9fca0c32c..647a10f12 100644
--- a/website/static/odoc/next/infer/ATDGenerated/Jsonbug_t/index.html
+++ b/website/static/odoc/next/infer/ATDGenerated/Jsonbug_t/index.html
@@ -1,2 +1,2 @@
-Jsonbug_t (infer.ATDGenerated.Jsonbug_t)
\ No newline at end of file
diff --git a/website/static/odoc/next/infer/ATDGenerated__Config_impact_data_j/.dune-keep b/website/static/odoc/next/infer/ATDGenerated__Config_impact_data_j/.dune-keep
new file mode 100644
index 000000000..e69de29bb
diff --git a/website/static/odoc/next/infer/ATDGenerated__Config_impact_data_j/index.html b/website/static/odoc/next/infer/ATDGenerated__Config_impact_data_j/index.html
new file mode 100644
index 000000000..46ffda1ee
--- /dev/null
+++ b/website/static/odoc/next/infer/ATDGenerated__Config_impact_data_j/index.html
@@ -0,0 +1,2 @@
+
+ATDGenerated__Config_impact_data_j (infer.ATDGenerated__Config_impact_data_j)
\ No newline at end of file
diff --git a/website/static/odoc/next/infer/ATDGenerated__Config_impact_data_t/.dune-keep b/website/static/odoc/next/infer/ATDGenerated__Config_impact_data_t/.dune-keep
new file mode 100644
index 000000000..e69de29bb
diff --git a/website/static/odoc/next/infer/ATDGenerated__Config_impact_data_t/index.html b/website/static/odoc/next/infer/ATDGenerated__Config_impact_data_t/index.html
new file mode 100644
index 000000000..114892ef4
--- /dev/null
+++ b/website/static/odoc/next/infer/ATDGenerated__Config_impact_data_t/index.html
@@ -0,0 +1,2 @@
+
+ATDGenerated__Config_impact_data_t (infer.ATDGenerated__Config_impact_data_t)
\ No newline at end of file
diff --git a/website/static/odoc/next/infer/ATDGenerated__Jsonbug_j/index.html b/website/static/odoc/next/infer/ATDGenerated__Jsonbug_j/index.html
index 814378912..ed8c26193 100644
--- a/website/static/odoc/next/infer/ATDGenerated__Jsonbug_j/index.html
+++ b/website/static/odoc/next/infer/ATDGenerated__Jsonbug_j/index.html
@@ -1,2 +1,2 @@
-ATDGenerated__Jsonbug_j (infer.ATDGenerated__Jsonbug_j)
\ No newline at end of file
diff --git a/website/static/odoc/next/infer/ATDGenerated__Jsonbug_t/index.html b/website/static/odoc/next/infer/ATDGenerated__Jsonbug_t/index.html
index ebd25f078..64bc1363f 100644
--- a/website/static/odoc/next/infer/ATDGenerated__Jsonbug_t/index.html
+++ b/website/static/odoc/next/infer/ATDGenerated__Jsonbug_t/index.html
@@ -1,2 +1,2 @@
-ATDGenerated__Jsonbug_t (infer.ATDGenerated__Jsonbug_t)
\ No newline at end of file
diff --git a/website/static/odoc/next/infer/Checkers/ConfigImpactAnalysis/Summary/index.html b/website/static/odoc/next/infer/Checkers/ConfigImpactAnalysis/Summary/index.html
new file mode 100644
index 000000000..0dc6db09b
--- /dev/null
+++ b/website/static/odoc/next/infer/Checkers/ConfigImpactAnalysis/Summary/index.html
@@ -0,0 +1,2 @@
+
+Summary (infer.Checkers.ConfigImpactAnalysis.Summary)
\ No newline at end of file
diff --git a/website/static/odoc/next/infer/Checkers/ConfigImpactAnalysis/UncheckedCallee/index.html b/website/static/odoc/next/infer/Checkers/ConfigImpactAnalysis/UncheckedCallee/index.html
new file mode 100644
index 000000000..35d39e5e9
--- /dev/null
+++ b/website/static/odoc/next/infer/Checkers/ConfigImpactAnalysis/UncheckedCallee/index.html
@@ -0,0 +1,2 @@
+
+UncheckedCallee (infer.Checkers.ConfigImpactAnalysis.UncheckedCallee)
val pp_without_location_list : Stdlib.Format.formatter ->t list-> unit
\ No newline at end of file
diff --git a/website/static/odoc/next/infer/Checkers/ConfigImpactAnalysis/UncheckedCallees/index.html b/website/static/odoc/next/infer/Checkers/ConfigImpactAnalysis/UncheckedCallees/index.html
new file mode 100644
index 000000000..9f3646b76
--- /dev/null
+++ b/website/static/odoc/next/infer/Checkers/ConfigImpactAnalysis/UncheckedCallees/index.html
@@ -0,0 +1,2 @@
+
+UncheckedCallees (infer.Checkers.ConfigImpactAnalysis.UncheckedCallees)
val pp_without_location : Stdlib.Format.formatter ->t-> unit
\ No newline at end of file
diff --git a/website/static/odoc/next/infer/Checkers/ConfigImpactAnalysis/index.html b/website/static/odoc/next/infer/Checkers/ConfigImpactAnalysis/index.html
new file mode 100644
index 000000000..e4a4acb8d
--- /dev/null
+++ b/website/static/odoc/next/infer/Checkers/ConfigImpactAnalysis/index.html
@@ -0,0 +1,2 @@
+
+ConfigImpactAnalysis (infer.Checkers.ConfigImpactAnalysis)
\ No newline at end of file
diff --git a/website/static/odoc/next/infer/Checkers/ExternalConfigImpactData/index.html b/website/static/odoc/next/infer/Checkers/ExternalConfigImpactData/index.html
new file mode 100644
index 000000000..d5be7457f
--- /dev/null
+++ b/website/static/odoc/next/infer/Checkers/ExternalConfigImpactData/index.html
@@ -0,0 +1,2 @@
+
+ExternalConfigImpactData (infer.Checkers.ExternalConfigImpactData)
\ No newline at end of file
diff --git a/website/static/odoc/next/infer/Checkers__ConfigImpactAnalysis/.dune-keep b/website/static/odoc/next/infer/Checkers__ConfigImpactAnalysis/.dune-keep
new file mode 100644
index 000000000..e69de29bb
diff --git a/website/static/odoc/next/infer/Checkers__ConfigImpactAnalysis/Summary/index.html b/website/static/odoc/next/infer/Checkers__ConfigImpactAnalysis/Summary/index.html
new file mode 100644
index 000000000..e76d0de3d
--- /dev/null
+++ b/website/static/odoc/next/infer/Checkers__ConfigImpactAnalysis/Summary/index.html
@@ -0,0 +1,2 @@
+
+Summary (infer.Checkers__ConfigImpactAnalysis.Summary)
\ No newline at end of file
diff --git a/website/static/odoc/next/infer/Checkers__ConfigImpactAnalysis/UncheckedCallee/index.html b/website/static/odoc/next/infer/Checkers__ConfigImpactAnalysis/UncheckedCallee/index.html
new file mode 100644
index 000000000..8e02e3f2f
--- /dev/null
+++ b/website/static/odoc/next/infer/Checkers__ConfigImpactAnalysis/UncheckedCallee/index.html
@@ -0,0 +1,2 @@
+
+UncheckedCallee (infer.Checkers__ConfigImpactAnalysis.UncheckedCallee)
val pp_without_location_list : Stdlib.Format.formatter ->t list-> unit
\ No newline at end of file
diff --git a/website/static/odoc/next/infer/Checkers__ConfigImpactAnalysis/UncheckedCallees/index.html b/website/static/odoc/next/infer/Checkers__ConfigImpactAnalysis/UncheckedCallees/index.html
new file mode 100644
index 000000000..416d6adf6
--- /dev/null
+++ b/website/static/odoc/next/infer/Checkers__ConfigImpactAnalysis/UncheckedCallees/index.html
@@ -0,0 +1,2 @@
+
+UncheckedCallees (infer.Checkers__ConfigImpactAnalysis.UncheckedCallees)
val pp_without_location : Stdlib.Format.formatter ->t-> unit
\ No newline at end of file
diff --git a/website/static/odoc/next/infer/Checkers__ConfigImpactAnalysis/index.html b/website/static/odoc/next/infer/Checkers__ConfigImpactAnalysis/index.html
new file mode 100644
index 000000000..719a379b4
--- /dev/null
+++ b/website/static/odoc/next/infer/Checkers__ConfigImpactAnalysis/index.html
@@ -0,0 +1,2 @@
+
+Checkers__ConfigImpactAnalysis (infer.Checkers__ConfigImpactAnalysis)
\ No newline at end of file
diff --git a/website/static/odoc/next/infer/Checkers__ExternalConfigImpactData/.dune-keep b/website/static/odoc/next/infer/Checkers__ExternalConfigImpactData/.dune-keep
new file mode 100644
index 000000000..e69de29bb
diff --git a/website/static/odoc/next/infer/Checkers__ExternalConfigImpactData/index.html b/website/static/odoc/next/infer/Checkers__ExternalConfigImpactData/index.html
new file mode 100644
index 000000000..f2780f4e1
--- /dev/null
+++ b/website/static/odoc/next/infer/Checkers__ExternalConfigImpactData/index.html
@@ -0,0 +1,2 @@
+
+Checkers__ExternalConfigImpactData (infer.Checkers__ExternalConfigImpactData)
\ No newline at end of file
diff --git a/website/static/odoc/next/infer/ClangFrontend/CGeneral_utils/index.html b/website/static/odoc/next/infer/ClangFrontend/CGeneral_utils/index.html
index fa840b918..86e3b2fd9 100644
--- a/website/static/odoc/next/infer/ClangFrontend/CGeneral_utils/index.html
+++ b/website/static/odoc/next/infer/ClangFrontend/CGeneral_utils/index.html
@@ -1,2 +1,2 @@
-CGeneral_utils (infer.ClangFrontend.CGeneral_utils)
\ No newline at end of file
diff --git a/website/static/odoc/next/infer/ClangFrontend/CMethodSignature/index.html b/website/static/odoc/next/infer/ClangFrontend/CMethodSignature/index.html
index 53a8a7ccb..74f826e66 100644
--- a/website/static/odoc/next/infer/ClangFrontend/CMethodSignature/index.html
+++ b/website/static/odoc/next/infer/ClangFrontend/CMethodSignature/index.html
@@ -1,2 +1,2 @@
-CMethodSignature (infer.ClangFrontend.CMethodSignature)
\ No newline at end of file
diff --git a/website/static/odoc/next/infer/ClangFrontend__CGeneral_utils/index.html b/website/static/odoc/next/infer/ClangFrontend__CGeneral_utils/index.html
index f36483cba..41d621624 100644
--- a/website/static/odoc/next/infer/ClangFrontend__CGeneral_utils/index.html
+++ b/website/static/odoc/next/infer/ClangFrontend__CGeneral_utils/index.html
@@ -1,2 +1,2 @@
-ClangFrontend__CGeneral_utils (infer.ClangFrontend__CGeneral_utils)
\ No newline at end of file
diff --git a/website/static/odoc/next/infer/ClangFrontend__CMethodSignature/index.html b/website/static/odoc/next/infer/ClangFrontend__CMethodSignature/index.html
index 9f0c93977..bde4f72cc 100644
--- a/website/static/odoc/next/infer/ClangFrontend__CMethodSignature/index.html
+++ b/website/static/odoc/next/infer/ClangFrontend__CMethodSignature/index.html
@@ -1,2 +1,2 @@
-ClangFrontend__CMethodSignature (infer.ClangFrontend__CMethodSignature)
\ No newline at end of file
diff --git a/website/static/odoc/next/infer/Concurrency/StarvationDomain/Event/index.html b/website/static/odoc/next/infer/Concurrency/StarvationDomain/Event/index.html
index 41a442560..54ce4ce07 100644
--- a/website/static/odoc/next/infer/Concurrency/StarvationDomain/Event/index.html
+++ b/website/static/odoc/next/infer/Concurrency/StarvationDomain/Event/index.html
@@ -1,2 +1,2 @@
-Event (infer.Concurrency.StarvationDomain.Event)
\ No newline at end of file
diff --git a/website/static/odoc/next/infer/Concurrency/StarvationDomain/index.html b/website/static/odoc/next/infer/Concurrency/StarvationDomain/index.html
index d9de8b1bd..55b650224 100644
--- a/website/static/odoc/next/infer/Concurrency/StarvationDomain/index.html
+++ b/website/static/odoc/next/infer/Concurrency/StarvationDomain/index.html
@@ -1,2 +1,2 @@
-StarvationDomain (infer.Concurrency.StarvationDomain)
A CriticalPairElement equipped with a call stack. The intuition is that if we have a critical pair `(locks, event)` in the summary of a method then there is a trace of that method where `event` occurs, and right before it occurs the locks held are exactly `locks` (no over/under approximation). We call it "critical" because the information here alone determines deadlock conditions.
A CriticalPairElement equipped with a call stack. The intuition is that if we have a critical pair `(locks, event)` in the summary of a method then there is a trace of that method where `event` occurs, and right before it occurs the locks held are exactly `locks` (no over/under approximation). We call it "critical" because the information here alone determines deadlock conditions.
\ No newline at end of file
diff --git a/website/static/odoc/next/infer/Concurrency/StarvationModels/index.html b/website/static/odoc/next/infer/Concurrency/StarvationModels/index.html
index 345c1cf44..da7dc69cb 100644
--- a/website/static/odoc/next/infer/Concurrency/StarvationModels/index.html
+++ b/website/static/odoc/next/infer/Concurrency/StarvationModels/index.html
@@ -1,2 +1,2 @@
-StarvationModels (infer.Concurrency.StarvationModels)
given an executor receiver, get its thread constraint, if any. None means lookup somehow failed, whereas Some UnknownThread means the receiver is an unannotated executor.
given an executor receiver, get its thread constraint, if any. None means lookup somehow failed, whereas Some UnknownThread means the receiver is an unannotated executor.
for example com.google.common.util.concurrent.SettableFuture.set
\ No newline at end of file
diff --git a/website/static/odoc/next/infer/Concurrency__StarvationDomain/Event/index.html b/website/static/odoc/next/infer/Concurrency__StarvationDomain/Event/index.html
index e22ed1323..a8d76eb7c 100644
--- a/website/static/odoc/next/infer/Concurrency__StarvationDomain/Event/index.html
+++ b/website/static/odoc/next/infer/Concurrency__StarvationDomain/Event/index.html
@@ -1,2 +1,2 @@
-Event (infer.Concurrency__StarvationDomain.Event)
\ No newline at end of file
diff --git a/website/static/odoc/next/infer/Concurrency__StarvationDomain/index.html b/website/static/odoc/next/infer/Concurrency__StarvationDomain/index.html
index b0699a77c..040bfcaa2 100644
--- a/website/static/odoc/next/infer/Concurrency__StarvationDomain/index.html
+++ b/website/static/odoc/next/infer/Concurrency__StarvationDomain/index.html
@@ -1,2 +1,2 @@
-Concurrency__StarvationDomain (infer.Concurrency__StarvationDomain)
A CriticalPairElement equipped with a call stack. The intuition is that if we have a critical pair `(locks, event)` in the summary of a method then there is a trace of that method where `event` occurs, and right before it occurs the locks held are exactly `locks` (no over/under approximation). We call it "critical" because the information here alone determines deadlock conditions.
A CriticalPairElement equipped with a call stack. The intuition is that if we have a critical pair `(locks, event)` in the summary of a method then there is a trace of that method where `event` occurs, and right before it occurs the locks held are exactly `locks` (no over/under approximation). We call it "critical" because the information here alone determines deadlock conditions.
\ No newline at end of file
diff --git a/website/static/odoc/next/infer/Concurrency__StarvationModels/index.html b/website/static/odoc/next/infer/Concurrency__StarvationModels/index.html
index a7ae456e5..42fa44a2a 100644
--- a/website/static/odoc/next/infer/Concurrency__StarvationModels/index.html
+++ b/website/static/odoc/next/infer/Concurrency__StarvationModels/index.html
@@ -1,2 +1,2 @@
-Concurrency__StarvationModels (infer.Concurrency__StarvationModels)
given an executor receiver, get its thread constraint, if any. None means lookup somehow failed, whereas Some UnknownThread means the receiver is an unannotated executor.
given an executor receiver, get its thread constraint, if any. None means lookup somehow failed, whereas Some UnknownThread means the receiver is an unannotated executor.
for example com.google.common.util.concurrent.SettableFuture.set
\ 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 4696d2a85..d5bf5f502 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)
val scuba_normals : string IStdlib.IStd.String.Map.t
val scuba_tags : string listIStdlib.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)
val scuba_normals : string IStdlib.IStd.String.Map.t
val scuba_tags : string listIStdlib.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
diff --git a/website/static/odoc/next/infer/IBase/IssueType/index.html b/website/static/odoc/next/infer/IBase/IssueType/index.html
index ad45c51fb..48a94a7aa 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)
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.
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.
\ No newline at end of file
diff --git a/website/static/odoc/next/infer/IBase/ResultsDirEntryName/index.html b/website/static/odoc/next/infer/IBase/ResultsDirEntryName/index.html
index 31fc391db..045a917f3 100644
--- a/website/static/odoc/next/infer/IBase/ResultsDirEntryName/index.html
+++ b/website/static/odoc/next/infer/IBase/ResultsDirEntryName/index.html
@@ -1,2 +1,2 @@
-ResultsDirEntryName (infer.IBase.ResultsDirEntryName)
Module IBase.ResultsDirEntryName
type id =
| AllocationTraces
directory for storing allocation traces
| CaptureDB
the capture database
| CaptureDependencies
list of infer-out/ directories that contain capture artefacts
| ChangedFunctions
results of the clang test determinator
| Debug
directory containing debug data
| Differential
contains the results of infer reportdiff
| DuplicateFunctions
list of duplicated functions
| JavaClassnamesCache
used when capturing Java jar dependencies
| JavaGlobalTypeEnvironment
internal Tenv.t object corresponding to the whole project
| LintDotty
directory of linters' dotty debug output for CTL evaluation
| LintIssues
directory of linters' issues
| Logs
log file
| NullsafeFileIssues
file-wide issues of the nullsafe analysis
| PerfEvents
file containing events for performance profiling
| ProcnamesLocks
directory of per-Procname.t file locks, used by the analysis scheduler in certain modes
| RacerDIssues
directory of issues reported by the RacerD analysis
| ReportConfigImpactJson
reports of the config impact analysis
| ReportCostsJson
reports of the costs analysis
| ReportHtml
directory of the HTML report
| ReportJson
the main product of the analysis: report.json
| ReportText
a human-readable textual version of report.json
| ReportXML
a PMD-style XML version of report.json
| RetainCycles
directory of retain cycles dotty files
| RunState
internal data about the last infer run
| StarvationIssues
directory of issues reported by the starvation analysis
| Temporary
directory containing temp files
| TestDeterminatorReport
the report produced by the test determinator capture mode
sad that we have to have this here but some code path is looking for all files with that name in buck-out/
\ 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 bf23c6cf3..ea1bc8bf5 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)
val scuba_normals : string IStdlib.IStd.String.Map.t
val scuba_tags : string listIStdlib.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)
val scuba_normals : string IStdlib.IStd.String.Map.t
val scuba_tags : string listIStdlib.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
diff --git a/website/static/odoc/next/infer/IBase__IssueType/index.html b/website/static/odoc/next/infer/IBase__IssueType/index.html
index eda0b1049..f0143d6fa 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)
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.
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.
\ No newline at end of file
diff --git a/website/static/odoc/next/infer/IBase__ResultsDirEntryName/index.html b/website/static/odoc/next/infer/IBase__ResultsDirEntryName/index.html
index 213663e89..e0163d531 100644
--- a/website/static/odoc/next/infer/IBase__ResultsDirEntryName/index.html
+++ b/website/static/odoc/next/infer/IBase__ResultsDirEntryName/index.html
@@ -1,2 +1,2 @@
-IBase__ResultsDirEntryName (infer.IBase__ResultsDirEntryName)
Module IBase__ResultsDirEntryName
type id =
| AllocationTraces
directory for storing allocation traces
| CaptureDB
the capture database
| CaptureDependencies
list of infer-out/ directories that contain capture artefacts
| ChangedFunctions
results of the clang test determinator
| Debug
directory containing debug data
| Differential
contains the results of infer reportdiff
| DuplicateFunctions
list of duplicated functions
| JavaClassnamesCache
used when capturing Java jar dependencies
| JavaGlobalTypeEnvironment
internal Tenv.t object corresponding to the whole project
| LintDotty
directory of linters' dotty debug output for CTL evaluation
| LintIssues
directory of linters' issues
| Logs
log file
| NullsafeFileIssues
file-wide issues of the nullsafe analysis
| PerfEvents
file containing events for performance profiling
| ProcnamesLocks
directory of per-Procname.t file locks, used by the analysis scheduler in certain modes
| RacerDIssues
directory of issues reported by the RacerD analysis
| ReportConfigImpactJson
reports of the config impact analysis
| ReportCostsJson
reports of the costs analysis
| ReportHtml
directory of the HTML report
| ReportJson
the main product of the analysis: report.json
| ReportText
a human-readable textual version of report.json
| ReportXML
a PMD-style XML version of report.json
| RetainCycles
directory of retain cycles dotty files
| RunState
internal data about the last infer run
| StarvationIssues
directory of issues reported by the starvation analysis
| Temporary
directory containing temp files
| TestDeterminatorReport
the report produced by the test determinator capture mode
all the entries that correspond to directories containing temporary issue logs for certain analyses
val to_delete_before_incremental_capture_and_analysis : results_dir:string->string list
utility for ResultsDir.scrub_for_incremental, you probably want to use that instead
val to_delete_before_caching_capture : results_dir:string->string list
utility for ResultsDir.scrub_for_caching, you probably want to use that instead
val buck_infer_deps_file_name : string
sad that we have to have this here but some code path is looking for all files with that name in buck-out/
\ No newline at end of file
diff --git a/website/static/odoc/next/infer/IR/ProcAttributes/index.html b/website/static/odoc/next/infer/IR/ProcAttributes/index.html
index df0cf1cc5..5779fbb4a 100644
--- a/website/static/odoc/next/infer/IR/ProcAttributes/index.html
+++ b/website/static/odoc/next/infer/IR/ProcAttributes/index.html
@@ -1,2 +1,2 @@
-ProcAttributes (infer.IR.ProcAttributes)
the procedure is a clone specialized with calls to concrete closures, with link to the original procedure, and a map that links the original formals to the elements of the closure used to specialize the procedure.
the procedure is a clone specialized with calls to concrete closures, with link to the original procedure, and a map that links the original formals to the elements of the closure used to specialize the procedure.
\ 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 38d82308a..c6b025d98 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)
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.
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.
\ No newline at end of file
diff --git a/website/static/odoc/next/infer/IR__ProcAttributes/index.html b/website/static/odoc/next/infer/IR__ProcAttributes/index.html
index f892bcf2c..9aabe257b 100644
--- a/website/static/odoc/next/infer/IR__ProcAttributes/index.html
+++ b/website/static/odoc/next/infer/IR__ProcAttributes/index.html
@@ -1,2 +1,2 @@
-IR__ProcAttributes (infer.IR__ProcAttributes)
the procedure is a clone specialized with calls to concrete closures, with link to the original procedure, and a map that links the original formals to the elements of the closure used to specialize the procedure.
the procedure is a clone specialized with calls to concrete closures, with link to the original procedure, and a map that links the original formals to the elements of the closure used to specialize the procedure.
\ 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 eda270729..9f704646e 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)
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.
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.
\ No newline at end of file
diff --git a/website/static/odoc/next/infer/Integration/ConfigImpactIssuesTest/index.html b/website/static/odoc/next/infer/Integration/ConfigImpactIssuesTest/index.html
new file mode 100644
index 000000000..5df2ab246
--- /dev/null
+++ b/website/static/odoc/next/infer/Integration/ConfigImpactIssuesTest/index.html
@@ -0,0 +1,2 @@
+
+ConfigImpactIssuesTest (infer.Integration.ConfigImpactIssuesTest)
Module Integration.ConfigImpactIssuesTest
val write_from_json : json_path:string->out_path:string-> unit
\ No newline at end of file
diff --git a/website/static/odoc/next/infer/Integration/Differential/index.html b/website/static/odoc/next/infer/Integration/Differential/index.html
index 6c8c16cc9..11c236b2b 100644
--- a/website/static/odoc/next/infer/Integration/Differential/index.html
+++ b/website/static/odoc/next/infer/Integration/Differential/index.html
@@ -1,2 +1,2 @@
-Differential (infer.Integration.Differential)
\ No newline at end of file
diff --git a/website/static/odoc/next/infer/Integration/ReportDiff/index.html b/website/static/odoc/next/infer/Integration/ReportDiff/index.html
index 46578ff33..84c5bacae 100644
--- a/website/static/odoc/next/infer/Integration/ReportDiff/index.html
+++ b/website/static/odoc/next/infer/Integration/ReportDiff/index.html
@@ -1,2 +1,2 @@
-ReportDiff (infer.Integration.ReportDiff)
Module Integration.ReportDiff
val reportdiff : current_report:string option->previous_report:string option->current_costs:string option->previous_costs:string option-> unit
\ No newline at end of file
+ReportDiff (infer.Integration.ReportDiff)
Module Integration.ReportDiff
val reportdiff : current_report:string option->previous_report:string option->current_costs:string option->previous_costs:string option->current_config_impact:string option->previous_config_impact:string option-> unit
\ No newline at end of file
diff --git a/website/static/odoc/next/infer/Integration/index.html b/website/static/odoc/next/infer/Integration/index.html
index 4b43cab2f..b84de8d9f 100644
--- a/website/static/odoc/next/infer/Integration/index.html
+++ b/website/static/odoc/next/infer/Integration/index.html
@@ -1,2 +1,2 @@
-Integration (infer.Integration)
\ No newline at end of file
diff --git a/website/static/odoc/next/infer/Integration__ConfigImpactIssuesTest/.dune-keep b/website/static/odoc/next/infer/Integration__ConfigImpactIssuesTest/.dune-keep
new file mode 100644
index 000000000..e69de29bb
diff --git a/website/static/odoc/next/infer/Integration__ConfigImpactIssuesTest/index.html b/website/static/odoc/next/infer/Integration__ConfigImpactIssuesTest/index.html
new file mode 100644
index 000000000..e4785ab5e
--- /dev/null
+++ b/website/static/odoc/next/infer/Integration__ConfigImpactIssuesTest/index.html
@@ -0,0 +1,2 @@
+
+Integration__ConfigImpactIssuesTest (infer.Integration__ConfigImpactIssuesTest)
Module Integration__ConfigImpactIssuesTest
val write_from_json : json_path:string->out_path:string-> unit
\ No newline at end of file
diff --git a/website/static/odoc/next/infer/Integration__Differential/index.html b/website/static/odoc/next/infer/Integration__Differential/index.html
index 4cabbfa55..64face1a6 100644
--- a/website/static/odoc/next/infer/Integration__Differential/index.html
+++ b/website/static/odoc/next/infer/Integration__Differential/index.html
@@ -1,2 +1,2 @@
-Integration__Differential (infer.Integration__Differential)
\ No newline at end of file
diff --git a/website/static/odoc/next/infer/Integration__ReportDiff/index.html b/website/static/odoc/next/infer/Integration__ReportDiff/index.html
index 663ff6d68..78aaa2b3c 100644
--- a/website/static/odoc/next/infer/Integration__ReportDiff/index.html
+++ b/website/static/odoc/next/infer/Integration__ReportDiff/index.html
@@ -1,2 +1,2 @@
-Integration__ReportDiff (infer.Integration__ReportDiff)
Module Integration__ReportDiff
val reportdiff : current_report:string option->previous_report:string option->current_costs:string option->previous_costs:string option-> unit
\ No newline at end of file
+Integration__ReportDiff (infer.Integration__ReportDiff)
Module Integration__ReportDiff
val reportdiff : current_report:string option->previous_report:string option->current_costs:string option->previous_costs:string option->current_config_impact:string option->previous_config_impact:string option-> unit
\ No newline at end of file
diff --git a/website/static/odoc/next/infer/Pulselib/PulseAbductiveDomain/AddressAttributes/index.html b/website/static/odoc/next/infer/Pulselib/PulseAbductiveDomain/AddressAttributes/index.html
index 35f8b8e12..15251f952 100644
--- a/website/static/odoc/next/infer/Pulselib/PulseAbductiveDomain/AddressAttributes/index.html
+++ b/website/static/odoc/next/infer/Pulselib/PulseAbductiveDomain/AddressAttributes/index.html
@@ -1,2 +1,2 @@
-AddressAttributes (infer.Pulselib.PulseAbductiveDomain.AddressAttributes)
Module PulseAbductiveDomain.AddressAttributes
attribute operations like BaseAddressAttributes but that also take care of propagating facts to the precondition
\ No newline at end of file
diff --git a/website/static/odoc/next/infer/Pulselib/PulseAbductiveDomain/index.html b/website/static/odoc/next/infer/Pulselib/PulseAbductiveDomain/index.html
index 06bf01f09..e046eaea6 100644
--- a/website/static/odoc/next/infer/Pulselib/PulseAbductiveDomain/index.html
+++ b/website/static/odoc/next/infer/Pulselib/PulseAbductiveDomain/index.html
@@ -1,2 +1,2 @@
-PulseAbductiveDomain (infer.Pulselib.PulseAbductiveDomain)
signature common to the "normal" Domain, representing the post at the current program point, and the inverted PreDomain, representing the inferred pre-condition
The inferred pre-condition at each program point, biabduction style.
type isl_status =
| ISLOk
ok triple: the program executes without error
| ISLError
Error specification: an invalid address recorded in the precondition will cause an error
Execution status, similar to PulseExecutionDomain but for ISL (Incorrectness Separation Logic) mode, where PulseExecutionDomain.base_t.ContinueProgram can also contain "error specs" that describe what happens when some addresses are invalid explicitly instead of relying on MustBeValid attributes.
garbage collect unreachable addresses in the state to make it smaller and return the new state, the live addresses, and the discarded addresses that used to have attributes attached
Check that the new equalities discovered are compatible with the current pre and post heaps, e.g. x = 0 is not compatible with x being allocated, and x = y is not compatible with x and y being allocated separately. In those cases, the resulting path condition is PathCondition.false_.
signature common to the "normal" Domain, representing the post at the current program point, and the inverted PreDomain, representing the inferred pre-condition
garbage collect unreachable addresses in the state to make it smaller and return the new state, the live addresses, and the discarded addresses that used to have attributes attached
Check that the new equalities discovered are compatible with the current pre and post heaps, e.g. x = 0 is not compatible with x being allocated, and x = y is not compatible with x and y being allocated separately. In those cases, the resulting path condition is PathCondition.false_.
\ No newline at end of file
diff --git a/website/static/odoc/next/infer/Pulselib/PulseAccessResult/index.html b/website/static/odoc/next/infer/Pulselib/PulseAccessResult/index.html
new file mode 100644
index 000000000..5c152a3df
--- /dev/null
+++ b/website/static/odoc/next/infer/Pulselib/PulseAccessResult/index.html
@@ -0,0 +1,2 @@
+
+PulseAccessResult (infer.Pulselib.PulseAccessResult)
\ No newline at end of file
diff --git a/website/static/odoc/next/infer/Pulselib/PulseAttribute/Attributes/index.html b/website/static/odoc/next/infer/Pulselib/PulseAttribute/Attributes/index.html
index 2b690a0d2..c219c8d5a 100644
--- a/website/static/odoc/next/infer/Pulselib/PulseAttribute/Attributes/index.html
+++ b/website/static/odoc/next/infer/Pulselib/PulseAttribute/Attributes/index.html
@@ -1,2 +1,2 @@
-Attributes (infer.Pulselib.PulseAttribute.Attributes)
While applying a spec, replacing ISLAbduced by Allocated and Invalidation.Cfree by Invalidation.delete, if applicable
\ No newline at end of file
diff --git a/website/static/odoc/next/infer/Pulselib/PulseAttribute/index.html b/website/static/odoc/next/infer/Pulselib/PulseAttribute/index.html
index 23b8400b5..e9fd7c160 100644
--- a/website/static/odoc/next/infer/Pulselib/PulseAttribute/index.html
+++ b/website/static/odoc/next/infer/Pulselib/PulseAttribute/index.html
@@ -1,2 +1,2 @@
-PulseAttribute (infer.Pulselib.PulseAttribute)
\ No newline at end of file
diff --git a/website/static/odoc/next/infer/Pulselib/PulseBaseAddressAttributes/index.html b/website/static/odoc/next/infer/Pulselib/PulseBaseAddressAttributes/index.html
index d29a3965e..1edf066e0 100644
--- a/website/static/odoc/next/infer/Pulselib/PulseBaseAddressAttributes/index.html
+++ b/website/static/odoc/next/infer/Pulselib/PulseBaseAddressAttributes/index.html
@@ -1,2 +1,2 @@
-PulseBaseAddressAttributes (infer.Pulselib.PulseBaseAddressAttributes)
merge the attributes of all the variables that are equal according to get_var_repr and remove non-canonical variables in favor of their rerpresentative
merge the attributes of all the variables that are equal according to get_var_repr and remove non-canonical variables in favor of their rerpresentative
\ No newline at end of file
diff --git a/website/static/odoc/next/infer/Pulselib/PulseDomainInterface/index.html b/website/static/odoc/next/infer/Pulselib/PulseDomainInterface/index.html
index 23200e425..47991d8d2 100644
--- a/website/static/odoc/next/infer/Pulselib/PulseDomainInterface/index.html
+++ b/website/static/odoc/next/infer/Pulselib/PulseDomainInterface/index.html
@@ -1,2 +1,2 @@
-PulseDomainInterface (infer.Pulselib.PulseDomainInterface)
\ No newline at end of file
diff --git a/website/static/odoc/next/infer/Pulselib/PulseExecutionDomain/index.html b/website/static/odoc/next/infer/Pulselib/PulseExecutionDomain/index.html
index afc38cef0..6d768c6f6 100644
--- a/website/static/odoc/next/infer/Pulselib/PulseExecutionDomain/index.html
+++ b/website/static/odoc/next/infer/Pulselib/PulseExecutionDomain/index.html
@@ -1,2 +1,2 @@
-PulseExecutionDomain (infer.Pulselib.PulseExecutionDomain)
\ No newline at end of file
diff --git a/website/static/odoc/next/infer/Pulselib/PulseFormula/DynamicTypes/index.html b/website/static/odoc/next/infer/Pulselib/PulseFormula/DynamicTypes/index.html
new file mode 100644
index 000000000..5ca62e86b
--- /dev/null
+++ b/website/static/odoc/next/infer/Pulselib/PulseFormula/DynamicTypes/index.html
@@ -0,0 +1,2 @@
+
+DynamicTypes (infer.Pulselib.PulseFormula.DynamicTypes)
Simplifies IsInstanceOf(var, typ) predicate when dynamic type information is available in state. *
\ 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 7c0e6082a..b1751ae59 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)
\ No newline at end of file
diff --git a/website/static/odoc/next/infer/Pulselib/PulseInterproc/index.html b/website/static/odoc/next/infer/Pulselib/PulseInterproc/index.html
index 52e8248ac..3c1344ae1 100644
--- a/website/static/odoc/next/infer/Pulselib/PulseInterproc/index.html
+++ b/website/static/odoc/next/infer/Pulselib/PulseInterproc/index.html
@@ -1,2 +1,2 @@
-PulseInterproc (infer.Pulselib.PulseInterproc)
\ No newline at end of file
diff --git a/website/static/odoc/next/infer/Pulselib/PulseLatentIssue/index.html b/website/static/odoc/next/infer/Pulselib/PulseLatentIssue/index.html
index ee5a0a440..5f47e9aa6 100644
--- a/website/static/odoc/next/infer/Pulselib/PulseLatentIssue/index.html
+++ b/website/static/odoc/next/infer/Pulselib/PulseLatentIssue/index.html
@@ -1,2 +1,2 @@
-PulseLatentIssue (infer.Pulselib.PulseLatentIssue)
\ No newline at end of file
diff --git a/website/static/odoc/next/infer/Pulselib/PulseModels/index.html b/website/static/odoc/next/infer/Pulselib/PulseModels/index.html
index 919182a25..93b1574c0 100644
--- a/website/static/odoc/next/infer/Pulselib/PulseModels/index.html
+++ b/website/static/odoc/next/infer/Pulselib/PulseModels/index.html
@@ -1,2 +1,2 @@
-PulseModels (infer.Pulselib.PulseModels)
\ No newline at end of file
diff --git a/website/static/odoc/next/infer/Pulselib/PulseObjectiveCSummary/index.html b/website/static/odoc/next/infer/Pulselib/PulseObjectiveCSummary/index.html
new file mode 100644
index 000000000..3af085be4
--- /dev/null
+++ b/website/static/odoc/next/infer/Pulselib/PulseObjectiveCSummary/index.html
@@ -0,0 +1,2 @@
+
+PulseObjectiveCSummary (infer.Pulselib.PulseObjectiveCSummary)
For ObjC instance methods: adds path condition `self > 0` to given posts and appends additional nil summary. Does nothing to posts for other kinds of methods
\ No newline at end of file
diff --git a/website/static/odoc/next/infer/Pulselib/PulseOperations/Closures/index.html b/website/static/odoc/next/infer/Pulselib/PulseOperations/Closures/index.html
index 16eb155ba..459221cd5 100644
--- a/website/static/odoc/next/infer/Pulselib/PulseOperations/Closures/index.html
+++ b/website/static/odoc/next/infer/Pulselib/PulseOperations/Closures/index.html
@@ -1,2 +1,2 @@
-Closures (infer.Pulselib.PulseOperations.Closures)
assert the validity of the addresses captured by the lambda
\ No newline at end of file
diff --git a/website/static/odoc/next/infer/Pulselib/PulseOperations/Import/index.html b/website/static/odoc/next/infer/Pulselib/PulseOperations/Import/index.html
index 7a939ea38..fc07431b7 100644
--- a/website/static/odoc/next/infer/Pulselib/PulseOperations/Import/index.html
+++ b/website/static/odoc/next/infer/Pulselib/PulseOperations/Import/index.html
@@ -1,2 +1,2 @@
-Import (infer.Pulselib.PulseOperations.Import)
Module PulseOperations.Import
For opening in other modules.
type access_mode =
| Read
| Write
| NoAccess
The initialized-ness of the address is not checked when it evaluates a heap address without actual memory access, for example, when evaluating &x.f we need to check initialized-ness of x, not that of x.f.
Imported types for ease of use and so we can write variants without the corresponding module prefix
monadic "bind" but not really that turns an access_result into a list of access_results (not really because the first type is not an access_result list but just an access_result)
monadic "map" but even less really that turns an access_result into an analysis result
\ No newline at end of file
+Import (infer.Pulselib.PulseOperations.Import)
Module PulseOperations.Import
For opening in other modules.
type access_mode =
| Read
| Write
| NoAccess
The initialized-ness of the address is not checked when it evaluates a heap address without actual memory access, for example, when evaluating &x.f we need to check initialized-ness of x, not that of x.f.
Imported types for ease of use and so we can write variants without the corresponding module prefix
monadic "bind" but not really that turns an AccessResult.t into a list of AccessResult.ts (not really because the first type is not an AccessResult.t list but just an AccessResult.t)
monadic "map" but even less really that turns an AccessResult.t into an analysis result
\ No newline at end of file
diff --git a/website/static/odoc/next/infer/Pulselib/PulseOperations/index.html b/website/static/odoc/next/infer/Pulselib/PulseOperations/index.html
index 400574a60..3c87172f8 100644
--- a/website/static/odoc/next/infer/Pulselib/PulseOperations/index.html
+++ b/website/static/odoc/next/infer/Pulselib/PulseOperations/index.html
@@ -1,2 +1,2 @@
-PulseOperations (infer.Pulselib.PulseOperations)
The initialized-ness of the address is not checked when it evaluates a heap address without actual memory access, for example, when evaluating &x.f we need to check initialized-ness of x, not that of x.f.
Imported types for ease of use and so we can write variants without the corresponding module prefix
monadic "bind" but not really that turns an access_result into a list of access_results (not really because the first type is not an access_result list but just an access_result)
Similar to eval but apply to data structures and ISL abduction. Return a list of abduced states (ISLOk and ISLErs); The boolean indicates whether it is data structures or not.
Given a list of variables, computes the unreachable values if the variables were removed from the stack, then return the dynamic types of those values if they are available
The initialized-ness of the address is not checked when it evaluates a heap address without actual memory access, for example, when evaluating &x.f we need to check initialized-ness of x, not that of x.f.
Imported types for ease of use and so we can write variants without the corresponding module prefix
monadic "bind" but not really that turns an AccessResult.t into a list of AccessResult.ts (not really because the first type is not an AccessResult.t list but just an AccessResult.t)
Similar to eval but apply to data structures and ISL abduction. Return a list of abduced states (ISLOk and ISLErs); The boolean indicates whether it is data structures or not.
Given a list of variables, computes the unreachable values if the variables were removed from the stack, then return the dynamic types of those values if they are available
\ 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 453dfebbc..8549f8434 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)
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/PulseReport/index.html b/website/static/odoc/next/infer/Pulselib/PulseReport/index.html
index afae6f73b..ff7596abd 100644
--- a/website/static/odoc/next/infer/Pulselib/PulseReport/index.html
+++ b/website/static/odoc/next/infer/Pulselib/PulseReport/index.html
@@ -1,2 +1,2 @@
-PulseReport (infer.Pulselib.PulseReport)
\ No newline at end of file
diff --git a/website/static/odoc/next/infer/Pulselib/PulseSummary/index.html b/website/static/odoc/next/infer/Pulselib/PulseSummary/index.html
index 649196d84..309c9f709 100644
--- a/website/static/odoc/next/infer/Pulselib/PulseSummary/index.html
+++ b/website/static/odoc/next/infer/Pulselib/PulseSummary/index.html
@@ -1,2 +1,2 @@
-PulseSummary (infer.Pulselib.PulseSummary)
\ No newline at end of file
diff --git a/website/static/odoc/next/infer/Pulselib/PulseTopl/index.html b/website/static/odoc/next/infer/Pulselib/PulseTopl/index.html
index 05b66ad3c..2972e6c67 100644
--- a/website/static/odoc/next/infer/Pulselib/PulseTopl/index.html
+++ b/website/static/odoc/next/infer/Pulselib/PulseTopl/index.html
@@ -1,2 +1,2 @@
-PulseTopl (infer.Pulselib.PulseTopl)
large_step ~substitution ~condition state ~callee_prepost updates state according to callee_prepost. The abstract values in condition and state are in one scope, and those in callee_prepost in another scope: the substitution maps from the callee scope to the condition&state scope.
Remove from state those parts that are inconsistent with the path condition. (We do a cheap check to not introduce inconsistent Topl states, but they mey become inconsistent because the program path condition is updated later.)
large_step ~substitution ~condition state ~callee_prepost updates state according to callee_prepost. The abstract values in condition and state are in one scope, and those in callee_prepost in another scope: the substitution maps from the callee scope to the condition&state scope.
Remove from state those parts that are inconsistent with the path condition. (We do a cheap check to not introduce inconsistent Topl states, but they mey become inconsistent because the program path condition is updated later.)
Calls Reporting.log_issue with error traces, if any.
val pp_state : Stdlib.Format.formatter ->state-> unit
\ 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 dc25e2bea..aeda48eba 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)
\ No newline at end of file
diff --git a/website/static/odoc/next/infer/Pulselib__PulseAbductiveDomain/AddressAttributes/index.html b/website/static/odoc/next/infer/Pulselib__PulseAbductiveDomain/AddressAttributes/index.html
index 43c9b4cb9..6da1cbb48 100644
--- a/website/static/odoc/next/infer/Pulselib__PulseAbductiveDomain/AddressAttributes/index.html
+++ b/website/static/odoc/next/infer/Pulselib__PulseAbductiveDomain/AddressAttributes/index.html
@@ -1,2 +1,2 @@
-AddressAttributes (infer.Pulselib__PulseAbductiveDomain.AddressAttributes)
\ No newline at end of file
diff --git a/website/static/odoc/next/infer/Pulselib__PulseAbductiveDomain/index.html b/website/static/odoc/next/infer/Pulselib__PulseAbductiveDomain/index.html
index acadba488..eb2d6a04e 100644
--- a/website/static/odoc/next/infer/Pulselib__PulseAbductiveDomain/index.html
+++ b/website/static/odoc/next/infer/Pulselib__PulseAbductiveDomain/index.html
@@ -1,2 +1,2 @@
-Pulselib__PulseAbductiveDomain (infer.Pulselib__PulseAbductiveDomain)
signature common to the "normal" Domain, representing the post at the current program point, and the inverted PreDomain, representing the inferred pre-condition
The inferred pre-condition at each program point, biabduction style.
type isl_status =
| ISLOk
ok triple: the program executes without error
| ISLError
Error specification: an invalid address recorded in the precondition will cause an error
Execution status, similar to PulseExecutionDomain but for ISL (Incorrectness Separation Logic) mode, where PulseExecutionDomain.ContinueProgram can also contain "error specs" that describe what happens when some addresses are invalid explicitly instead of relying on MustBeValid attributes.
garbage collect unreachable addresses in the state to make it smaller and return the new state, the live addresses, and the discarded addresses that used to have attributes attached
Check that the new equalities discovered are compatible with the current pre and post heaps, e.g. x = 0 is not compatible with x being allocated, and x = y is not compatible with x and y being allocated separately. In those cases, the resulting path condition is PathCondition.false_.
signature common to the "normal" Domain, representing the post at the current program point, and the inverted PreDomain, representing the inferred pre-condition
garbage collect unreachable addresses in the state to make it smaller and return the new state, the live addresses, and the discarded addresses that used to have attributes attached
Check that the new equalities discovered are compatible with the current pre and post heaps, e.g. x = 0 is not compatible with x being allocated, and x = y is not compatible with x and y being allocated separately. In those cases, the resulting path condition is PathCondition.false_.
\ No newline at end of file
diff --git a/website/static/odoc/next/infer/Pulselib__PulseAccessResult/.dune-keep b/website/static/odoc/next/infer/Pulselib__PulseAccessResult/.dune-keep
new file mode 100644
index 000000000..e69de29bb
diff --git a/website/static/odoc/next/infer/Pulselib__PulseAccessResult/index.html b/website/static/odoc/next/infer/Pulselib__PulseAccessResult/index.html
new file mode 100644
index 000000000..95cb29899
--- /dev/null
+++ b/website/static/odoc/next/infer/Pulselib__PulseAccessResult/index.html
@@ -0,0 +1,2 @@
+
+Pulselib__PulseAccessResult (infer.Pulselib__PulseAccessResult)
\ No newline at end of file
diff --git a/website/static/odoc/next/infer/Pulselib__PulseAttribute/Attributes/index.html b/website/static/odoc/next/infer/Pulselib__PulseAttribute/Attributes/index.html
index 4425d4bfa..0dc0b6351 100644
--- a/website/static/odoc/next/infer/Pulselib__PulseAttribute/Attributes/index.html
+++ b/website/static/odoc/next/infer/Pulselib__PulseAttribute/Attributes/index.html
@@ -1,2 +1,2 @@
-Attributes (infer.Pulselib__PulseAttribute.Attributes)
While applying a spec, replacing ISLAbduced by Allocated and Invalidation.Cfree by Invalidation.delete, if applicable
\ No newline at end of file
diff --git a/website/static/odoc/next/infer/Pulselib__PulseAttribute/index.html b/website/static/odoc/next/infer/Pulselib__PulseAttribute/index.html
index f084eae35..a662f0a6b 100644
--- a/website/static/odoc/next/infer/Pulselib__PulseAttribute/index.html
+++ b/website/static/odoc/next/infer/Pulselib__PulseAttribute/index.html
@@ -1,2 +1,2 @@
-Pulselib__PulseAttribute (infer.Pulselib__PulseAttribute)
\ No newline at end of file
diff --git a/website/static/odoc/next/infer/Pulselib__PulseBaseAddressAttributes/index.html b/website/static/odoc/next/infer/Pulselib__PulseBaseAddressAttributes/index.html
index d414762b9..466e8fbd8 100644
--- a/website/static/odoc/next/infer/Pulselib__PulseBaseAddressAttributes/index.html
+++ b/website/static/odoc/next/infer/Pulselib__PulseBaseAddressAttributes/index.html
@@ -1,2 +1,2 @@
-Pulselib__PulseBaseAddressAttributes (infer.Pulselib__PulseBaseAddressAttributes)
merge the attributes of all the variables that are equal according to get_var_repr and remove non-canonical variables in favor of their rerpresentative
merge the attributes of all the variables that are equal according to get_var_repr and remove non-canonical variables in favor of their rerpresentative
\ No newline at end of file
diff --git a/website/static/odoc/next/infer/Pulselib__PulseDomainInterface/index.html b/website/static/odoc/next/infer/Pulselib__PulseDomainInterface/index.html
index a993d16fe..344338c8a 100644
--- a/website/static/odoc/next/infer/Pulselib__PulseDomainInterface/index.html
+++ b/website/static/odoc/next/infer/Pulselib__PulseDomainInterface/index.html
@@ -1,2 +1,2 @@
-Pulselib__PulseDomainInterface (infer.Pulselib__PulseDomainInterface)
\ No newline at end of file
diff --git a/website/static/odoc/next/infer/Pulselib__PulseExecutionDomain/index.html b/website/static/odoc/next/infer/Pulselib__PulseExecutionDomain/index.html
index 541ea664c..99d6a8694 100644
--- a/website/static/odoc/next/infer/Pulselib__PulseExecutionDomain/index.html
+++ b/website/static/odoc/next/infer/Pulselib__PulseExecutionDomain/index.html
@@ -1,2 +1,2 @@
-Pulselib__PulseExecutionDomain (infer.Pulselib__PulseExecutionDomain)
\ No newline at end of file
diff --git a/website/static/odoc/next/infer/Pulselib__PulseFormula/DynamicTypes/index.html b/website/static/odoc/next/infer/Pulselib__PulseFormula/DynamicTypes/index.html
new file mode 100644
index 000000000..cdc0b1de0
--- /dev/null
+++ b/website/static/odoc/next/infer/Pulselib__PulseFormula/DynamicTypes/index.html
@@ -0,0 +1,2 @@
+
+DynamicTypes (infer.Pulselib__PulseFormula.DynamicTypes)
Simplifies IsInstanceOf(var, typ) predicate when dynamic type information is available in state. *
\ 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 e65c0c02e..f7569e610 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)
\ No newline at end of file
diff --git a/website/static/odoc/next/infer/Pulselib__PulseInterproc/index.html b/website/static/odoc/next/infer/Pulselib__PulseInterproc/index.html
index 6638053f7..5494ed76b 100644
--- a/website/static/odoc/next/infer/Pulselib__PulseInterproc/index.html
+++ b/website/static/odoc/next/infer/Pulselib__PulseInterproc/index.html
@@ -1,2 +1,2 @@
-Pulselib__PulseInterproc (infer.Pulselib__PulseInterproc)
\ No newline at end of file
diff --git a/website/static/odoc/next/infer/Pulselib__PulseLatentIssue/index.html b/website/static/odoc/next/infer/Pulselib__PulseLatentIssue/index.html
index 7a4c28d39..0d42b23c0 100644
--- a/website/static/odoc/next/infer/Pulselib__PulseLatentIssue/index.html
+++ b/website/static/odoc/next/infer/Pulselib__PulseLatentIssue/index.html
@@ -1,2 +1,2 @@
-Pulselib__PulseLatentIssue (infer.Pulselib__PulseLatentIssue)
\ No newline at end of file
diff --git a/website/static/odoc/next/infer/Pulselib__PulseModels/index.html b/website/static/odoc/next/infer/Pulselib__PulseModels/index.html
index 208cb6388..e90795d36 100644
--- a/website/static/odoc/next/infer/Pulselib__PulseModels/index.html
+++ b/website/static/odoc/next/infer/Pulselib__PulseModels/index.html
@@ -1,2 +1,2 @@
-Pulselib__PulseModels (infer.Pulselib__PulseModels)
\ No newline at end of file
diff --git a/website/static/odoc/next/infer/Pulselib__PulseObjectiveCSummary/.dune-keep b/website/static/odoc/next/infer/Pulselib__PulseObjectiveCSummary/.dune-keep
new file mode 100644
index 000000000..e69de29bb
diff --git a/website/static/odoc/next/infer/Pulselib__PulseObjectiveCSummary/index.html b/website/static/odoc/next/infer/Pulselib__PulseObjectiveCSummary/index.html
new file mode 100644
index 000000000..fc198a631
--- /dev/null
+++ b/website/static/odoc/next/infer/Pulselib__PulseObjectiveCSummary/index.html
@@ -0,0 +1,2 @@
+
+Pulselib__PulseObjectiveCSummary (infer.Pulselib__PulseObjectiveCSummary)
For ObjC instance methods: adds path condition `self > 0` to given posts and appends additional nil summary. Does nothing to posts for other kinds of methods
\ No newline at end of file
diff --git a/website/static/odoc/next/infer/Pulselib__PulseOperations/Closures/index.html b/website/static/odoc/next/infer/Pulselib__PulseOperations/Closures/index.html
index 77bfaeac5..06e2edbe4 100644
--- a/website/static/odoc/next/infer/Pulselib__PulseOperations/Closures/index.html
+++ b/website/static/odoc/next/infer/Pulselib__PulseOperations/Closures/index.html
@@ -1,2 +1,2 @@
-Closures (infer.Pulselib__PulseOperations.Closures)
assert the validity of the addresses captured by the lambda
\ No newline at end of file
diff --git a/website/static/odoc/next/infer/Pulselib__PulseOperations/Import/index.html b/website/static/odoc/next/infer/Pulselib__PulseOperations/Import/index.html
index 31b800ee9..b26388e33 100644
--- a/website/static/odoc/next/infer/Pulselib__PulseOperations/Import/index.html
+++ b/website/static/odoc/next/infer/Pulselib__PulseOperations/Import/index.html
@@ -1,2 +1,2 @@
-Import (infer.Pulselib__PulseOperations.Import)
Module Pulselib__PulseOperations.Import
For opening in other modules.
type access_mode =
| Read
| Write
| NoAccess
The initialized-ness of the address is not checked when it evaluates a heap address without actual memory access, for example, when evaluating &x.f we need to check initialized-ness of x, not that of x.f.
Imported types for ease of use and so we can write variants without the corresponding module prefix
monadic "bind" but not really that turns an access_result into a list of access_results (not really because the first type is not an access_result list but just an access_result)
monadic "map" but even less really that turns an access_result into an analysis result
\ No newline at end of file
+Import (infer.Pulselib__PulseOperations.Import)
Module Pulselib__PulseOperations.Import
For opening in other modules.
type access_mode =
| Read
| Write
| NoAccess
The initialized-ness of the address is not checked when it evaluates a heap address without actual memory access, for example, when evaluating &x.f we need to check initialized-ness of x, not that of x.f.
Imported types for ease of use and so we can write variants without the corresponding module prefix
monadic "bind" but not really that turns an AccessResult.t into a list of AccessResult.ts (not really because the first type is not an AccessResult.t list but just an AccessResult.t)
monadic "map" but even less really that turns an AccessResult.t into an analysis result
\ No newline at end of file
diff --git a/website/static/odoc/next/infer/Pulselib__PulseOperations/index.html b/website/static/odoc/next/infer/Pulselib__PulseOperations/index.html
index 462363c00..1b8f67f4f 100644
--- a/website/static/odoc/next/infer/Pulselib__PulseOperations/index.html
+++ b/website/static/odoc/next/infer/Pulselib__PulseOperations/index.html
@@ -1,2 +1,2 @@
-Pulselib__PulseOperations (infer.Pulselib__PulseOperations)
The initialized-ness of the address is not checked when it evaluates a heap address without actual memory access, for example, when evaluating &x.f we need to check initialized-ness of x, not that of x.f.
Imported types for ease of use and so we can write variants without the corresponding module prefix
monadic "bind" but not really that turns an access_result into a list of access_results (not really because the first type is not an access_result list but just an access_result)
Similar to eval but apply to data structures and ISL abduction. Return a list of abduced states (ISLOk and ISLErs); The boolean indicates whether it is data structures or not.
Given a list of variables, computes the unreachable values if the variables were removed from the stack, then return the dynamic types of those values if they are available
The initialized-ness of the address is not checked when it evaluates a heap address without actual memory access, for example, when evaluating &x.f we need to check initialized-ness of x, not that of x.f.
Imported types for ease of use and so we can write variants without the corresponding module prefix
monadic "bind" but not really that turns an AccessResult.t into a list of AccessResult.ts (not really because the first type is not an AccessResult.t list but just an AccessResult.t)
Similar to eval but apply to data structures and ISL abduction. Return a list of abduced states (ISLOk and ISLErs); The boolean indicates whether it is data structures or not.
Given a list of variables, computes the unreachable values if the variables were removed from the stack, then return the dynamic types of those values if they are available
\ 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 1c8d9c2b7..e5ad11f51 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)
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__PulseReport/index.html b/website/static/odoc/next/infer/Pulselib__PulseReport/index.html
index 11997200f..868462cab 100644
--- a/website/static/odoc/next/infer/Pulselib__PulseReport/index.html
+++ b/website/static/odoc/next/infer/Pulselib__PulseReport/index.html
@@ -1,2 +1,2 @@
-Pulselib__PulseReport (infer.Pulselib__PulseReport)
\ No newline at end of file
diff --git a/website/static/odoc/next/infer/Pulselib__PulseSummary/index.html b/website/static/odoc/next/infer/Pulselib__PulseSummary/index.html
index c2901c485..72c105ab0 100644
--- a/website/static/odoc/next/infer/Pulselib__PulseSummary/index.html
+++ b/website/static/odoc/next/infer/Pulselib__PulseSummary/index.html
@@ -1,2 +1,2 @@
-Pulselib__PulseSummary (infer.Pulselib__PulseSummary)
\ No newline at end of file
diff --git a/website/static/odoc/next/infer/Pulselib__PulseTopl/index.html b/website/static/odoc/next/infer/Pulselib__PulseTopl/index.html
index 4c859b384..917c483da 100644
--- a/website/static/odoc/next/infer/Pulselib__PulseTopl/index.html
+++ b/website/static/odoc/next/infer/Pulselib__PulseTopl/index.html
@@ -1,2 +1,2 @@
-Pulselib__PulseTopl (infer.Pulselib__PulseTopl)
large_step ~substitution ~condition state ~callee_prepost updates state according to callee_prepost. The abstract values in condition and state are in one scope, and those in callee_prepost in another scope: the substitution maps from the callee scope to the condition&state scope.
Remove from state those parts that are inconsistent with the path condition. (We do a cheap check to not introduce inconsistent Topl states, but they mey become inconsistent because the program path condition is updated later.)
large_step ~substitution ~condition state ~callee_prepost updates state according to callee_prepost. The abstract values in condition and state are in one scope, and those in callee_prepost in another scope: the substitution maps from the callee scope to the condition&state scope.
Remove from state those parts that are inconsistent with the path condition. (We do a cheap check to not introduce inconsistent Topl states, but they mey become inconsistent because the program path condition is updated later.)
Calls Reporting.log_issue with error traces, if any.
val pp_state : Stdlib.Format.formatter ->state-> unit
\ No newline at end of file
diff --git a/website/static/odoc/next/infer/UnitTests/DifferentialTests/index.html b/website/static/odoc/next/infer/UnitTests/DifferentialTests/index.html
index 1631a047c..ba2679488 100644
--- a/website/static/odoc/next/infer/UnitTests/DifferentialTests/index.html
+++ b/website/static/odoc/next/infer/UnitTests/DifferentialTests/index.html
@@ -1,2 +1,2 @@
-DifferentialTests (infer.UnitTests.DifferentialTests)
val test_diff_keeps_duplicated_hashes : OUnit2.test
val test_set_operations : OUnit2.test
val tests : OUnit2.test
\ No newline at end of file
diff --git a/website/static/odoc/next/infer/UnitTests__DifferentialTests/index.html b/website/static/odoc/next/infer/UnitTests__DifferentialTests/index.html
index 3ff852075..55294fb55 100644
--- a/website/static/odoc/next/infer/UnitTests__DifferentialTests/index.html
+++ b/website/static/odoc/next/infer/UnitTests__DifferentialTests/index.html
@@ -1,2 +1,2 @@
-UnitTests__DifferentialTests (infer.UnitTests__DifferentialTests)