diff --git a/.github/workflows/deploy.yml b/.github/workflows/deploy.yml
index d8269449b..bb7437927 100644
--- a/.github/workflows/deploy.yml
+++ b/.github/workflows/deploy.yml
@@ -34,8 +34,7 @@ jobs:
uses: actions/cache@v1.1.2
with:
path: ${{ steps.yarn.outputs.dir }}
- # prettier-ignore
- key: ${{ runner.os }}-yarn-${{ hashFiles(format('{0}{1}', github.workspace, '/website/yarn.lock')) }}
+ key: ${{ runner.os }}-yarn-${{ hashFiles('website/yarn.lock') }}
- name: Install packages
working-directory: ${{ env.working-directory }}
diff --git a/website/.prettierignore b/website/.prettierignore
index 84ba12e04..b28b56186 100644
--- a/website/.prettierignore
+++ b/website/.prettierignore
@@ -1,2 +1,3 @@
.docusaurus/
build/
+static/
diff --git a/website/.prettierrc.json b/website/.prettierrc.json
new file mode 100644
index 000000000..5b5bd9933
--- /dev/null
+++ b/website/.prettierrc.json
@@ -0,0 +1,3 @@
+{
+ "proseWrap": "always"
+}
diff --git a/website/blog/2016-06-23-first-opensourceversary.md b/website/blog/2016-06-23-first-opensourceversary.md
index 14e785678..3501c558f 100644
--- a/website/blog/2016-06-23-first-opensourceversary.md
+++ b/website/blog/2016-06-23-first-opensourceversary.md
@@ -13,8 +13,7 @@ The Infer GitHub repo has seen a lot of activity since then:
- 339 [issues](https://github.com/facebook/infer/issues) opened
- 44 [pull requests](https://github.com/facebook/infer/pulls) by 15 contributors
- 10 [releases](https://github.com/facebook/infer/releases/)
-- 5 [external companies](/#who-uses-infer) officially using Infer (add
- yourself
+- 5 [external companies](/#who-uses-infer) officially using Infer (add yourself
[here](https://github.com/facebook/infer/edit/master/website/src/pages/index.js))
Infer was presented at 13 academic and tech international conferences, and at 8
@@ -22,10 +21,9 @@ universities around the world!
Amongst these was
[Mobile@Scale](https://code.facebook.com/posts/1566627733629653/mobile-scale-london-recap/)
-in March 2016, where we
-[announced](/blog/2016/03/17/collaboration-with-spotify) our collaboration
-with [Spotify](https://www.spotify.com/). Around the same time,
-[Uber](https://www.uber.com/) presented at
+in March 2016, where we [announced](/blog/2016/03/17/collaboration-with-spotify)
+our collaboration with [Spotify](https://www.spotify.com/). Around the same
+time, [Uber](https://www.uber.com/) presented at
[Droidcon SF](http://sf.droidcon.com/) their
[Rave](https://github.com/uber-common/rave) + Infer combo to
[help their developers move fast](https://speakerdeck.com/lukestclair/frameworks-for-coding-confidence),
diff --git a/website/docs/00-getting-started.md b/website/docs/00-getting-started.md
index aaa288fb3..d5b2f341a 100755
--- a/website/docs/00-getting-started.md
+++ b/website/docs/00-getting-started.md
@@ -8,7 +8,8 @@ title: Getting started with Infer
You can use Homebrew (Mac only), our binary releases, build infer from source,
or use our Docker image.
-On Mac, the simplest way is to use [Homebrew](http://brew.sh/). Type this into a terminal:
+On Mac, the simplest way is to use [Homebrew](http://brew.sh/). Type this into a
+terminal:
```sh
brew install infer
diff --git a/website/docs/00-hello-world.md b/website/docs/00-hello-world.md
index 259d8a076..e525eb064 100644
--- a/website/docs/00-hello-world.md
+++ b/website/docs/00-hello-world.md
@@ -6,8 +6,8 @@ title: Hello, World!
Follow the instructions in this page to try Infer on a few small examples. You
should be able to see the bugs reported by Infer, fix the bugs and run Infer
again to check that they are not reported anymore. This should give you a first
-idea of how Infer works. See the [User Guide](infer-workflow) for more
-details about the use of Infer.
+idea of how Infer works. See the [User Guide](infer-workflow) for more details
+about the use of Infer.
All these examples can be found in the
[`infer/examples`](https://github.com/facebook/infer/tree/master/examples)
diff --git a/website/docs/01-advanced-features.md b/website/docs/01-advanced-features.md
index 423365009..eb7ab3b34 100644
--- a/website/docs/01-advanced-features.md
+++ b/website/docs/01-advanced-features.md
@@ -25,8 +25,8 @@ infer-out
- `captured/` contains information for each file analyzed by Infer. See
[below](advanced-features#captured-folder) for more information.
-- `specs/` contains the [specs](advanced-features#print-the-specs) of
- each function that was analyzed, as inferred by Infer.
+- `specs/` contains the [specs](advanced-features#print-the-specs) of each
+ function that was analyzed, as inferred by Infer.
- `log/` and toplevel.log contains logs
- `report.txt` and `report.json` contain the Infer reports in text and JSON
formats
diff --git a/website/docs/01-checkers.md b/website/docs/01-checkers.md
index 6a4a0037a..337971b7b 100644
--- a/website/docs/01-checkers.md
+++ b/website/docs/01-checkers.md
@@ -10,8 +10,8 @@ based on Abstract Interpretation.
Current Infer.AI's which are in production include ThreadSafety,
AnnotationReachability (e.g., can an allocation be reached from a
@PerformanceCritical method), and
-[immutable cast](checkers-bug-types#CHECKERS_IMMUTABLE_CAST) for Java,
-as well as Static Initialization Order Fiasco for C++.
+[immutable cast](checkers-bug-types#CHECKERS_IMMUTABLE_CAST) for Java, as well
+as Static Initialization Order Fiasco for C++.
The current checkers can be run by adding the option `-a checkers` to the
analysis command as in this example:
diff --git a/website/docs/01-infer-workflow.md b/website/docs/01-infer-workflow.md
index 58651e9ba..3140ead40 100644
--- a/website/docs/01-infer-workflow.md
+++ b/website/docs/01-infer-workflow.md
@@ -61,8 +61,8 @@ would be to run Infer on your code, fix the errors generated, and run it again
to find possibly more errors or to check that all the errors have been fixed.
The errors will be displayed in the standard output and also in a file
-`infer-out/report.txt`. We filter the bugs and show the ones that are most likely
-to be real.
+`infer-out/report.txt`. We filter the bugs and show the ones that are most
+likely to be real.
## Global (default) and differential workflows
diff --git a/website/docs/01-linters.md b/website/docs/01-linters.md
index dfd24a14c..01f25f301 100644
--- a/website/docs/01-linters.md
+++ b/website/docs/01-linters.md
@@ -6,9 +6,8 @@ title: "Infer : AL"
For C/C++ and Objective-C languages, we provide a linters framework. These are
checks about the syntax of the program; it could be about a property, or about
code inside one method, or that a class or method have certain properties. We
-provide [a few checks](/docs/linters-bug-types) and we have developed a
-domain specific language (DSL) to make it easier to write checks.
-
+provide [a few checks](/docs/linters-bug-types) and we have developed a domain
+specific language (DSL) to make it easier to write checks.
## AL: A declarative language for writing linters in Infer
diff --git a/website/docs/01-racerd.md b/website/docs/01-racerd.md
index b1f4999ae..4b18cc546 100644
--- a/website/docs/01-racerd.md
+++ b/website/docs/01-racerd.md
@@ -401,8 +401,8 @@ Facebook engineers.
[A separate blog post looked at 100 recent data race fixes](https://code.facebook.com/posts/1537144479682247/finding-inter-procedural-bugs-at-scale-with-infer-static-analyzer/)
in Infer's deployment in various bug categories, and for data races observed
that 53 of them were inter-file (and thus involving multiple classes).
-[See above](racerd#interprocedural) for an example
-of RacerD's interprocedural capabilities.
+[See above](racerd#interprocedural) for an example of RacerD's interprocedural
+capabilities.
One reaction to the challenge of developing effective static race detectors has
been to ask the programmer to do more work to help the analyzer. Examples of
diff --git a/website/docs/02-limitations.md b/website/docs/02-limitations.md
index 058010d94..cbd3e5c9c 100644
--- a/website/docs/02-limitations.md
+++ b/website/docs/02-limitations.md
@@ -26,12 +26,12 @@ limitations, which we describe in terms of bug types and language features.
## Bug types
At present Infer is reporting on a restricted collection of
-[bug types](/docs/checkers-bug-types), typically involving null pointers
-and memory or resource leaks. The initial set of bug types Infer has focused on
-was driven by the most pressing needs for serving the Facebook mobile
-developers. Our approach has been to report less initially, to iterate with
-developers and provide value to them, and gradually expand what we can do while
-still providing value.
+[bug types](/docs/checkers-bug-types), typically involving null pointers and
+memory or resource leaks. The initial set of bug types Infer has focused on was
+driven by the most pressing needs for serving the Facebook mobile developers.
+Our approach has been to report less initially, to iterate with developers and
+provide value to them, and gradually expand what we can do while still providing
+value.
Some bug types we don't report as of yet include
diff --git a/website/docs/02-separation-logic-and-biabduction.md b/website/docs/02-separation-logic-and-biabduction.md
index 58429a311..a543696ca 100644
--- a/website/docs/02-separation-logic-and-biabduction.md
+++ b/website/docs/02-separation-logic-and-biabduction.md
@@ -3,12 +3,9 @@ id: separation-logic-and-bi-abduction
title: Separation logic and bi-abduction
---
-export const Math = ({ code }) => (
- (
-);
+style={{ height: '100%', verticalAlign: "middle" }} /> );
- [Separation logic](separation-logic-and-bi-abduction#separation-logic)
- [Bi-abduction](separation-logic-and-bi-abduction#bi-abduction)
@@ -16,14 +13,17 @@ style={{ height: '100%', verticalAlign: "middle" }}
## Separation logic
-Separation logic is a novel kind of mathematical logic which facilitates reasoning about
-mutations to computer memory. It enables scalability by breaking reasoning into chunks
-corresponding to local operations on memory, and then composing
-the reasoning chunks together.
+Separation logic is a novel kind of mathematical logic which facilitates
+reasoning about mutations to computer memory. It enables scalability by breaking
+reasoning into chunks corresponding to local operations on memory, and then
+composing the reasoning chunks together.
-Separation logic is based on a logical connective called the _separating conjunction_ and pronounced "and separately". Separation logic formulae are interpreted over program allocated heaps. The logical formula
- holds of a piece of program heap (a heaplet) when it can be divided into two sub-heaplets described by and .
-For example, the formula
+Separation logic is based on a logical connective
+called the _separating conjunction_ and pronounced "and separately". Separation
+logic formulae are interpreted over program allocated heaps. The logical formula
+ holds of a piece of program heap (a heaplet) when it
+can be divided into two sub-heaplets described by and
+. For example, the formula
---
@@ -31,19 +31,33 @@ For example, the formula
---
-can be read " points to and separately points to ". This formula describes precisely two allocated memory cells. The first cell is allocated at the address denoted by the pointer and the content of this cell is the value of .
-The second cell is allocated at the address denoted by the pointer and the content of this second cell is the value of . Crucially, we know that there are precisely two cells because stipulates that they are separated and therefore the cells are allocated in two different parts of memory. In other words,
-says that and do not hold the same value (i.e., these pointers are not aliased).
-The heaplet partitioning defined by the formula above can visualized like so:
+can be read " points to and
+separately points to ". This
+formula describes precisely two allocated memory cells. The first cell is
+allocated at the address denoted by the pointer and the
+content of this cell is the value of . The second cell is
+allocated at the address denoted by the pointer and the
+content of this second cell is the value of . Crucially,
+we know that there are precisely two cells because
+stipulates that they are separated and therefore the cells are allocated in two
+different parts of memory. In other words, says that
+ and do not hold the same value
+(i.e., these pointers are not aliased). The heaplet partitioning defined by the
+formula above can visualized like so:
-The important thing about separating conjunction is
-the way that it fits together with mutation to computer memory; reasoning about program commands
-tends to work by updating -conjuncts in-place, mimicking the operational in-place update of RAM.
+The important thing about separating conjunction is the way that it fits
+together with mutation to computer memory; reasoning about program commands
+tends to work by updating -conjuncts in-place, mimicking
+the operational in-place update of RAM.
-Separation logic uses Hoare triples of the form where is the precondition, a program part, and
-the postcondition. Triples are abstract specifications of the behavior of the program. For example, we could take
+Separation logic uses Hoare triples of the form
+ where
+ is the precondition, a
+program part, and the postcondition. Triples are
+abstract specifications of the behavior of the program. For example, we could
+take
---
@@ -51,11 +65,14 @@ the postcondition. Triples are abstract specifications of the behavior of the pr
---
-as a specification for a method which closes a resource given to it as a parameter.
+as a specification for a method which closes a resource given to it as a
+parameter.
-Now, suppose we have two resources and , described by
-and we close the first of them. We think operationally in terms of updating the memory in place, leaving \\(r_2 \mapsto open\\) alone,
-as described by this triple:
+Now, suppose we have two resources and
+, described by
+ and we close the
+first of them. We think operationally in terms of updating the memory in place,
+leaving \\(r_2 \mapsto open\\) alone, as described by this triple:
---
@@ -63,12 +80,13 @@ as described by this triple:
---
-What we have here is the that specification (spec) described how works by mentioning only one
-piece of state, what is sometimes called a small specification,
-and in (use) we use that specification to update a larger precondition in place.
+What we have here is the that specification (spec) described how
+ works by mentioning only one piece of
+state, what is sometimes called a small specification, and in (use) we use that
+specification to update a larger precondition in place.
-This is an instance of a general pattern.
-There is a rule that lets you go from smaller to bigger specifications
+This is an instance of a general pattern. There is a rule that lets you go from
+smaller to bigger specifications
---
@@ -79,21 +97,24 @@ There is a rule that lets you go from smaller to bigger specifications
Our passage from (spec) to (use) is obtained by taking
- to be
-- to be , and
+- to be ,
+ and
- to be
-This rule is called the _frame rule_ of separation logic. It is named after the frame problem, a classic problem in artificial intelligence.
-Generally, the describes state that remains unchanged; the terminology comes from the analogy of
-a background scene in an animation as unchanging while the objects and characters within the scene change.
+This rule is called the _frame rule_ of separation logic. It is named after the
+frame problem, a classic problem in artificial intelligence. Generally, the
+ describes state that remains unchanged; the
+terminology comes from the analogy of a background scene in an animation as
+unchanging while the objects and characters within the scene change.
-The frame rule is the key to the principle of local reasoning in separation logic: reasoning and specifications
-should concentrate on the resources that a program accesses (the footprint), without mentioning what
-doesn't change.
+The frame rule is the key to the principle of local reasoning in separation
+logic: reasoning and specifications should concentrate on the resources that a
+program accesses (the footprint), without mentioning what doesn't change.
## Bi-abduction
-Bi-abduction is a form of logical inference for separation logic which automates the key ideas about local
-reasoning.
+Bi-abduction is a form of logical inference for separation logic which automates
+the key ideas about local reasoning.
Usually, logic works with validity or entailment statements like
@@ -103,9 +124,9 @@ Usually, logic works with validity or entailment statements like
---
-which says that implies . Infer uses an extension of this inference question in an internal
-theorem prover while it runs over program statements.
-Infer's question
+which says that implies . Infer
+uses an extension of this inference question in an internal theorem prover while
+it runs over program statements. Infer's question
---
@@ -113,17 +134,24 @@ Infer's question
---
-is called _bi-abduction_. The problem here is for the theorem prover to discover a pair of frame and antiframe formulae that make the entailment statement valid.
+is called _bi-abduction_. The problem here is for the theorem prover to
+discover a pair of frame and antiframe formulae that make the entailment
+statement valid.
-Global analyses of large programs are normally computational untractable. However,
-bi-abduction allows to break the large analysis of a large program in small independent analyses of its procedures. This gives Infer the ability to scale independently of the size of the analyzed code. Moreover, by breaking the analysis in small
-independent parts, when the full program is analyzed again because
-of a code change the analysis results of the unchanged part of the
-code can be reused and only the code change needs to be re-analyzed. This process is called incremental analysis and it
-is very powerful when integrating a static analysis tool like infer in a development environment.
+Global analyses of large programs are normally computational untractable.
+However, bi-abduction allows to break the large analysis of a large program in
+small independent analyses of its procedures. This gives Infer the ability to
+scale independently of the size of the analyzed code. Moreover, by breaking the
+analysis in small independent parts, when the full program is analyzed again
+because of a code change the analysis results of the unchanged part of the code
+can be reused and only the code change needs to be re-analyzed. This process is
+called incremental analysis and it is very powerful when integrating a static
+analysis tool like infer in a development environment.
-In order to be able to decompose a global analysis in small independent analyses, let's first consider how a function
-call is analyzed in separation logic. Assume we have the following spec for a function :
+In order to be able to decompose a global analysis in small independent
+analyses, let's first consider how a function call is analyzed in separation
+logic. Assume we have the following spec for a function
+:
---
@@ -131,9 +159,10 @@ call is analyzed in separation logic. Assume we have the following spec for a fu
---
-and by analyzing the caller function, we compute that before
-the call of , the formula hold. Then
-to utilize the specification of the following implication must holds:
+and by analyzing the caller function, we compute that before the call of
+, the formula
+hold. Then to utilize the specification of the
+following implication must holds:
---
@@ -141,9 +170,10 @@ to utilize the specification of the following implicat
---
-Given that,
-bi-abduction is used at procedure call sites for two reasons: to discover missing state that is needed for the above implication to hold and allow the analysis
-to proceed (the antiframe) as well as state that the procedure leaves unchanged (the frame).
+Given that, bi-abduction is used at procedure call sites for two reasons: to
+discover missing state that is needed for the above implication to hold and
+allow the analysis to proceed (the antiframe) as well as state that the
+procedure leaves unchanged (the frame).
To see how this works suppose we have some bare code
@@ -153,12 +183,10 @@ To see how this works suppose we have some bare code
---
-but no overall specification;
-we are going to describe how to discover a pre/post spec for it.
-Considering the first statement and the (spec) above, the human might say: if only we had
- in the precondition then we could proceed.
-Technically,
-we ask a bi-abduction question
+but no overall specification; we are going to describe how to discover a
+pre/post spec for it. Considering the first statement and the (spec) above, the
+human might say: if only we had in the
+precondition then we could proceed. Technically, we ask a bi-abduction question
---
@@ -166,8 +194,11 @@ we ask a bi-abduction question
---
-and we can fill this in easily by picking and ,
-where emp means the empty state. The emp is recording that at the start we presume nothing. So we obtain the trivially true implication:
+and we can fill this in easily by picking
+ and
+, where emp means the empty state. The emp is
+recording that at the start we presume nothing. So we obtain the trivially true
+implication:
---
@@ -183,9 +214,9 @@ which, by applying logical rules, can be re-written equivalently to:
---
-Notice that this satisfy the (Function Call) requirement to correctly make the call.
-So let's add that information in the pre, and while we are at it
-record the information in the post of the first statement that comes from (spec).
+Notice that this satisfy the (Function Call) requirement to correctly make the
+call. So let's add that information in the pre, and while we are at it record
+the information in the post of the first statement that comes from (spec).
---
@@ -196,9 +227,12 @@ record the information in the post of the first statement that comes from (spec)
---
-Now, let's move to the second statement. Its precondition in the partial symbolic execution trace just given
-does not have the information needed by , so we can fill that in and continue by
-putting in the pre. While we are at it we can thread this assertion back to the beginning.
+Now, let's move to the second statement. Its precondition
+ in the partial symbolic execution trace
+just given does not have the information needed by
+, so we can fill that in and continue by
+putting in the pre. While we are at it we
+can thread this assertion back to the beginning.
---
@@ -209,7 +243,8 @@ putting in the pre. While we are at it we
---
-This information on what to thread backwards can be obtained as the antiframe part of the bi-abduction question
+This information on what to thread backwards can be obtained as the antiframe
+part of the bi-abduction question
---
@@ -219,9 +254,12 @@ This information on what to thread backwards can be obtained as the antiframe pa
where the solution picks
.
-Note that the antiframe is precisely the information missing from the precondition in order for to proceed. On the other hand, the frame is the portion of state not changed by ;
-we can thread that through to the overall postconditon
-(as justified by the frame rule), giving us
+Note that the antiframe is precisely the information missing from the
+precondition in order for to proceed. On
+the other hand, the frame is the portion
+of state not changed by ; we can thread
+that through to the overall postconditon (as justified by the frame rule),
+giving us
---
@@ -233,39 +271,53 @@ we can thread that through to the overall postconditon
---
-Thus, we have obtained a pre and post for this code by symbolically executing it, using bi-abduction
-to discover preconditions (abduction of antiframes) as well as untouched portions of memory (frames) as we go along.
-
-In general, bi-abduction
-provides a way to infer a pre/post specs from bare code, as long as we know specs for the primitives at the base level of the code. The human does not need to write preconditions and postconditions for all the procedures,
-which is the key to having a high level of automation.
-This is the basis for how Infer works, why it can scale, and how it can analyze code changes incrementally.
-
-Context: The logical terminology we have been using here comes from AI and philosophy of science.
-Abductive inference was introduced by the philosopher Charles Peirce, and described as the mechanism
-underpinning hypothesis formation (or, guessing what might be true about the world), the most
-creative part of the scientific process.
-Abduction and the frame problem have both attracted significant attention in AI.
-Infer uses an automated form of abduction to generate
-preconditions describing the memory that a program touches (the antiframe part above), and frame inference to
-discover what isn't touched.
-Infer then uses deductive reasoning to
-calculate a formula describing the effect of a program, starting from the preconditions.
-In a sense, Infer approaches automated reasoning about programs by mimicking what a human might do when trying to understand a program: it abduces what the program needs, and deduces conclusions of that.
-It is when the reasoning goes wrong that Infer reports a potential bug.
-
-This description is by necessity simplified compared to what Infer actually does.
-More technical information can be found in the following papers. The descriptions in the papers are
-precise, but still simplified; there are many engineering decisions not recorded there. Finally, beyond the papers,
-you can read the source code if you wish!
+Thus, we have obtained a pre and post for this code by symbolically executing
+it, using bi-abduction to discover preconditions (abduction of antiframes) as
+well as untouched portions of memory (frames) as we go along.
+
+In general, bi-abduction provides a way to infer a pre/post specs from bare
+code, as long as we know specs for the primitives at the base level of the code.
+The human does not need to write preconditions and postconditions for all the
+procedures, which is the key to having a high level of automation. This is the
+basis for how Infer works, why it can scale, and how it can analyze code changes
+incrementally.
+
+Context: The logical terminology we have been using here comes from AI and
+philosophy of science. Abductive inference was introduced by the philosopher
+Charles Peirce, and described as the mechanism underpinning hypothesis formation
+(or, guessing what might be true about the world), the most creative part of the
+scientific process. Abduction and the frame problem have both attracted
+significant attention in AI. Infer uses an automated form of abduction to
+generate preconditions describing the memory that a program touches (the
+antiframe part above), and frame inference to discover what isn't touched. Infer
+then uses deductive reasoning to calculate a formula describing the effect of a
+program, starting from the preconditions. In a sense, Infer approaches automated
+reasoning about programs by mimicking what a human might do when trying to
+understand a program: it abduces what the program needs, and deduces conclusions
+of that. It is when the reasoning goes wrong that Infer reports a potential bug.
+
+This description is by necessity simplified compared to what Infer actually
+does. More technical information can be found in the following papers. The
+descriptions in the papers are precise, but still simplified; there are many
+engineering decisions not recorded there. Finally, beyond the papers, you can
+read the source code if you wish!
## Technical papers
-The following papers contain some of the technical background on Infer and information on how it is used inside Facebook.
-
-- Local Reasoning about Programs that Alter Data Structures. An early separation logic paper which advanced ideas about local reasoning and the frame rule.
-- Smallfoot: Modular Automatic Assertion Checking with Separation Logic. First separation logic verification tool, introduced frame inference
-- A Local Shape Analysis Based on Separation Logic. Separation logic meets abstract interpretation; calculating loop invariants via a fixed-point computation.
-- Compositional Shape Analysis by Means of Bi-Abduction.
- The bi-abduction paper.
-- Moving Fast with Software Verification. A paper about the way we use Infer at Facebook.
+The following papers contain some of the technical background on Infer and
+information on how it is used inside Facebook.
+
+- Local
+ Reasoning about Programs that Alter Data Structures. An early separation
+ logic paper which advanced ideas about local reasoning and the frame rule.
+- Smallfoot:
+ Modular Automatic Assertion Checking with Separation Logic. First
+ separation logic verification tool, introduced frame inference
+- A Local Shape
+ Analysis Based on Separation Logic. Separation logic meets abstract
+ interpretation; calculating loop invariants via a fixed-point computation.
+- Compositional Shape
+ Analysis by Means of Bi-Abduction. The bi-abduction paper.
+- Moving
+ Fast with Software Verification. A paper about the way we use Infer at
+ Facebook.
diff --git a/website/docs/03-checker-bug-types.md b/website/docs/03-checker-bug-types.md
index 6ab1a885a..6849526b8 100644
--- a/website/docs/03-checker-bug-types.md
+++ b/website/docs/03-checker-bug-types.md
@@ -5,15 +5,16 @@ title: Checkers bug types
Here is an overview of the types of bugs currently reported by Infer checkers.
+## Captured Strong Self
-## Captured Strong Self
+This will happen in one of two cases generally:
-This will happen in one of two cases generally:
1. One uses `weakSelf` but forgot to declare it weak first.
-2. One is using `strongSelf`, declared in a block, in another (inside) block. This changes the delicate balance of the
-`weakSelf`/`strongSelf` use in the first block. The retain cycle is avoided there because `strongSelf` is a local variable
-to the block. If `strongSelf` is used in the inside block, then it's not a local variable anymore, but a captured variable.
-
+2. One is using `strongSelf`, declared in a block, in another (inside) block.
+ This changes the delicate balance of the `weakSelf`/`strongSelf` use in the
+ first block. The retain cycle is avoided there because `strongSelf` is a
+ local variable to the block. If `strongSelf` is used in the inside block,
+ then it's not a local variable anymore, but a captured variable.
## Checkers immutable cast
@@ -33,7 +34,6 @@ list e.g. by adding elements.
Action: you can change the return type to be immutable, or make a copy of the
collection so that it can be modified.
-
## Deadlock
This error is currently reported in Java. A deadlock occurs when two distinct
@@ -97,13 +97,11 @@ To suppress reports of deadlocks in a method `m()` use the
}
```
-
## Dead store
This error is reported in C++. It fires when the value assigned to a variables
is never used (e.g., `int i = 1; i = 2; return i;`).
-
## Empty vector access
This error type is reported only in C++, in versions >= C++11.
@@ -119,7 +117,6 @@ int foo(){
}
```
-
## Field should be nullable
This error type is reported in Java. It fires when a field is not marked
@@ -169,7 +166,6 @@ Action:
...
```
-
## Fragment retains view
This error type is Android-specific. It fires when a `Fragment` type fails to
@@ -182,7 +178,6 @@ retain a useless reference to that `View` that will not be cleaned up until the
Action: Nullify the `View` in question in `onDestroyView`.
-
## Interface not thread-safe
This error indicates that you have invoked an interface method not annotated
@@ -192,7 +187,6 @@ interface or to the interface method. For background on why these annotations
are needed, see the detailed explanation
[here](racerd#interface-not-thread-safe).
-
## Ivar not null checked
This error type is only reported in Objective-C. This is similar to Null
@@ -210,7 +204,6 @@ parameter is `nil`. For example:
Possible solutions are adding a check for `nil`, or making sure that the method
is not called with `nil`.
-
## Lock Consistency Violation
This is a C++ and Objective C error reported whenever:
@@ -234,7 +227,6 @@ container (an array, a vector, etc).
Infer considers a method as private if it's not exported in the header-file
interface.
-
## Mixed self weakSelf
This happens when an Objective-C block captures both `self` and `weakSelf`, a
@@ -242,11 +234,13 @@ weak pointer to `self`. Possibly the developer meant to capture only `weakSelf`
to avoid a retain cycle, but made a typo and used `self` as well in the block,
instead of `strongSelf`. In this case, this could cause a retain cycle.
-
## Multiple weakSelf
-An Objective-C block uses `weakSelf` more than once. This could lead to unexpected behaviour. Even if `weakSelf` is not nil in the first use, it could be nil in the following uses since the object that `weakSelf` points to could be freed anytime. One should assign it to a strong pointer first, and then use it in the block.
-
+An Objective-C block uses `weakSelf` more than once. This could lead to
+unexpected behaviour. Even if `weakSelf` is not nil in the first use, it could
+be nil in the following uses since the object that `weakSelf` points to could be
+freed anytime. One should assign it to a strong pointer first, and then use it
+in the block.
## Memory leak
@@ -275,7 +269,6 @@ objects from Core Foundation or Core Graphics don't get released.
}
```
-
## Null Dereference
Infer reports null dereference bugs in C, Objective-C and Java. The issue is
@@ -376,7 +369,6 @@ 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.
-
## Parameter not null checked
This error type is reported only in Objective-C. It is similar to Null
@@ -404,7 +396,6 @@ is not called with `nil`. When an argument will never be `nil`, you can add the
annotation `nonnull` to the argument's type, to tell Infer (and the type
system), that the argument won't be `nil`. This will silence the warning.
-
## Premature nil termination argument
This error type is reported in C and Objective-C. In many variadic methods,
@@ -423,7 +414,6 @@ An example of such variadic methods is
In this example, if `str` is `nil` then an array `@[@"aaa"]` of size 1 will be
created, and not an array `@[@"aaa", str, @"bbb"]` of size 3 as expected.
-
## Resource leak
Infer reports resource leaks in C, Objective-C and Java. In general, resources
@@ -700,7 +690,6 @@ way. This just illustrates that, though you might hear people say that
try-with-resources "solves" the resource problem, it does not. It is very
useful, but you cannot use it blindly when you see a resource-allocation site.
-
## Retain cycle
A retain cycle is a situation when object A retains object B, and object B
@@ -734,7 +723,6 @@ hierarchy:
@end
```
-
## Static initialization order fiasco
This error is reported in C++. It fires when the initialization of a static
@@ -745,13 +733,12 @@ already initialized or not at that point.
For more technical definition and techniques to avoid/remediate, see the
[FAQ](https://isocpp.org/wiki/faq/ctors#static-init-order).
-
## Thread-safety violation
This warning indicates a potential data race in Java. The analyser is called
RacerD and this section gives brief but a mostly complete description of its
-features. See the [RacerD page](/docs/racerd) for more in-depth information
-and examples.
+features. See the [RacerD page](/docs/racerd) for more in-depth information and
+examples.
NB this warning **is not related to @GuardedBy** and not issued by the same
analysis.
@@ -843,7 +830,6 @@ These annotations can be found at `com.facebook.infer.annotation.*`.
other threads. The main utility of this annotation is in interfaces, where
Infer cannot look up the implementation and decide for itself.
-
## UI Thread Starvation
This error is reported in Java, and specifically on Android. These reports are
@@ -902,7 +888,6 @@ This instructs Infer to filter out any potentially blocking calls in `m()`
due to a call to `m()`. You will need to set up your class path appropriately to
include the JAR files in `infer/annotations` for this annotation to work.
-
## Strict mode violation
Android has a feature called
@@ -915,7 +900,6 @@ ability to statically detect such violations.
To suppress this warning, it's enough to annotate the offending method with
`@SuppressLint("STRICT_MODE_VIOLATION")`.
-
## StrongSelf Not Checked
When a block captures `weakSelf` in the following pattern:
@@ -931,7 +915,6 @@ the variable `strongSelf` should be checked for `null` before being used,
otherwise this could cause a crash because the weak pointer `weakSelf` could be
`null`.
-
## Unsafe GuardedBy Access
Infer reports issues when a field or method is accessed when a lock is not held,
@@ -1010,8 +993,9 @@ Outer.java:13: error: UNSAFE_GUARDED_BY_ACCESS
```
-
## weakSelf In NOESCAPE Block
-In many methods that take a block as an argument, the block position is annotated with NS_NOESCAPE to mark that the block
-passed to this method won't be leaving the current scope. In those cases, there is no need to use `weakSelf` to avoid the block to capture `self`. This issue type flags this case.
+In many methods that take a block as an argument, the block position is
+annotated with NS_NOESCAPE to mark that the block passed to this method won't be
+leaving the current scope. In those cases, there is no need to use `weakSelf` to
+avoid the block to capture `self`. This issue type flags this case.
diff --git a/website/docs/03-eradicate-warnings.md b/website/docs/03-eradicate-warnings.md
index f413ff6ca..b54fca270 100644
--- a/website/docs/03-eradicate-warnings.md
+++ b/website/docs/03-eradicate-warnings.md
@@ -32,7 +32,6 @@ could originate in third party libraries which are not under your control, and
the best place to check for null is typically immediately after calling these
library functions.
-
## Eradicate null method call
A method call x.m(...) where x could be null.
@@ -49,7 +48,6 @@ class C {
Action: Same as for Null field access.
-
## Eradicate field not nullable
An assignment x.f = v where v could be null and field f is not annotated with
diff --git a/website/docs/03-linter-bug-types.md b/website/docs/03-linter-bug-types.md
index 69032853b..0b80be15b 100644
--- a/website/docs/03-linter-bug-types.md
+++ b/website/docs/03-linter-bug-types.md
@@ -5,14 +5,14 @@ title: Linters bug types
Here is an overview of the linter checks we provide in Infer:
-## Assign pointer warning
+## Assign pointer warning
This check fires when a pointer to an Obj-C object is tagged with an `assign`
property (similar to the `-Warc-unsafe-retained-assign` compiler flag). Not
holding a strong reference to the object makes it easy to accidentally create
and use a dangling pointer.
-## Bad pointer comparison
+## Bad pointer comparison
Infer reports these warnings in Objective-C when a boxed primitive type such as
`NSNumber *` is coerced to a boolean in a comparison. For example, consider the
@@ -29,7 +29,7 @@ integer pointed to by `n` is nonzero (e.g., she may have meant to call an
accessor like `[n intValue]` instead). Infer will ask the programmer explicitly
compare `n` to `nil` or call an accessor to clarify her intention.
-## C++ reference captured in Objective-C block
+## C++ reference captured in Objective-C block
With this check, Infer detects C++ references captured in a block. Doing this is
almost always wrong. The reason is that C++ references are not managed pointers
@@ -46,7 +46,7 @@ const int copied_v = v;
};
```
-## Direct atomic property access
+## Direct atomic property access
This check warns you when you are accessing an atomic property directly with an
ivar. This makes the atomic property not atomic anymore. So potentially you may
@@ -54,14 +54,14 @@ get a race condition.
To fix the problem you need to access properties with their getter or setter.
-## Global variable initialized with function or method call
+## Global variable initialized with function or method call
This checker warns you when the initialization of global variable contain a
method or function call. The warning wants to make you aware that some functions
are expensive. As the global variables are initialized before main() is called,
these initializations can slow down the start-up time of an app.
-## Registered observer being deallocated
+## Registered observer being deallocated
Objects register with a notification center to receive notifications. This check
warns you when an object is registered as observer of a NSNotificationCenter but
@@ -69,13 +69,13 @@ it is never unregistered. This is problematic as if the object is not
unregistered the notification center can still send notification even after the
object has been deallocated. In that case we would get a crash.
-## Strong delegate warning
+## Strong delegate warning
This check warns you when you have a property called delegate or variations
thereof which is declared strong. The idea is that delegates should generally be
weak, otherwise this may cause retain cycles.
-## Unavailable api in supported ios sdk
+## Unavailable api in supported ios sdk
This checks warns you when you are using an API (constant, method call, etc.)
that is only defined in a version higher than the version that you support. To
@@ -98,14 +98,14 @@ if (kCFCoreFoundationVersionNumber >= kCFCoreFoundationVersionNumber_iOS_9_0) {
}
```
-## Pointer To const Objective-C Class
+## Pointer To const Objective-C Class
In Objective-C, `const Class *` represents a mutable pointer pointing to an
Objective-C class where the ivars cannot be changed. More useful is
`Class *const` instead, meaning the destination of the pointer cannot be
changed.
-## Objective-C Weak Property has Custom Setter
+## Objective-C Weak Property has Custom Setter
This check warns you when you have a custom setter for a weak property. When
compiled with Automatic Reference Counting (ARC, `-fobj-arc`) ARC may set the
@@ -172,22 +172,22 @@ I work for (null)
Note that the custom setter was only invoked once.
-## Component factory function
+## Component factory function
[Doc in ComponentKit page](http://componentkit.org/docs/break-out-composites)
-## Component initializer with side effects
+## Component initializer with side effects
[Doc in ComponentKit page](http://componentkit.org/docs/no-side-effects)
-## Component with multiple factory methods
+## Component with multiple factory methods
[Doc in ComponentKit page](http://componentkit.org/docs/avoid-overrides)
-## Component with unconventional superclass
+## Component with unconventional superclass
[Doc in ComponentKit page](http://componentkit.org/docs/never-subclass-components)
-## Mutable local variable in component file
+## Mutable local variable in component file
[Doc in ComponentKit page](http://componentkit.org/docs/avoid-local-variables)
diff --git a/website/docs/04-absint-framework.md b/website/docs/04-absint-framework.md
index b8d820903..0fba85ebc 100644
--- a/website/docs/04-absint-framework.md
+++ b/website/docs/04-absint-framework.md
@@ -81,9 +81,8 @@ checkers
[here](https://github.com/facebook/infer/blob/master/infer/src/checkers/registerCheckers.ml#L42).
you can then run `infer run -a checkers -- ` to run your
-checker on real code. See
-[here](/docs/analyzing-apps-or-projects) for more details
-on the build systems supported by Infer.
+checker on real code. See [here](/docs/analyzing-apps-or-projects) for more
+details on the build systems supported by Infer.
Other examples of simple intraprocedural checkers are
[addressTaken.ml](https://github.com/facebook/infer/blob/master/infer/src/checkers/addressTaken.ml)
diff --git a/website/docs/04-internal-API.md b/website/docs/04-internal-API.md
index 1cdf3fe92..927032082 100644
--- a/website/docs/04-internal-API.md
+++ b/website/docs/04-internal-API.md
@@ -4,8 +4,8 @@ title: Infer Internal OCaml Modules API
---
The generated OCaml documentation for the latest release of infer can be found
-[here](/odoc/latest/index.html). You can generate these pages from within
-an infer git checkout with `make doc`.
+[here](/odoc/latest/index.html). You can generate these pages from within an
+infer git checkout with `make doc`.
You can also browse the following specific versions:
diff --git a/website/docs/support.md b/website/docs/support.md
index 209700dac..b99ccebf3 100644
--- a/website/docs/support.md
+++ b/website/docs/support.md
@@ -43,8 +43,8 @@ infer run -- xcodebuild -workspace HelloWorld.xcworkspace -scheme HelloWorld
### "infer [options] -- \" fails during a linking step
The linker will sometimes not work if files have been compiled using a different
-compiler, such as the one Infer uses [under the hood](/docs/infer-workflow)
-to analyze your files.
+compiler, such as the one Infer uses [under the hood](/docs/infer-workflow) to
+analyze your files.
A workaround consists in setting the `LD` environment variable to a dummy
linker, for instance:
diff --git a/website/docusaurus.config.js b/website/docusaurus.config.js
index ca5ac1147..c9def1905 100755
--- a/website/docusaurus.config.js
+++ b/website/docusaurus.config.js
@@ -6,66 +6,66 @@
*/
module.exports = {
- title: 'Infer',
+ title: "Infer",
tagline:
- 'A tool to detect bugs in Java and C/C++/Objective-C code before it ships',
- url: 'https://fbinfer.com',
- baseUrl: '/',
- favicon: 'img/favicon.png',
- organizationName: 'facebook',
- projectName: 'infer',
+ "A tool to detect bugs in Java and C/C++/Objective-C code before it ships",
+ url: "https://fbinfer.com",
+ baseUrl: "/",
+ favicon: "img/favicon.png",
+ organizationName: "facebook",
+ projectName: "infer",
themeConfig: {
algolia: {
- apiKey: 'aac9e661e851db0d4b6e74802c3df9de',
- indexName: 'fbinfer',
+ apiKey: "aac9e661e851db0d4b6e74802c3df9de",
+ indexName: "fbinfer",
},
navbar: {
- title: 'Infer',
- logo: { alt: 'Infer Logo', src: 'img/logo.png' },
+ title: "Infer",
+ logo: { alt: "Infer Logo", src: "img/logo.png" },
links: [
- { label: 'Docs', to: 'docs/getting-started' },
- { label: 'Support', to: 'docs/support' },
- { label: 'Blog', to: 'blog' },
+ { label: "Docs", to: "docs/getting-started" },
+ { label: "Support", to: "docs/support" },
+ { label: "Blog", to: "blog" },
{
- href: 'https://twitter.com/fbinfer',
- label: 'Twitter',
- position: 'right',
+ href: "https://twitter.com/fbinfer",
+ label: "Twitter",
+ position: "right",
},
{
- href: 'https://www.facebook.com/inferstaticanalyzer',
- label: 'Facebook',
- position: 'right',
+ href: "https://www.facebook.com/inferstaticanalyzer",
+ label: "Facebook",
+ position: "right",
},
{
- href: 'https://github.com/facebook/infer',
- label: 'GitHub',
- position: 'right',
+ href: "https://github.com/facebook/infer",
+ label: "GitHub",
+ position: "right",
},
],
},
footer: {
- style: 'light',
+ style: "light",
links: [
{
- title: 'Docs',
+ title: "Docs",
items: [
- { label: 'Quick Start', to: 'docs/getting-started' },
- { label: 'User Guide', to: 'docs/infer-workflow' },
- { label: 'Foundations', to: 'docs/about-Infer' },
- { label: 'Bug Types Reference', to: 'docs/checkers-bug-types' },
- { label: 'Contribute', to: 'docs/absint-framework' },
+ { label: "Quick Start", to: "docs/getting-started" },
+ { label: "User Guide", to: "docs/infer-workflow" },
+ { label: "Foundations", to: "docs/about-Infer" },
+ { label: "Bug Types Reference", to: "docs/checkers-bug-types" },
+ { label: "Contribute", to: "docs/absint-framework" },
],
},
{
- title: 'Community',
- items: [{ label: 'Support', to: 'docs/support' }],
+ title: "Community",
+ items: [{ label: "Support", to: "docs/support" }],
},
{
- title: 'Social',
+ title: "Social",
items: [
- { label: 'Blog', to: 'blog' },
- { label: 'GitHub', href: 'https://github.com/facebook/infer' },
- { label: 'Twitter', href: 'https://twitter.com/fbinfer' },
+ { label: "Blog", to: "blog" },
+ { label: "GitHub", href: "https://github.com/facebook/infer" },
+ { label: "Twitter", href: "https://twitter.com/fbinfer" },
],
},
],
@@ -74,10 +74,10 @@ module.exports = {
},
presets: [
[
- '@docusaurus/preset-classic',
+ "@docusaurus/preset-classic",
{
- docs: { sidebarPath: require.resolve('./sidebars.js') },
- theme: { customCss: require.resolve('./src/css/custom.css') },
+ docs: { sidebarPath: require.resolve("./sidebars.js") },
+ theme: { customCss: require.resolve("./src/css/custom.css") },
},
],
],
diff --git a/website/package.json b/website/package.json
index 2432ad7c8..6b2dde420 100755
--- a/website/package.json
+++ b/website/package.json
@@ -2,21 +2,23 @@
"license": "MIT",
"private": true,
"scripts": {
+ "fmt:check": "prettier --check .",
+ "fmt": "prettier --write .",
"start": "docusaurus start",
"build": "docusaurus build",
"swizzle": "docusaurus swizzle",
"deploy": "docusaurus deploy"
},
"dependencies": {
- "@docusaurus/core": "2.0.0-alpha.43",
- "@docusaurus/preset-classic": "2.0.0-alpha.43",
+ "@docusaurus/core": "2.0.0-alpha.48",
+ "@docusaurus/preset-classic": "2.0.0-alpha.48",
"classnames": "2.2.6",
- "react": "16.13.0",
- "react-dom": "16.13.0",
+ "react": "16.13.1",
+ "react-dom": "16.13.1",
"react-github-btn": "1.1.1"
},
"devDependencies": {
- "prettier": "1.19.1"
+ "prettier": "2.0.2"
},
"browserslist": {
"production": [
diff --git a/website/sidebars.js b/website/sidebars.js
index 99c2d2cb9..a31ba2cb4 100755
--- a/website/sidebars.js
+++ b/website/sidebars.js
@@ -19,18 +19,18 @@ module.exports = {
"experimental-checkers",
"advanced-features",
"adding-models",
- "man-pages"
+ "man-pages",
],
Foundations: [
"about-Infer",
"separation-logic-and-bi-abduction",
- "limitations"
+ "limitations",
],
"Bug Types Reference": [
"checkers-bug-types",
"eradicate-warnings",
- "linters-bug-types"
+ "linters-bug-types",
],
- Contribute: ["absint-framework", "adding-checkers", "internal-API"]
- }
+ Contribute: ["absint-framework", "adding-checkers", "internal-API"],
+ },
};
diff --git a/website/src/pages/index.js b/website/src/pages/index.js
index 26b695d16..dc55e2fc0 100755
--- a/website/src/pages/index.js
+++ b/website/src/pages/index.js
@@ -24,7 +24,7 @@ const features = [
reachability, missing lock guards, and concurrency race conditions in
Android and Java code.
- )
+ ),
},
{
title: <>C, C++, and iOS/Objective-C,
@@ -33,8 +33,8 @@ const features = [
Infer checks for null pointer dereferences, memory leaks, coding
conventions and unavailable API’s.
- )
- }
+ ),
+ },
];
const poweredByImages = [
@@ -46,7 +46,7 @@ const poweredByImages = [
{ url: "https://www.oculus.com", image: "/img/who/oculus.png" },
{
url: "/blog/2016/03/17/collaboration-with-spotify",
- image: "/img/who/spotify.png"
+ image: "/img/who/spotify.png",
},
{ url: "https://www.uber.com", image: "/img/who/uber.svg" },
{ url: "https://www.whatsapp.com", image: "/img/who/whatsapp.svg" },
@@ -85,27 +85,40 @@ function Home() {
users, and help prevent crashes or poor performance.