diff --git a/infer/src/backend/registerCheckers.ml b/infer/src/backend/registerCheckers.ml
index c0c3f52e5..4390d0c99 100644
--- a/infer/src/backend/registerCheckers.ml
+++ b/infer/src/backend/registerCheckers.ml
@@ -11,13 +11,6 @@ open! IStd
 
 module F = Format
 
-(* make sure SimpleChecker.ml is not dead code *)
-let () =
-  if false then
-    let module SC = SimpleChecker.Make in
-    ()
-
-
 type callback_fun =
   | Procedure of Callbacks.proc_callback_t
   | DynamicDispatch of Callbacks.proc_callback_t
diff --git a/infer/src/checkers/SimpleChecker.ml b/infer/src/checkers/SimpleChecker.ml
deleted file mode 100644
index 4e1596397..000000000
--- a/infer/src/checkers/SimpleChecker.ml
+++ /dev/null
@@ -1,96 +0,0 @@
-(*
- * Copyright (c) Facebook, Inc. and its affiliates.
- *
- * This source code is licensed under the MIT license found in the
- * LICENSE file in the root directory of this source tree.
- *)
-
-open! IStd
-module F = Format
-module L = Logging
-
-(** functor that makes it easy to write a basic abstract interpretation checker by lifting a type,
-    comparison function, reporting function, and exec function into an analyzer *)
-
-module type Spec = sig
-  (** what state do you want to propagate? *)
-  type t
-
-  val initial : t
-  (** implement the state the analysis should start from here *)
-
-  val exec_instr : t -> Sil.instr -> Procdesc.Node.nodekind -> Procname.t -> Tenv.t -> t
-  (** implement how an instruction changes your state here. input is the previous state, current
-      instruction, current node kind, current procedure and type environment. *)
-
-  val report : t -> Location.t -> Procname.t -> unit
-  (** log errors here. input is a state, location where the state occurs in the source, and the
-      current procedure. *)
-
-  val compare : t -> t -> int
-end
-
-module type S = sig
-  val checker : IntraproceduralAnalysis.t -> unit
-  (** add YourChecker.checker to registerCallbacks.ml to run your checker *)
-end
-
-module Make (Spec : Spec) : S = struct
-  (* powerset domain over Spec.t *)
-  module Domain = struct
-    include AbstractDomain.FiniteSet (struct
-      type t = Spec.t
-
-      let compare = Spec.compare
-
-      let pp _ _ = ()
-    end)
-
-    let widen ~prev ~next ~num_iters =
-      let iters_befor_timeout = 1000 in
-      (* failsafe for accidental non-finite height domains *)
-      if num_iters >= iters_befor_timeout then
-        L.(die InternalError)
-          "Stopping analysis after 1000 iterations without convergence. Make sure your domain is \
-           finite height."
-      else widen ~prev ~next ~num_iters
-  end
-
-  module TransferFunctions (CFG : ProcCfg.S) = struct
-    module CFG = CFG
-    module Domain = Domain
-
-    type analysis_data = IntraproceduralAnalysis.t
-
-    let exec_instr astate_set {IntraproceduralAnalysis.proc_desc; tenv} node instr =
-      let node_kind = CFG.Node.kind node in
-      let pname = Procdesc.get_proc_name proc_desc in
-      Domain.fold
-        (fun astate acc -> Domain.add (Spec.exec_instr astate instr node_kind pname tenv) acc)
-        astate_set Domain.empty
-
-
-    let pp_session_name _node fmt = F.pp_print_string fmt "simple checker"
-  end
-
-  module Analyzer = AbstractInterpreter.MakeRPO (TransferFunctions (ProcCfg.Exceptional))
-
-  let checker ({IntraproceduralAnalysis.proc_desc} as analysis_data) =
-    let proc_name = Procdesc.get_proc_name proc_desc in
-    let nodes = Procdesc.get_nodes proc_desc in
-    let do_reporting node_id state =
-      let astate_set = state.AbstractInterpreter.State.post in
-      if not (Domain.is_empty astate_set) then
-        (* should never fail since keys in the invariant map should always be real node id's *)
-        let node =
-          List.find_exn
-            ~f:(fun node -> Procdesc.Node.equal_id node_id (Procdesc.Node.get_id node))
-            nodes
-        in
-        Domain.iter
-          (fun astate -> Spec.report astate (ProcCfg.Exceptional.Node.loc node) proc_name)
-          astate_set
-    in
-    let inv_map = Analyzer.exec_pdesc analysis_data ~initial:Domain.empty proc_desc in
-    Analyzer.InvariantMap.iter do_reporting inv_map
-end
diff --git a/infer/src/checkers/SimpleChecker.mli b/infer/src/checkers/SimpleChecker.mli
deleted file mode 100644
index ecd0a7fc5..000000000
--- a/infer/src/checkers/SimpleChecker.mli
+++ /dev/null
@@ -1,26 +0,0 @@
-(*
- * Copyright (c) Facebook, Inc. and its affiliates.
- *
- * This source code is licensed under the MIT license found in the
- * LICENSE file in the root directory of this source tree.
- *)
-
-open! IStd
-
-module type Spec = sig
-  type t
-
-  val initial : t
-
-  val exec_instr : t -> Sil.instr -> Procdesc.Node.nodekind -> Procname.t -> Tenv.t -> t
-
-  val report : t -> Location.t -> Procname.t -> unit
-
-  val compare : t -> t -> int
-end
-
-module type S = sig
-  val checker : IntraproceduralAnalysis.t -> unit
-end
-
-module Make (Spec : Spec) : S
diff --git a/website/docs/04-absint-framework.md b/website/docs/04-absint-framework.md
index af3244fe5..d230c6936 100644
--- a/website/docs/04-absint-framework.md
+++ b/website/docs/04-absint-framework.md
@@ -6,14 +6,13 @@ title: Building checkers with the Infer.AI framework
 Infer.AI is a framework for quickly developing abstract interpretation-based
 checkers (intraprocedural or interprocedural). You define only:
 
-(1) An abstract domain (type of abstract state plus `<=`, `join`, and `widen`
+1. An abstract domain (type of abstract state plus `<=`, `join`, and `widen`
 operations)
-
-(2) Transfer functions (a transformer that takes an abstract state as input and
+2. Transfer functions (a transformer that takes an abstract state as input and
 produces an abstract state as output)
 
-and then you have an analysis that can run on all of the languages Infer
-supports (C, Obj-C, C++, and Java)!
+What you get in exchange is an analysis that can run on all of the
+languages Infer supports (C, Objective-C, C++, and Java)!
 
 This guide covers how to use the framework. For background on why we built the
 framework and how it works, check out these
@@ -44,14 +43,13 @@ There are basically three important bits here: defining the domain, defining the
 transfer functions, and then passing the pieces to the framework to create an an
 analysis. Let's break down the third bit:
 
-```
-module Analyzer =
-  AbstractInterpreter.Make
-    (ProcCfg.Backward(ProcCfg.Exceptional))
-    (TransferFunctions)
+```OCaml
+module CFG = ProcCfg.OneInstrPerNode (ProcCfg.Backward (ProcCfg.Exceptional))
+module CheckerAnalyzer =
+  AbstractInterpreter.MakeRPO (TransferFunctions (CheckerMode) (CFG))
 ```
 
-The `ProcCfg.Backward(ProcCfg.Exceptional)` part says: "I want the direction of
+The `ProcCfg.Backward (ProcCfg.Exceptional)` part says: "I want the direction of
 iteration to be backward" (since liveness is a backward analysis), and "I want
 to the analysis to follow exceptional edges". For a forward analysis that
 ignores exceptional edges, you would do `ProcCfg.Normal` instead (and many other
@@ -60,45 +58,46 @@ combinations are possible; take a look at
 for more). And finally, the `TransferFunctions` part says "Use the transfer
 functions I defined above".
 
-Now you have an `Analyzer` module that exposes useful functions like
+Now you have a `CheckerAnalyzer` module that exposes useful functions
+like
 [`compute_post`](https://github.com/facebook/infer/blob/master/infer/src/absint/AbstractInterpreter.mli#L30)
 (take a procedure as input and compute a postcondition) and
 [`exec_pdesc`](https://github.com/facebook/infer/blob/master/infer/src/absint/AbstractInterpreter.mli#L36)
-(take a procedure and compute an invariant map from node id's to the pre/post at
-each node). The next step is to hook your checker up to the Infer CLI. For the
-liveness analysis, you would do this by exposing a function for running the
-checker on a single procedure:
-
-```
-let checker { Callbacks.proc_desc; tenv; } =
-  match Analyzer.compute_post (ProcData.make_default proc_desc tenv) with
-  | Some post -> Logging.progress "Computed post %a for %a" Analyzer.Domain.pp post Typ.Procname.pp (Procdesc.get_proc_name proc_desc);
+(take a procedure and compute an invariant map from node id's to the
+pre/post at each node). The next step is to hook your checker up to
+the Infer command-line interface (CLI). For the liveness analysis, you
+would do this by exposing a function for running the checker on a
+single procedure:
+
+```OCaml
+let checker ({IntraproceduralAnalysis.proc_desc; err_log} as analysis_data) =
+  match Analyzer.compute_post analysis_data ~initial:Domain.empty with
+  | Some post ->
+      Logging.progress "Computed post %a for %a"
+        Domain.pp post Procname.pp (Procdesc.get_proc_name proc_desc);
   | None -> ()
 ```
 
-and then adding `Liveness.checker, checkers_enabled` to the list of registered
-checkers
-[here](https://github.com/facebook/infer/blob/master/infer/src/checkers/registerCheckers.ml#L42).
+and then adding `Liveness.checker` to the list of registered checkers
+in
+[registerCheckers.ml](https://github.com/facebook/infer/blob/master/infer/src/backend/registerCheckers.ml)
+(search for "Liveness").
 
-you can then run `infer run -a checkers -- <your_build_command>` to run your
+you can then run `infer run --liveness-only -- <your_build_command>` to run your
 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)
 and
-[copyPropagation.ml](https://github.com/facebook/infer/blob/master/infer/src/checkers/copyPropagation.ml).
+[Siof.ml](https://github.com/facebook/infer/blob/master/infer/src/checkers/Siof.ml).
 
-## Basic error reporting
+## Error reporting
 
-Useful analyses have output. Basic printing to stderr or stderr is good for
-debugging, but to report a programmer-readable error that is tied to a source
-code location, you'll want to use `Reporting.log_error`. Some examples of
-error-logging code:
-[1](https://github.com/facebook/infer/blob/master/infer/src/concurrency/RacerD.ml#L166),
-[2](https://github.com/facebook/infer/blob/master/infer/src/checkers/annotationReachability.ml#L224),
-or
-[3](https://github.com/facebook/infer/blob/master/infer/src/quandary/TaintAnalysis.ml#L186).
+Useful analyses have output. Basic printing to stderr or stderr is
+good for debugging, but to report a programmer-readable error that is
+tied to a source code location, you'll want to use
+[`Reporting.log_issue`](/odoc/next/infer/Absint/Reporting/index.html#val-log_issue).
 
 ## By example: interprocedural analysis
 
@@ -110,187 +109,61 @@ more; global analyses cannot be expressed in this framework.
 
 To make your checker interprocedural, you need to:
 
-(1) Define the type of procedure summaries for your analysis and add some
-boilerplate for storing your data alongside the summaries for other analyses
+1. Define the type of procedure summaries for your analysis and let
+registerCheckers.ml know that your checker is interprocedural
 
-(2) Add logic for (a) using summaries in your transfer functions and (b)
+2. Add logic for (a) using summaries in your transfer functions and (b)
 converting your intraprocedural abstract state to a summary.
 
 A good example to look at here is
-[siof.ml](https://github.com/facebook/infer/blob/master/infer/src/checkers/Siof.ml).
+[Siof.ml](https://github.com/facebook/infer/blob/master/infer/src/checkers/Siof.ml).
 Step (1) is just:
 
-```
-module Summary = Summary.Make (struct
-    type summary = SiofDomain.astate
+```OCaml
+(* in src/checkers/SiofDomain.ml *)
+(* note that as a result the type of summaries is the same as the type of domain
+   elements *)
+module Summary = ...
+include Summary
+
+
+(* in src/backend/Payloads.ml: register the payload of the analyzer *)
+type t =
+  { ...
+  ; siof: SiofDomain.Summary.t option
+  ... }
 
-    let update_payload astate payload =
-      { payload with Specs.siof = Some astate }
 
-    let read_from_payload payload =
-      payload.Specs.siof
-  end)
+(* in src/backend/registerCheckers.ml *)
+let all_checkers = [ ...
+  ; {checker= SIOF; callbacks= [(interprocedural Payloads.Fields.siof Siof.checker, Clang)]}
+  ... ]
 ```
 
-along with adding the `Specs.siof`
-[field](https://github.com/facebook/infer/blob/master/infer/src/backend/specs.ml#L329)
-to the `Specs.payload` record
-[type](https://github.com/facebook/infer/blob/master/infer/src/backend/specs.ml#L321).
 Here, the type of the abstract state and the type of the summary are the same,
 which makes things easier for us (no logic to convert an abstract state to a
 summary).
 
 Part (2a) is
-[here](https://github.com/facebook/infer/blob/master/infer/src/checkers/Siof.ml#L65):
+[here](https://github.com/facebook/infer/blob/be4ddc48f6330b7b788d899ce12ca51b4d673530/infer/src/checkers/Siof.ml#L168)
+and uses the `analyze_dependency` callback provided by the framework:
 
 ```
-match Summary.read_summary pdesc callee_pname with
+match analyze_dependency callee_pname with
 ```
 
-This says: "read the summary for `callee_pname` from procedure `pdesc` with type
-environment `tenv`". You must then add logic for applying the summary to the
+This says: "read the summary for `callee_pname`, possibly computing it
+first". You must then add logic for applying the summary to the
 current abstract state (often, this is as simple as doing a join).
 
-Because our summary type is the same as the abstract state, part (2b) can be
-done for us by making use of the convenient
-`AbstractInterpreter.Interprocedural`
-[functor](https://github.com/facebook/infer/blob/master/infer/src/absint/AbstractInterpreter.mli#L19)
-(for an example of what to do when the types are different, take a look at
-[Quandary](https://github.com/facebook/infer/blob/master/infer/src/quandary/TaintAnalysis.ml#L540)):
-
-```
-module Interprocedural = Analyzer.Interprocedural (Summary)
-```
-
-This `Interprocedural` module will automatically do the work of computing and
-storing the summary for us. All we need to do is change the exposed `checker`
-function registered in `registerCheckers.ml` to call `Interprocedural.checker`
-instead:
-
-```
-let checker callback =
-  ignore(Interprocedural.checker callback ProcData.empty_extras in)
-```
+Because our summary type is the same as the abstract state, part (2b)
+here simply consists in return the post computed by the analysis as
+the procedure's summary, using `Analyzer.compute_post`.
 
 That's it! We now have an interprocedural analysis.
 
-One very important note here: a current (and soon-to-be-lifted) limitation
-prevents us from running multiple interprocedural checkers at the same time. If
-you register an interprocedural checker, be sure to unregister the other other
-ones. Otherwise, there's a risk that the checkers will clobber each other's
-results.
-
-## Relevant code
-
-Some pointers to useful code for building new analyses, and to the
-implementation of the framework for the interested:
-
-Domain combinators:
-
-- `AbstractDomain.BottomLifted`, `AbstractDomain.FiniteSet`,
-  `AbstractDomain.Map`, `AbstractDomain.Pair` (all in
-  [AbstractDomain](https://github.com/facebook/infer/blob/master/infer/src/checkers/AbstractDomain.mli))
-
-Domains and domain building blocks:
-
-- [AccessPath](https://github.com/facebook/infer/blob/master/infer/src/checkers/accessPath.mli)
-- [AccessPathDomains](https://github.com/facebook/infer/blob/master/infer/src/checkers/accessPathDomains.mli)
-- [AccessTree](https://github.com/facebook/infer/blob/master/infer/src/checkers/accessTree.ml)
-
-Reporting errors with interprocedural traces:
-
-- Examples:
-  [`SiofTrace.ml`](https://github.com/facebook/infer/blob/master/infer/src/checkers/SiofTrace.ml),
-  [`JavaTrace.ml`](https://github.com/facebook/infer/blob/master/infer/src/quandary/JavaTrace.ml),
-  [`CppTrace.ml`](https://github.com/facebook/infer/blob/master/infer/src/quandary/CppTrace.ml).
-- Implementation:
-  [`Trace`](https://github.com/facebook/infer/blob/master/infer/src/checkers/Trace.mli)
-
-Implementation:
-
-- [`AbstractDomain`](https://github.com/facebook/infer/blob/master/infer/src/absint/AbstractDomain.ml)
-- [`TransferFunctions`](https://github.com/facebook/infer/blob/master/infer/src/absint/AbstractInterpreter.mli)
-- [`AbstractInterpreter`](https://github.com/facebook/infer/blob/master/infer/src/absint/AbstractInterpreter.mli)
-- [`ProcCFG`](https://github.com/facebook/infer/blob/master/infer/src/absint/ProcCfg.mli)
-- [`Summary`](https://github.com/facebook/infer/blob/master/infer/src/absint/Summary.ml)
-- [`Scheduler`](https://github.com/facebook/infer/blob/master/infer/src/absint/Scheduler.ml)
-
-## IR basics: SIL, CFG's, `tenv`'s, `procdesc`'s, and `procname`'s
-
-All of the languages analyzed by Infer are converted into a common intermediate
-representation. A program is represented as a control-flow graph
-([CFG](https://github.com/facebook/infer/blob/master/infer/src/IR/Cfg.rei))
-whose nodes contain lists of instructions in the SIL language. SIL is a small
-low-level language that has some similarities with C, LLVM
-[IR](http://llvm.org/docs/LangRef.html), and
-[Boogie](https://research.microsoft.com/en-us/um/people/leino/papers/krml178.pdf).
-
-[Expressions](https://github.com/facebook/infer/blob/master/infer/src/IR/Exp.rei#L25)
-are literals, program variables (`Pvar`'s), temporary variables (`Ident`'s), a
-field offset from a struct (OO features like objects are lowered into struct's),
-or an index offset from an array.
-
-There are four interesting kinds of
-[instructions](https://github.com/facebook/infer/blob/master/infer/src/IR/Sil.rei#L38):
-`Load` for reading into a temporary variable, `Store` for writing to a program
-variable, field of a struct, or an array, `Prune e` (often called `assume` in
-other PL formalisms) blocks execution unless the expression `e` evaluates to
-true, and `Call` represents function calls.
-
-Instructions and expressions have
-[types](https://github.com/facebook/infer/blob/master/infer/src/IR/Typ.rei#L76).
-A `Tstruct` (think: object) type has a
-[`Typename`](https://github.com/facebook/infer/blob/master/infer/src/IR/Typename.rei#L13),
-and it is often useful to look up metadata about the type (what fields does it
-have, what methods does it declare, what is its superclass, etc.) in the type
-environment, or
-[`tenv`](https://github.com/facebook/infer/blob/master/infer/src/IR/Tenv.rei#L37).
-
-A procedure description or
-[`procdesc`](https://github.com/facebook/infer/blob/master/infer/src/IR/Procdesc.rei)
-(sometimes abbreviated `pdesc`) is an abstraction of a procedure declaration: it
-stores the CFG of the procedure, its signature, its annotations, and so on.
-
-A procedure name or
-[`procname`](https://github.com/facebook/infer/blob/master/infer/src/IR/Procname.rei)
-(sometimes abbreviated `pname`) is an abstraction of a called procedure name.
-One procname may correspond to multiple (or zero) `procdesc`'s after resolution.
-
-## Framework-specific IR: `ProcCFG`, `ProcData`, and `extras`
-
-The abstract interpretation framework has a few additional constructs that are
-worth explaining.
-
-A
-[`ProcCfG`](https://github.com/facebook/infer/blob/master/infer/src/absint/procCfg.mli)
-represents the CFG of a _single_ procedure whereas (perhaps confusingly) a
-[`Cfg`](https://github.com/facebook/infer/blob/master/infer/src/IR/Cfg.rei) is
-the CFG for an entire file. A `ProcCfg` is really a customizable view of the
-underlying procedure CFG; we can get a view the CFG with its edges backward
-(`ProcCfg.Backward`), with or without exceptional edges (`Normal`/`Exceptional`,
-respectively), or with each node holding at most one instruction
-(`OneInstrPerNode`).
-
-[`ProcData`](https://github.com/facebook/infer/blob/master/infer/src/absint/procData.mli)
-is a container that holds all of the read-only information required to analyze a
-single procedure: procedure description, and `extras`. The `extras` are custom
-read-only data that are computed before analysis begins, and can be accessed
-from the transfer functions. Most often, no extras are required for analysis
-(`ProcData.empty_extras`), but it can be useful to stash information like a map
-from a formal to its
-[index](https://github.com/facebook/infer/blob/master/infer/src/quandary/TaintAnalysis.ml#L88)
-or an invariant
-[map](https://github.com/facebook/infer/blob/master/infer/src/backend/preanal.ml#L115)
-from a prior analysis in the extras.
-
-## How it works
-
-Coming soon.
-
-## Intro: abstract interpretation
-
-Coming soon.
-
-## How do I make an analysis compositional?
-
-Coming soon.
+To go deeper, jump to the [lab
+exercise](https://github.com/facebook/infer/blob/master/infer/src/labs/README.md)
+and to the [API documentation](internal-API/), e.g. for the
+[Absint](/odoc/next/infer/Absint.html) and
+[IR](/odoc/next/infer/IR.html) modules.
diff --git a/website/docs/04-adding-checkers.md b/website/docs/04-adding-checkers.md
deleted file mode 100644
index 18e4161d7..000000000
--- a/website/docs/04-adding-checkers.md
+++ /dev/null
@@ -1,210 +0,0 @@
----
-id: adding-checkers
-title: Simple intraprocedural checkers
----
-
-## How can I create my own checkers?
-
-Infer Checkers provide a framework to perform intra-procedural static analyses.
-Since this is an open source project, everyone is welcome to contribute with new
-great checkers. In this page, we will create a very basic checker - a detector
-for every time the output method `java.io.PrintStream.println` is called. This
-should be enough to get you started.
-
-## Before you start
-
-Make sure you are able to successfully build Infer and your developer
-environment is set up:
-
-```
-./build-infer.sh
-make devsetup
-```
-
-Get familiar with Infer checkers and run Infer with some examples:
-
-```
-infer run -- javac Hello.java
-```
-
-In addition, get familiar with the Control Flow Graph (CFG) that Infer generates
-for you:
-
-```
-infer run -g -- javac Hello.java
-dot -Tpdf infer-out/captured/Hello.java*/icfg.dot -o icfg.pdf
-open icfg.pdf
-```
-
-This will give you further information about the analysis that is being done,
-including the CFG in dot format. It is important that you understand the
-generated CFG since this is the abstraction of code that Checkers will analyze.
-
-Infer is built with [OCaml](https://ocaml.org). This is a programming language
-that combines both functional and imperative programming. If you are not
-familiar with OCaml, it might be hard at the beginning to understand the code.
-Take your time to review the
-[basics](https://ocaml.org/learn/tutorials/basics.html) and do some
-[exercises](https://ocaml.org/learn/tutorials/99problems.html).
-
-## Let's go
-
-The directory `infer/src/absint` contains utilities for the abstract
-interpretation framework that checkers are based on.
-
-Looking into `infer/src/checkers` we can find some simple checkers. Most of them
-are implemented as a module created from a `TransferFunctions` module that is
-turned into an analyzer by applying one of the `AbstractInterpreter.Make*`
-functors, together with a `checker` function that calls into it. You can start
-by copying the code for one of these and modify it (eg
-checkers/SimpleChecker.ml). For example:
-
-```ocaml
-module TransferFunctions = struct
-  ...
-  let exec_instr astate proc_data cfg_node (instr : Sil.instr) =
-    match instr with
-    | pattern ->
-        ST.report_error
-          proc_name
-          proc_desc
-          "CHECKERS_MY_SIMPLE_CHECKER"
-          location
-          "A description of my simple checker"
-    | _ -> astate
-end
-
-module Analyzer = AbstractInterpreter.Make (TransferFunctions)
-
-let checker {Callbacks.exe_env; summary; get_procs_in_file} : Summary.t =
-  let proc_name = Summary.get_proc_name summary in
-  let tenv = Exe_env.get_tenv exe_env proc_name in
-  let proc_data = ProcData.make_default summary tenv in
-  ignore (Analyzer.compute_post proc_data ~initial) ;
-  summary
-```
-
-Checkers implement a function that detects a given pattern for our specific
-checker and then calls `AbstractInterpreter.Make` to iterate over all the nodes
-of the CFG.
-
-So now we need to know how to create our pattern. As an example, consider the
-following:
-
-```ocaml
-Sil.Call (_, Sil.Const (Sil.Cfun pn), _, loc, _)
-```
-
-This pattern matches every function call. In our code, it would look like:
-
-```ocaml
-  let exec_instr astate proc_data cfg_node (instr : Sil.instr) =
-    match instr with
-    | Call (_, Const (Cfun pn), _, loc, _) ->
-        ST.report_error
-          proc_name
-          proc_desc
-          "CHECKERS_MY_SIMPLE_CHECKER"
-          location
-          "A description of my simple checker"
-    | _ -> astate
-```
-
-The `absint/PatternMatch.ml` module contains the
-`java_proc_name_with_class_method` function which we can use for matching the
-required pattern.
-
-Each node is represented using the type `instr` from the Smallfoot Intermediate
-Language (SIL). Take a look at `IR/Sil.mli` to get familiar with all the types.
-All source code languages supported by Infer are converted to this
-representation.
-
-In this particular example, `Sil.Call` has the following information:
-
-```ocaml
-Sil.Call (
-	list_of_return_values,
-	Sil.Const (Const.Cfun name_of_function),
-	list_of_arguments,
-	location,
-	call_flags
-)
-```
-
-I hope this looks straight forward. Argument `call_flags` holds information
-about the function, such as whether it is virtual or not. Again, this is
-specified in the file `Sil.mli`.
-
-The Checker we have written so far is able to detect every single function call.
-Now, we have to detect whether a specific function call is actually calling
-`java.io.PrintStream.println`.
-
-Let's try this:
-
-```ocaml
-  let is_println pln = match pln with
-    | Procname.Java pn_java ->
-        PatternMatch.java_proc_name_with_class_method
-          pn_java "java.io.PrintStream" "println"
-    | _ ->
-        false in
-
-  let exec_instr astate proc_data cfg_node (instr : Sil.instr) =
-    match instr with
-    | Call (_, Const (Cfun pn), _, loc, _) when is_println pn ->
-        ST.report_error
-          proc_name
-          proc_desc
-          "CHECKERS_MY_SIMPLE_CHECKER"
-          location
-          "A description of my simple checker"
-    | _ -> astate
-
-```
-
-Can you spot the difference? A new restriction was added to our pattern --
-`is_println` expression helps us to check whether the current method is a
-`java.io.PrintStream.println` method or not.
-
-So our implementation is done. Now we have to register it as an enabled Checker
-in `checkers/registerCheckers.ml`.
-
-Assuming the code is in SimpleCheckers.ml, you would register your checker as a
-_java_checker_ in `checkers/registerCheckers.ml` by adding it to the
-`all_checkers` list:
-
-```ocaml
-let all_checkers =
-  [ { name= "my simple checker"
-    ; active= true
-    ; callbacks= [(Procedure SimpleChecker.checker, Language.Java)] }
-  ; (* the rest of the list as it was there *)
-    ... ]
-```
-
-Build Infer with `./build-infer.sh` and your first Checker is ready!
-
-If you want you can try with this java example:
-
-```java
-/*Hello.java*/
-class Hello {
-	int println(){
-		return 0;
-	}
-	int test() {
-		String s = "Hello World";
-		System.out.println(s);
-		s = null;
-		println();
-		return s.length();
-	}
-}
-```
-
-Notice that only `System.out.println` is being detected.
-
-All set! You are ready to create your own Checkers! Infer is an open source
-project and you are more than welcome to contribute. Take a look at the
-[Github](https://github.com/facebook/infer/) page and feel free to fork or even
-open an issue if you're facing any trouble.
diff --git a/website/sidebars.js b/website/sidebars.js
index d7aa24300..28a879af1 100644
--- a/website/sidebars.js
+++ b/website/sidebars.js
@@ -32,7 +32,7 @@ module.exports = {
       "about-Infer",
       "separation-logic-and-bi-abduction",
     ],
-    Contribute: ["absint-framework", "adding-checkers", "internal-API"],
+    Contribute: ["absint-framework", "internal-API"],
     Versions: ["versions"],
   },
 };