[clang][docs][dataflow] Added an introduction to dataflow analysis
This documentation supports the dataflow analysis framework (see "[RFC]
A dataflow analysis framework for Clang AST" on cfe-dev).
Since the implementation of the framework has not been committed yet,
right now the doc describes dataflow analysis in general.
Since this is the first markdown document in clang/docs, I added support
for Markdown to clang/docs/conf.py in the same way as it is done in
llvm/docs.
Reviewed By: xazax.hun
Differential Revision: https://reviews.llvm.org/D114231
GitOrigin-RevId: ab31d003e16e483bff298ea2f28fec0f23e8eb79
diff --git a/docs/DataFlowAnalysisIntro.md b/docs/DataFlowAnalysisIntro.md
new file mode 100644
index 0000000..9aee197
--- /dev/null
+++ b/docs/DataFlowAnalysisIntro.md
@@ -0,0 +1,1000 @@
+# Data flow analysis: an informal introduction
+
+## Abstract
+
+This document introduces data flow analysis in an informal way. The goal is to
+give the reader an intuitive understanding of how it works, and show how it
+applies to a range of refactoring and bug finding problems.
+
+Data flow analysis is a well-established technique; it is described in many
+papers, books, and videos. If you would like a more formal, or a more thorough
+explanation of the concepts mentioned in this document, please refer to the
+following resources:
+
+* [The Lattice article in Wikipedia](https://en.wikipedia.org/wiki/Lattice_\(order\)).
+* Videos on the PacketPrep YouTube channel that introduce lattices and the
+ necessary background information:
+ [#20](https://www.youtube.com/watch?v=73j_FXBXGm8),
+ [#21](https://www.youtube.com/watch?v=b5sDjo9tfE8),
+ [#22](https://www.youtube.com/watch?v=saOG7Uooeho),
+ [#23](https://www.youtube.com/watch?v=3EAYX-wZH0g),
+ [#24](https://www.youtube.com/watch?v=KRkHwQtW6Cc),
+ [#25](https://www.youtube.com/watch?v=7Gwzsc4rAgw).
+* [Introduction to Dataflow Analysis](https://www.youtube.com/watch?v=OROXJ9-wUQE)
+* [Introduction to abstract interpretation](http://www.cs.tau.ac.il/~msagiv/courses/asv/absint-1.pdf).
+* [Introduction to symbolic execution](https://www.cs.umd.edu/~mwh/se-tutorial/symbolic-exec.pdf).
+* [Static Program Analysis by Anders Møller and Michael I. Schwartzbach](https://cs.au.dk/~amoeller/spa/).
+* [EXE: automatically generating inputs of death](https://css.csail.mit.edu/6.858/2020/readings/exe.pdf)
+ (a paper that successfully applies symbolic execution to real-world
+ software).
+
+## Data flow analysis
+
+### The purpose of data flow analysis
+
+Data flow analysis is a static analysis technique that proves facts about a
+program or its fragment. It can make conclusions about all paths through the
+program, while taking control flow into account and scaling to large programs.
+The basic idea is propagating facts about the program through the edges of the
+control flow graph (CFG) until a fixpoint is reached.
+
+### Sample problem and an ad-hoc solution
+
+We would like to explain data flow analysis while discussing an example. Let's
+imagine that we want to track possible values of an integer variable in our
+program. Here is how a human could annotate the code:
+
+```c++
+void Example(int n) {
+ int x = 0;
+ // x is {0}
+ if (n > 0) {
+ x = 5;
+ // x is {5}
+ } else {
+ x = 42;
+ // x is {42}
+ }
+ // x is {5; 42}
+ print(x);
+}
+```
+
+We use sets of integers to represent possible values of `x`. Local variables
+have unambiguous values between statements, so we annotate program points
+between statements with sets of possible values.
+
+Here is how we arrived at these annotations. Assigning a constant to `x` allows
+us to make a conclusion that `x` can only have one value. When control flow from
+the "then" and "else" branches joins, `x` can have either value.
+
+Abstract algebra provides a nice formalism that models this kind of structure,
+namely, a lattice. A join-semilattice is a partially ordered set, in which every
+two elements have a least upper bound (called a *join*).
+
+```
+join(a, b) ⩾ a and join(a, b) ⩾ b and join(x, x) = x
+```
+
+For this problem we will use the lattice of subsets of integers, with set
+inclusion relation as ordering and set union as a join.
+
+Lattices are often represented visually as Hasse diagrams. Here is a Hasse
+diagram for our lattice that tracks subsets of integers:
+
+
+
+Computing the join in the lattice corresponds to finding the lowest common
+ancestor (LCA) between two nodes in its Hasse diagram. There is a vast amount of
+literature on efficiently implementing LCA queries for a DAG, however Efficient
+Implementation of Lattice Operations (1989)
+([CiteSeerX](https://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.106.4911),
+[doi](https://doi.org/10.1145%2F59287.59293)) describes a scheme that
+particularly well-suited for programmatic implementation.
+
+### Too much information and "top" values
+
+Let's try to find the possible sets of values of `x` in a function that modifies
+`x` in a loop:
+
+```c++
+void ExampleOfInfiniteSets() {
+ int x = 0; // x is {0}
+ while (condition()) {
+ x += 1; // x is {0; 1; 2; …}
+ }
+ print(x); // x is {0; 1; 2; …}
+}
+```
+
+We have an issue: `x` can have any value greater than zero; that's an infinite
+set of values, if the program operated on mathematical integers. In C++ `int` is
+limited by `INT_MAX` so technically we have a set `{0; 1; …; INT_MAX}` which is
+still really big.
+
+To make our analysis practical to compute, we have to limit the amount of
+information that we track. In this case, we can, for example, arbitrarily limit
+the size of sets to 3 elements. If at a certain program point `x` has more than
+3 possible values, we stop tracking specific values at that program point.
+Instead, we denote possible values of `x` with the symbol `⊤` (pronounced "top"
+according to a convention in abstract algebra).
+
+```c++
+void ExampleOfTopWithALoop() {
+ int x = 0; // x is {0}
+ while (condition()) {
+ x += 1; // x is ⊤
+ }
+ print(x); // x is ⊤
+}
+```
+
+The statement "at this program point, `x`'s possible values are `⊤`" is
+understood as "at this program point `x` can have any value because we have too
+much information, or the information is conflicting".
+
+Note that we can get more than 3 possible values even without a loop:
+
+```c++
+void ExampleOfTopWithoutLoops(int n) {
+ int x = 0; // x is {0}
+ switch(n) {
+ case 0: x = 1; break; // x is {1}
+ case 1: x = 9; break; // x is {9}
+ case 2: x = 7; break; // x is {7}
+ default: x = 3; break; // x is {3}
+ }
+ // x is ⊤
+}
+```
+
+### Uninitialized variables and "bottom" values
+
+When `x` is declared but not initialized, it has no possible values. We
+represent this fact symbolically as `⊥` (pronounced "bottom").
+
+```c++
+void ExampleOfBottom() {
+ int x; // x is ⊥
+ x = 42; // x is {42}
+ print(x);
+}
+```
+
+Note that using values read from uninitialized variables is undefined behaviour
+in C++. Generally, compilers and static analysis tools can assume undefined
+behavior does not happen. We must model uninitialized variables only when we are
+implementing a checker that specifically is trying to find uninitialized reads.
+In this example we show how to model uninitialized variables only to demonstrate
+the concept of "bottom", and how it applies to possible value analysis. We
+describe an analysis that finds uninitialized reads in a section below.
+
+### A practical lattice that tracks sets of concrete values
+
+Taking into account all corner cases covered above, we can put together a
+lattice that we can use in practice to track possible values of integer
+variables. This lattice represents sets of integers with 1, 2, or 3 elements, as
+well as top and bottom. Here is a Hasse diagram for it:
+
+
+
+### Formalization
+
+Let's consider a slightly more complex example, and think about how we can
+compute the sets of possible values algorithmically.
+
+```c++
+void Example(int n) {
+ int x; // x is ⊥
+ if (n > 0) {
+ if (n == 42) {
+ x = 44; // x is {44}
+ } else {
+ x = 5; // x is {5}
+ }
+ print(x); // x is {44; 5}
+ } else {
+ x = n; // x is ⊤
+ }
+ print(x); // x is ⊤
+}
+```
+
+As humans, we understand the control flow from the program text. We used our
+understanding of control flow to find program points where two flows join.
+Formally, control flow is represented by a CFG (control flow graph):
+
+
+
+We can compute sets of possible values by propagating them through the CFG of
+the function:
+
+* When `x` is declared but not initialized, its possible values are `{}`. The
+ empty set plays the role of `⊥` in this lattice.
+
+* When `x` is assigned a concrete value, its possible set of values contains
+ just that specific value.
+
+* When `x` is assigned some unknown value, it can have any value. We represent
+ this fact as `⊤`.
+
+* When two control flow paths join, we compute the set union of incoming
+ values (limiting the number of elements to 3, representig larger sets as
+ `⊤`).
+
+The sets of possible values are influenced by:
+
+* Statements, for example, assignments.
+
+* Joins in control flow, for example, ones that appear at the end of "if"
+ statements.
+
+**Effects of statements** are modeled by what is formally known as a transfer
+function. A transfer function takes two arguments: the statement, and the state
+of `x` at the previous program point. It produces the state of `x` at the next
+program point. For example, the transfer function for assignment ignores the
+state at the previous program point:
+
+```c++
+// GIVEN: x is {42; 44}
+x = 0;
+// CONCLUSION: x is {0}
+```
+
+The transfer function for `+` performs arithmetic on every set member:
+
+```c++
+// GIVEN: x is {42, 44}
+x = x + 100;
+// CONCLUSION: x is {142, 144}
+```
+
+**Effects of control flow** are modeled by joining the knowledge from all
+possible previous program points.
+
+```c++
+if (...) {
+ ...
+ // GIVEN: x is {42}
+} else {
+ ...
+ // GIVEN: x is {44}
+}
+// CONCLUSION: x is {42; 44}
+```
+
+```c++
+// GIVEN: x is {42}
+while (...) {
+ ...
+ // GIVEN: x is {44}
+}
+// CONCLUSION: {42; 44}
+```
+
+The predicate that we marked "given" is usually called a precondition, and the
+conclusion is called a postcondition.
+
+In terms of the CFG, we join the information from all predecessor basic blocks.
+
+
+
+Putting it all together, to model the effects of a basic block we compute:
+
+```
+out = transfer(basic_block, join(in_1, in_2, ..., in_n))
+```
+
+(Note that there are other ways to write this equation that produce higher
+precision analysis results. The trick is to keep exploring the execution paths
+separately and delay joining until later. Hoowever, we won't discuss those
+variations here.)
+
+To make a conclusion about all paths through the program, we repeat this
+computation on all basic blocks until we reach a fixpoint. In other words, we
+keep propagating information through the CFG until the computed sets of values
+stop changing.
+
+If the lattice has a finite height and transfer functions are monotonic the
+algorithm is guaranteed to terminate. Each iteration of the algorithm can
+change computed values only to larger values from the lattice. In the worst
+case, all computed values become `⊤`, which is not very useful, but at least the
+analysis terminates at that point, because it can't change any of the values.
+
+Fixpoint iteration can be optimised by only reprocessing basic blocks which had
+one of their inputs changed on the previous iteration. This is typically
+implemented using a worklist queue. With this optimisation the time complexity
+becomes `O(m * |L|)`, where `m` is the number of basic blocks in the CFG and
+`|L|` is the size of lattice used by the analysis.
+
+## Symbolic execution: a very short informal introduction
+
+### Symbolic values
+
+In the previous example where we tried to figure out what values a variable can
+have, the analysis had to be seeded with a concrete value. What if there are no
+assignments of concrete values in the program? We can still deduce some
+interesting information by representing unknown input values symbolically, and
+computing results as symbolic expressions:
+
+```c++
+void PrintAbs(int x) {
+ int result;
+ if (x >= 0) {
+ result = x; // result is {x}
+ } else {
+ result = -x; // result is {-x}
+ }
+ print(result); // result is {x; -x}
+}
+```
+
+We can't say what specific value gets printed, but we know that it is either `x`
+or `-x`.
+
+Dataflow analysis is an istance of abstract interpretation, and does not dictate
+how exactly the lattice and transfer functions should be designed, beyond the
+necessary conditions for the analysis to converge. Nevertheless, we can use
+symbolic execution ideas to guide our design of the lattice and transfer
+functions: lattice values can be symbolic expressions, and transfer functions
+can construct more complex symbolic expressions from symbolic expressions that
+represent arguments. See [this StackOverflow
+discussion](https://cstheory.stackexchange.com/questions/19708/symbolic-execution-is-a-case-of-abstract-interpretation)
+for a further comparison of abstract interpretation and symbolic execution.
+
+### Flow condition
+
+A human can say about the previous example that the function returns `x` when
+`x >= 0`, and `-x` when `x < 0`. We can make this conclusion programmatically by
+tracking a flow condition. A flow condition is a predicate written in terms of
+the program state that is true at a specific program point regardless of the
+execution path that led to this statement. For example, the flow condition for
+the program point right before evaluating `result = x` is `x >= 0`.
+
+If we enhance the lattice to be a set of pairs of values and predicates, the
+dataflow analysis computes the following values:
+
+```c++
+void PrintAbs(int x) {
+ int result;
+ if (x >= 0) {
+ // Flow condition: x >= 0.
+ result = x; // result is {x if x >= 0}
+ } else {
+ // Flow condition: x < 0.
+ result = -x; // result is {-x if x < 0}
+ }
+ print(result); // result is {x if x >= 0; -x if x < 0}
+}
+```
+
+Of course, in a program with loops, symbolic expressions for flow conditions can
+grow unbounded. A practical static analysis system must control this growth to
+keep the symbolic representations manageable and ensure that the data flow
+analysis terminates. For example, it can use a constraint solver to prune
+impossible flow conditions, and/or it can abstract them, losing precision, after
+their symbolic representations grow beyond some threshold. This is similar to
+how we had to limit the sizes of computed sets of possible values to 3 elements.
+
+### Symbolic pointers
+
+This approach proves to be particularly useful for modeling pointer values,
+since we don't care about specific addresses but just want to give a unique
+identifier to a memory location.
+
+```c++
+void ExampleOfSymbolicPointers(bool b) {
+ int x = 0; // x is {0}
+ int* ptr = &x; // x is {0} ptr is {&x}
+ if (b) {
+ *ptr = 42; // x is {42} ptr is {&x}
+ }
+ print(x); // x is {0; 42} ptr is {&x}
+}
+```
+
+## Example: finding output parameters
+
+Let's explore how data flow analysis can help with a problem that is hard to
+solve with other tools in Clang.
+
+### Problem description
+
+Output parameters are function parameters of pointer or reference type whose
+pointee is completely overwritten by the function, and not read before it is
+overwritten. They are common in pre-C++11 code due to the absence of move
+semantics. In modern C++ output parameters are non-idiomatic, and return values
+are used instead.
+
+Imagine that we would like to refactor output parameters to return values to
+modernize old code. The first step is to identify refactoring candidates through
+static analysis.
+
+For example, in the following code snippet the pointer `c` is an output
+parameter:
+
+```c++
+struct Customer {
+ int account_id;
+ std::string name;
+}
+
+void GetCustomer(Customer *c) {
+ c->account_id = ...;
+ if (...) {
+ c->name = ...;
+ } else {
+ c->name = ...;
+ }
+}
+```
+
+We would like to refactor this code into:
+
+```c++
+Customer GetCustomer() {
+ Customer c;
+ c.account_id = ...;
+ if (...) {
+ c.name = ...;
+ } else {
+ c.name = ...;
+ }
+ return c;
+}
+```
+
+However, in the function below the parameter `c` is not an output parameter
+because its field `name` is not overwritten on every path through the function.
+
+```c++
+void GetCustomer(Customer *c) {
+ c->account_id = ...;
+ if (...) {
+ c->name = ...;
+ }
+}
+```
+
+The code also cannot read the value of the parameter before overwriting it:
+
+```c++
+void GetCustomer(Customer *c) {
+ use(c->account_id);
+ c->name = ...;
+ c->account_id = ...;
+}
+```
+
+Functions that escape the pointer also block the refactoring:
+
+```c++
+Customer* kGlobalCustomer;
+
+void GetCustomer(Customer *c) {
+ c->name = ...;
+ c->account_id = ...;
+ kGlobalCustomer = c;
+}
+```
+
+To identify a candidate function for refactoring, we need to do the following:
+
+* Find a function with a non-const pointer or reference parameter.
+
+* Find the definition of that function.
+
+* Prove that the function completely overwrites the pointee on all paths
+ before returning.
+
+* Prove that the function reads the pointee only after overwriting it.
+
+* Prove that the function does not persist the pointer in a data structure
+ that is live after the function returns.
+
+There are also requirements that all usage sites of the candidate function must
+satisfy, for example, that function arguments do not alias, that users are not
+taking the address of the function, and so on. Let's consider verifying usage
+site conditions to be a separate static analysis problem.
+
+### Lattice design
+
+To analyze the function body we can use a lattice which consists of normal
+states and failure states. A normal state describes program points where we are
+sure that no behaviors that block the refactoring have occurred. Normal states
+keep track of all parameter's member fields that are known to be overwritten on
+every path from function entry to the corresponding program point. Failure
+states accumulate observed violations (unsafe reads and pointer escapes) that
+block the refactoring.
+
+In the partial order of the lattice failure states compare greater than normal
+states, which guarantees that they "win" when joined with normal states. Order
+between failure states is determined by inclusion relation on the set of
+accumulated violations (lattice's `⩽` is `⊆` on the set of violations). Order
+between normal states is determined by reversed inclusion relation on the set of
+overwritten parameter's member fields (lattice's `⩽` is `⊇` on the set of
+overwritten fields).
+
+
+
+To determine whether a statement reads or writes a field we can implement
+symbolic evaluation of `DeclRefExpr`s, `LValueToRValue` casts, pointer
+dereference operator and `MemberExpr`s.
+
+### Using data flow results to identify output parameters
+
+Let's take a look at how we use data flow analysis to identify an output
+parameter. The refactoring can be safely done when the data flow algorithm
+computes a normal state with all of the fields proven to be overwritten in the
+exit basic block of the function.
+
+```c++
+struct Customer {
+ int account_id;
+ std::string name;
+};
+
+void GetCustomer(Customer* c) {
+ // Overwritten: {}
+ c->account_id = ...; // Overwritten: {c->account_id}
+ if (...) {
+ c->name = ...; // Overwritten: {c->account_id, c->name}
+ } else {
+ c->name = ...; // Overwritten: {c->account_id, c->name}
+ }
+ // Overwritten: {c->account_id, c->name}
+}
+```
+
+When the data flow algorithm computes a normal state, but not all fields are
+proven to be overwritten we can't perform the refactoring.
+
+```c++
+void target(bool b, Customer* c) {
+ // Overwritten: {}
+ if (b) {
+ c->account_id = 42; // Overwritten: {c->account_id}
+ } else {
+ c->name = "Konrad"; // Overwritten: {c->name}
+ }
+ // Overwritten: {}
+}
+```
+
+Similarly, when the data flow algorithm computes a failure state, we also can't
+perform the refactoring.
+
+```c++
+Customer* kGlobalCustomer;
+
+void GetCustomer(Customer* c) {
+ // Overwritten: {}
+ c->account_id = ...; // Overwritten: {c->account_id}
+ if (...) {
+ print(c->name); // Unsafe read
+ } else {
+ kGlobalCustomer = c; // Pointer escape
+ }
+ // Unsafe read, Pointer escape
+}
+```
+
+## Example: finding dead stores
+
+Let's say we want to find redundant stores, because they indicate potential
+bugs.
+
+```c++
+x = GetX();
+x = GetY();
+```
+
+The first store to `x` is never read, probably there is a bug.
+
+The implementation of dead store analysis is very similar to output parameter
+analysis: we need to track stores and loads, and find stores that were never
+read.
+
+[Liveness analysis](https://en.wikipedia.org/wiki/Live_variable_analysis) is a
+generalization of this idea, which is often used to answer many related
+questions, for example:
+
+* finding dead stores,
+* finding uninitialized variables,
+* finding a good point to deallocate memory,
+* finding out if it would be safe to move an object.
+
+## Example: definitive initialization
+
+Definitive initialization proves that variables are known to be initialized when
+read. If we find a variable which is read when not initialized then we generate
+a warning.
+
+```c++
+void Init() {
+ int x; // x is uninitialized
+ if (cond()) {
+ x = 10; // x is initialized
+ } else {
+ x = 20; // x is initialized
+ }
+ print(x); // x is initialized
+}
+```
+
+```c++
+void Uninit() {
+ int x; // x is uninitialized
+ if (cond()) {
+ x = 10; // x is initialized
+ }
+ print(x); // x is maybe uninitialized, x is being read, report a bug.
+}
+```
+
+For this purpose we can use lattice in a form of a mapping from variable
+declarations to initialization states; each initialization state is represented
+by the followingn lattice:
+
+
+
+A lattice element could also capture the source locations of the branches that
+lead us to the corresponding program point. Diagnostics would use this
+information to show a sample buggy code path to the user.
+
+## Example: refactoring raw pointers to `unique_ptr`
+
+Modern idiomatic C++ uses smart pointers to express memory ownership, however in
+pre-C++11 code one can often find raw pointers that own heap memory blocks.
+
+Imagine that we would like to refactor raw pointers that own memory to
+`unique_ptr`. There are multiple ways to design a data flow analysis for this
+problem; let's look at one way to do it.
+
+For example, we would like to refactor the following code that uses raw
+pointers:
+
+```c++
+void UniqueOwnership1() {
+ int *pi = new int;
+ if (...) {
+ Borrow(pi);
+ delete pi;
+ } else {
+ TakeOwnership(pi);
+ }
+}
+```
+
+into code that uses `unique_ptr`:
+
+```c++
+void UniqueOwnership1() {
+ auto pi = std::make_unique<int>();
+ if (...) {
+ Borrow(pi.get());
+ } else {
+ TakeOwnership(pi.release());
+ }
+}
+```
+
+This problem can be solved with a lattice in form of map from value declarations
+to pointer states:
+
+
+
+We can perform the refactoring if at the exit of a function `pi` is
+`Compatible`.
+
+```c++
+void UniqueOwnership1() {
+ int *pi; // pi is Compatible
+ pi = new int; // pi is Defined
+ if (...) {
+ Borrow(pi); // pi is Defined
+ delete pi; // pi is Compatible
+ } else {
+ TakeOwnership(pi); // pi is Compatible
+ }
+ // pi is Compatible
+}
+```
+
+Let's look at an example where the raw pointer owns two different memory blocks:
+
+```c++
+void UniqueOwnership2() {
+ int *pi = new int; // pi is Defined
+ Borrow(pi);
+ delete pi; // pi is Compatible
+ if (smth) {
+ pi = new int; // pi is Defined
+ Borrow(pi);
+ delete pi; // pi is Compatible
+ }
+ // pi is Compatible
+}
+```
+
+It can be refactored to use `unique_ptr` like this:
+
+```c++
+void UniqueOwnership2() {
+ auto pi = make_unique<int>();
+ Borrow(pi);
+ if (smth) {
+ pi = make_unique<int>();
+ Borrow(pi);
+ }
+}
+```
+
+In the following example, the raw pointer is used to access the heap object
+after the ownership has been transferred.
+
+```c++
+void UniqueOwnership3() {
+ int *pi = new int; // pi is Defined
+ if (...) {
+ Borrow(pi);
+ delete pi; // pi is Compatible
+ } else {
+ vector<unique_ptr<int>> v = {std::unique_ptr(pi)}; // pi is Compatible
+ print(*pi);
+ use(v);
+ }
+ // pi is Compatible
+}
+```
+
+We can refactor this code to use `unique_ptr`, however we would have to
+introduce a non-owning pointer variable, since we can't use the moved-from
+`unique_ptr` to access the object:
+
+```c++
+void UniqueOwnership3() {
+ std::unique_ptr<int> pi = std::make_unique<int>();
+ if (...) {
+ Borrow(pi);
+ } else {
+ int *pi_non_owning = pi.get();
+ vector<unique_ptr<int>> v = {std::move(pi)};
+ print(*pi_non_owning);
+ use(v);
+ }
+}
+```
+
+If the original code didn't call `delete` at the very end of the function, then
+our refactoring may change the point at which we run the destructor and release
+memory. Specifically, if there is some user code after `delete`, then extending
+the lifetime of the object until the end of the function may hold locks for
+longer than necessary, introduce memory overhead etc.
+
+One solution is to always replace `delete` with a call to `reset()`, and then
+perform another analysis that removes unnecessary `reset()` calls.
+
+```c++
+void AddedMemoryOverhead() {
+ HugeObject *ho = new HugeObject();
+ use(ho);
+ delete ho; // Release the large amount of memory quickly.
+ LongRunningFunction();
+}
+```
+
+This analysis will refuse to refactor code that mixes borrowed pointer values
+and unique ownership. In the following code, `GetPtr()` returns a borrowed
+pointer, which is assigned to `pi`. Then, `pi` is used to hold a uniquely-owned
+pointer. We don't distinguish between these two assignments, and we want each
+assignment to be paired with a corresponding sink; otherwise, we transition the
+pointer to a `Conflicting` state, like in this example.
+
+```c++
+void ConflictingOwnership() {
+ int *pi; // pi is Compatible
+ pi = GetPtr(); // pi is Defined
+ Borrow(pi); // pi is Defined
+
+ pi = new int; // pi is Conflicting
+ Borrow(pi);
+ delete pi;
+ // pi is Conflicting
+}
+```
+
+We could still handle this case by finding a maximal range in the code where
+`pi` could be in the Compatible state, and only refactoring that part.
+
+```c++
+void ConflictingOwnership() {
+ int *pi;
+ pi = GetPtr();
+ Borrow(pi);
+
+ std::unique_ptr<int> pi_unique = std::make_unique<int>();
+ Borrow(pi_unique.get());
+}
+```
+
+## Example: finding redundant branch conditions
+
+In the code below `b1` should not be checked in both the outer and inner "if"
+statements. It is likely there is a bug in this code.
+
+```c++
+int F(bool b1, bool b2) {
+ if (b1) {
+ f();
+ if (b1 && b2) { // Check `b1` again -- unnecessary!
+ g();
+ }
+ }
+}
+```
+
+A checker that finds this pattern syntactically is already implemented in
+ClangTidy using AST matchers (`bugprone-redundant-branch-condition`).
+
+To implement it using the data flow analysis framework, we can produce a warning
+if any part of the branch condition is implied by the flow condition.
+
+```c++
+int F(bool b1, bool b2) {
+ // Flow condition: true.
+ if (b1) {
+ // Flow condition: b1.
+ f();
+ if (b1 && b2) { // `b1` is implied by the flow condition.
+ g();
+ }
+ }
+}
+```
+
+One way to check this implication is to use a SAT solver. Without a SAT solver,
+we could keep the flow condition in the CNF form and then it would be easy to
+check the implication.
+
+## Example: finding unchecked `std::optional` unwraps
+
+Calling `optional::value()` is only valid if `optional::has_value()` is true. We
+want to show that when `x.value()` is executed, the flow condition implies
+`x.has_value()`.
+
+In the example below `x.value()` is accessed safely because it is guarded by the
+`x.has_value()` check.
+
+```c++
+void Example(std::optional<int> &x) {
+ if (x.has_value()) {
+ use(x.value());
+ }
+}
+```
+
+While entering the if branch we deduce that `x.has_value()` is implied by the
+flow condition.
+
+```c++
+void Example(std::optional<int> x) {
+ // Flow condition: true.
+ if (x.has_value()) {
+ // Flow condition: x.has_value() == true.
+ use(x.value());
+ }
+ // Flow condition: true.
+}
+```
+
+We also need to prove that `x` is not modified between check and value access.
+The modification of `x` may be very subtle:
+
+```c++
+void F(std::optional<int> &x);
+
+void Example(std::optional<int> &x) {
+ if (x.has_value()) {
+ // Flow condition: x.has_value() == true.
+ unknown_function(x); // may change x.
+ // Flow condition: true.
+ use(x.value());
+ }
+}
+```
+
+## Example: finding dead code behind A/B experiment flags
+
+Finding dead code is a classic application of data flow analysis.
+
+Unused flags for A/B experiment hide dead code. However, this flavor of dead
+code is invisible to the compiler because the flag can be turned on at any
+moment.
+
+We could make a tool that deletes experiment flags. The user tells us which flag
+they want to delete, and we assume that the it's value is a given constant.
+
+For example, the user could use the tool to remove `example_flag` from this
+code:
+
+```c++
+DEFINE_FLAG(std::string, example_flag, "", "A sample flag.");
+
+void Example() {
+ bool x = GetFlag(FLAGS_example_flag).empty();
+ f();
+ if (x) {
+ g();
+ } else {
+ h();
+ }
+}
+```
+
+The tool would simplify the code to:
+
+```c++
+void Example() {
+ f();
+ g();
+}
+```
+
+We can solve this problem with a classic constant propagation lattice combined
+with symbolic evaluation.
+
+## Example: finding inefficient usages of associative containers
+
+Real-world code often accidentally performs repeated lookups in associative
+containers:
+
+```c++
+map<int, Employee> xs;
+xs[42]->name = "...";
+xs[42]->title = "...";
+```
+
+To find the above inefficiency we can use the available expressions analysis to
+understand that `m[42]` is evaluated twice.
+
+```c++
+map<int, Employee> xs;
+Employee &e = xs[42];
+e->name = "...";
+e->title = "...";
+```
+
+We can also track the `m.contains()` check in the flow condition to find
+redundant checks, like in the example below.
+
+```c++
+std::map<int, Employee> xs;
+if (!xs.contains(42)) {
+ xs.insert({42, someEmployee});
+}
+```
+
+## Example: refactoring types that implicitly convert to each other
+
+Refactoring one strong type to another is difficult, but the compiler can help:
+once you refactor one reference to the type, the compiler will flag other places
+where this information flows with type mismatch errors. Unfortunately this
+strategy does not work when you are refactoring types that implicitly convert to
+each other, for example, replacing `int32_t` with `int64_t`.
+
+Imagine that we want to change user IDs from 32 to 64-bit integers. In other
+words, we need to find all integers tainted with user IDs. We can use data flow
+analysis to implement taint analysis.
+
+```c++
+void UseUser(int32_t user_id) {
+ int32_t id = user_id;
+ // Variable `id` is tainted with a user ID.
+ ...
+}
+```
+
+Taint analysis is very well suited to this problem because the program rarely
+branches on user IDs, and almost certainly does not perform any computation
+(like arithmetic).
diff --git a/docs/DataFlowAnalysisIntroImages/CFGExample.svg b/docs/DataFlowAnalysisIntroImages/CFGExample.svg
new file mode 100644
index 0000000..8e81576
--- /dev/null
+++ b/docs/DataFlowAnalysisIntroImages/CFGExample.svg
@@ -0,0 +1,520 @@
+<?xml version="1.0" encoding="UTF-8" standalone="no"?>
+<svg
+ xmlns:dc="http://purl.org/dc/elements/1.1/"
+ xmlns:cc="http://creativecommons.org/ns#"
+ xmlns:rdf="http://www.w3.org/1999/02/22-rdf-syntax-ns#"
+ xmlns:svg="http://www.w3.org/2000/svg"
+ xmlns="http://www.w3.org/2000/svg"
+ xmlns:sodipodi="http://sodipodi.sourceforge.net/DTD/sodipodi-0.dtd"
+ xmlns:inkscape="http://www.inkscape.org/namespaces/inkscape"
+ id="svg8"
+ version="1.1"
+ viewBox="0 0 220 210"
+ height="210mm"
+ width="220mm">
+ <defs
+ id="defs2">
+ <marker
+ inkscape:isstock="true"
+ style="overflow:visible"
+ id="Arrow2Lend"
+ refX="0"
+ refY="0"
+ orient="auto"
+ inkscape:stockid="Arrow2Lend">
+ <path
+ transform="matrix(-1.1,0,0,-1.1,-1.1,0)"
+ d="M 8.7185878,4.0337352 -2.2072895,0.01601326 8.7185884,-4.0017078 c -1.7454984,2.3720609 -1.7354408,5.6174519 -6e-7,8.035443 z"
+ style="fill:#000000;fill-opacity:1;fill-rule:evenodd;stroke:#000000;stroke-width:0.625;stroke-linejoin:round;stroke-opacity:1"
+ id="path1109" />
+ </marker>
+ <marker
+ inkscape:isstock="true"
+ style="overflow:visible"
+ id="Arrow1Lend"
+ refX="0"
+ refY="0"
+ orient="auto"
+ inkscape:stockid="Arrow1Lend">
+ <path
+ transform="matrix(-0.8,0,0,-0.8,-10,0)"
+ style="fill:#000000;fill-opacity:1;fill-rule:evenodd;stroke:#000000;stroke-width:1pt;stroke-opacity:1"
+ d="M 0,0 5,-5 -12.5,0 5,5 Z"
+ id="path1091" />
+ </marker>
+ <marker
+ inkscape:stockid="Arrow2Lend"
+ orient="auto"
+ refY="0"
+ refX="0"
+ id="Arrow2Lend-5"
+ style="overflow:visible"
+ inkscape:isstock="true">
+ <path
+ id="path1109-7"
+ style="fill:#000000;fill-opacity:1;fill-rule:evenodd;stroke:#000000;stroke-width:0.625;stroke-linejoin:round;stroke-opacity:1"
+ d="M 8.7185878,4.0337352 -2.2072895,0.01601326 8.7185884,-4.0017078 c -1.7454984,2.3720609 -1.7354408,5.6174519 -6e-7,8.035443 z"
+ transform="matrix(-1.1,0,0,-1.1,-1.1,0)" />
+ </marker>
+ <marker
+ inkscape:stockid="Arrow2Lend"
+ orient="auto"
+ refY="0"
+ refX="0"
+ id="Arrow2Lend-6"
+ style="overflow:visible"
+ inkscape:isstock="true">
+ <path
+ id="path1109-77"
+ style="fill:#000000;fill-opacity:1;fill-rule:evenodd;stroke:#000000;stroke-width:0.625;stroke-linejoin:round;stroke-opacity:1"
+ d="M 8.7185878,4.0337352 -2.2072895,0.01601326 8.7185884,-4.0017078 c -1.7454984,2.3720609 -1.7354408,5.6174519 -6e-7,8.035443 z"
+ transform="matrix(-1.1,0,0,-1.1,-1.1,0)" />
+ </marker>
+ <marker
+ inkscape:stockid="Arrow2Lend"
+ orient="auto"
+ refY="0"
+ refX="0"
+ id="Arrow2Lend-1"
+ style="overflow:visible"
+ inkscape:isstock="true">
+ <path
+ id="path1109-0"
+ style="fill:#000000;fill-opacity:1;fill-rule:evenodd;stroke:#000000;stroke-width:0.625;stroke-linejoin:round;stroke-opacity:1"
+ d="M 8.7185878,4.0337352 -2.2072895,0.01601326 8.7185884,-4.0017078 c -1.7454984,2.3720609 -1.7354408,5.6174519 -6e-7,8.035443 z"
+ transform="matrix(-1.1,0,0,-1.1,-1.1,0)" />
+ </marker>
+ <marker
+ inkscape:stockid="Arrow2Lend"
+ orient="auto"
+ refY="0"
+ refX="0"
+ id="Arrow2Lend-8"
+ style="overflow:visible"
+ inkscape:isstock="true">
+ <path
+ id="path1109-73"
+ style="fill:#000000;fill-opacity:1;fill-rule:evenodd;stroke:#000000;stroke-width:0.625;stroke-linejoin:round;stroke-opacity:1"
+ d="M 8.7185878,4.0337352 -2.2072895,0.01601326 8.7185884,-4.0017078 c -1.7454984,2.3720609 -1.7354408,5.6174519 -6e-7,8.035443 z"
+ transform="matrix(-1.1,0,0,-1.1,-1.1,0)" />
+ </marker>
+ <marker
+ inkscape:stockid="Arrow2Lend"
+ orient="auto"
+ refY="0"
+ refX="0"
+ id="Arrow2Lend-81"
+ style="overflow:visible"
+ inkscape:isstock="true">
+ <path
+ id="path1109-8"
+ style="fill:#000000;fill-opacity:1;fill-rule:evenodd;stroke:#000000;stroke-width:0.625;stroke-linejoin:round;stroke-opacity:1"
+ d="M 8.7185878,4.0337352 -2.2072895,0.01601326 8.7185884,-4.0017078 c -1.7454984,2.3720609 -1.7354408,5.6174519 -6e-7,8.035443 z"
+ transform="matrix(-1.1,0,0,-1.1,-1.1,0)" />
+ </marker>
+ <marker
+ inkscape:stockid="Arrow2Lend"
+ orient="auto"
+ refY="0"
+ refX="0"
+ id="Arrow2Lend-7"
+ style="overflow:visible"
+ inkscape:isstock="true">
+ <path
+ id="path1109-5"
+ style="fill:#000000;fill-opacity:1;fill-rule:evenodd;stroke:#000000;stroke-width:0.625;stroke-linejoin:round;stroke-opacity:1"
+ d="M 8.7185878,4.0337352 -2.2072895,0.01601326 8.7185884,-4.0017078 c -1.7454984,2.3720609 -1.7354408,5.6174519 -6e-7,8.035443 z"
+ transform="matrix(-1.1,0,0,-1.1,-1.1,0)" />
+ </marker>
+ <marker
+ inkscape:stockid="Arrow2Lend"
+ orient="auto"
+ refY="0"
+ refX="0"
+ id="Arrow2Lend-2"
+ style="overflow:visible"
+ inkscape:isstock="true">
+ <path
+ id="path1109-6"
+ style="fill:#000000;fill-opacity:1;fill-rule:evenodd;stroke:#000000;stroke-width:0.625;stroke-linejoin:round;stroke-opacity:1"
+ d="M 8.7185878,4.0337352 -2.2072895,0.01601326 8.7185884,-4.0017078 c -1.7454984,2.3720609 -1.7354408,5.6174519 -6e-7,8.035443 z"
+ transform="matrix(-1.1,0,0,-1.1,-1.1,0)" />
+ </marker>
+ <marker
+ inkscape:stockid="Arrow2Lend"
+ orient="auto"
+ refY="0"
+ refX="0"
+ id="Arrow2Lend-83"
+ style="overflow:visible"
+ inkscape:isstock="true">
+ <path
+ id="path1109-88"
+ style="fill:#000000;fill-opacity:1;fill-rule:evenodd;stroke:#000000;stroke-width:0.625;stroke-linejoin:round;stroke-opacity:1"
+ d="M 8.7185878,4.0337352 -2.2072895,0.01601326 8.7185884,-4.0017078 c -1.7454984,2.3720609 -1.7354408,5.6174519 -6e-7,8.035443 z"
+ transform="matrix(-1.1,0,0,-1.1,-1.1,0)" />
+ </marker>
+ <marker
+ inkscape:stockid="Arrow2Lend"
+ orient="auto"
+ refY="0"
+ refX="0"
+ id="Arrow2Lend-0"
+ style="overflow:visible"
+ inkscape:isstock="true">
+ <path
+ id="path1109-81"
+ style="fill:#000000;fill-opacity:1;fill-rule:evenodd;stroke:#000000;stroke-width:0.625;stroke-linejoin:round;stroke-opacity:1"
+ d="M 8.7185878,4.0337352 -2.2072895,0.01601326 8.7185884,-4.0017078 c -1.7454984,2.3720609 -1.7354408,5.6174519 -6e-7,8.035443 z"
+ transform="matrix(-1.1,0,0,-1.1,-1.1,0)" />
+ </marker>
+ <marker
+ inkscape:stockid="Arrow2Lend"
+ orient="auto"
+ refY="0"
+ refX="0"
+ id="Arrow2Lend-15"
+ style="overflow:visible"
+ inkscape:isstock="true">
+ <path
+ id="path1109-67"
+ style="fill:#000000;fill-opacity:1;fill-rule:evenodd;stroke:#000000;stroke-width:0.625;stroke-linejoin:round;stroke-opacity:1"
+ d="M 8.7185878,4.0337352 -2.2072895,0.01601326 8.7185884,-4.0017078 c -1.7454984,2.3720609 -1.7354408,5.6174519 -6e-7,8.035443 z"
+ transform="matrix(-1.1,0,0,-1.1,-1.1,0)" />
+ </marker>
+ </defs>
+ <g
+ id="layer1"
+ inkscape:groupmode="layer"
+ inkscape:label="Layer 1">
+ <rect
+ y="2.6458333"
+ x="55.5625"
+ height="10.583333"
+ width="42.333332"
+ id="rect12"
+ style="fill:none;stroke:#000000;stroke-width:0.265;stroke-miterlimit:4;stroke-dasharray:none;stroke-dashoffset:0;stroke-opacity:1" />
+ <text
+ id="text839"
+ y="9.2361279"
+ x="76.561562"
+ style="font-size:4.93889px;line-height:1;font-family:sans-serif;text-align:center;word-spacing:0px;text-anchor:middle;stroke-width:0.264583"
+ xml:space="preserve"><tspan
+ style="font-size:4.93889px;text-align:center;text-anchor:middle;stroke-width:0.264583"
+ y="9.2361279"
+ x="76.561562"
+ id="tspan837"
+ sodipodi:role="line">Entry</tspan></text>
+ <rect
+ style="fill:none;stroke:#000000;stroke-width:0.264999;stroke-miterlimit:4;stroke-dasharray:none;stroke-dashoffset:0;stroke-opacity:1"
+ id="rect12-8"
+ width="52.916668"
+ height="26.458334"
+ x="50.270832"
+ y="23.812498" />
+ <text
+ xml:space="preserve"
+ style="font-size:4.9389px;line-height:1.1;font-family:sans-serif;text-align:start;word-spacing:0px;text-anchor:start;stroke-width:0.264583"
+ x="54.303524"
+ y="30.288889"
+ id="text839-6"><tspan
+ sodipodi:role="line"
+ id="tspan837-3"
+ x="54.303524"
+ y="30.288889"
+ style="font-style:normal;font-variant:normal;font-weight:normal;font-stretch:normal;font-size:4.9389px;font-family:monospace;-inkscape-font-specification:monospace;font-variant-ligatures:normal;font-variant-caps:normal;font-variant-numeric:normal;font-variant-east-asian:normal;text-align:start;text-anchor:start;stroke-width:0.264583">// Pre: x is ⊥</tspan><tspan
+ id="tspan876"
+ sodipodi:role="line"
+ x="54.303524"
+ y="35.772423"
+ style="font-style:normal;font-variant:normal;font-weight:normal;font-stretch:normal;font-size:4.9389px;font-family:monospace;-inkscape-font-specification:monospace;font-variant-ligatures:normal;font-variant-caps:normal;font-variant-numeric:normal;font-variant-east-asian:normal;text-align:start;text-anchor:start;stroke-width:0.264583">int x;</tspan><tspan
+ id="tspan878"
+ sodipodi:role="line"
+ x="54.303524"
+ y="41.255955"
+ style="font-style:normal;font-variant:normal;font-weight:normal;font-stretch:normal;font-size:4.9389px;font-family:monospace;-inkscape-font-specification:monospace;font-variant-ligatures:normal;font-variant-caps:normal;font-variant-numeric:normal;font-variant-east-asian:normal;text-align:start;text-anchor:start;stroke-width:0.264583">if (n > 0)</tspan><tspan
+ id="tspan874"
+ sodipodi:role="line"
+ x="54.303524"
+ y="47.197174"
+ style="font-style:normal;font-variant:normal;font-weight:normal;font-stretch:normal;font-size:4.9389px;font-family:monospace;-inkscape-font-specification:monospace;font-variant-ligatures:normal;font-variant-caps:normal;font-variant-numeric:normal;font-variant-east-asian:normal;text-align:start;text-anchor:start;stroke-width:0.264583">// Post: x is ⊥</tspan></text>
+ <rect
+ y="92.604164"
+ x="2.6458302"
+ height="21.166666"
+ width="52.916668"
+ id="rect12-8-6"
+ style="fill:none;stroke:#000000;stroke-width:0.264999;stroke-miterlimit:4;stroke-dasharray:none;stroke-dashoffset:0;stroke-opacity:1" />
+ <text
+ id="text839-6-0"
+ y="99.405327"
+ x="6.154747"
+ style="font-size:4.9389px;line-height:1.1;font-family:sans-serif;text-align:start;word-spacing:0px;text-anchor:start;stroke-width:0.264583"
+ xml:space="preserve"><tspan
+ style="font-style:normal;font-variant:normal;font-weight:normal;font-stretch:normal;font-size:4.9389px;font-family:monospace;-inkscape-font-specification:monospace;text-align:start;text-anchor:start;stroke-width:0.264583"
+ y="99.405327"
+ x="6.154747"
+ id="tspan837-3-1"
+ sodipodi:role="line">// Pre: x is ⊥</tspan><tspan
+ style="font-style:normal;font-variant:normal;font-weight:normal;font-stretch:normal;font-size:4.9389px;font-family:monospace;-inkscape-font-specification:monospace;text-align:start;text-anchor:start;stroke-width:0.264583"
+ y="104.88886"
+ x="6.154747"
+ sodipodi:role="line"
+ id="tspan878-2">x = n;</tspan><tspan
+ style="font-style:normal;font-variant:normal;font-weight:normal;font-stretch:normal;font-size:4.9389px;font-family:monospace;-inkscape-font-specification:monospace;text-align:start;text-anchor:start;stroke-width:0.264583"
+ y="110.37239"
+ x="6.154747"
+ sodipodi:role="line"
+ id="tspan874-3">// Post: x is ⊤</tspan></text>
+ <rect
+ y="60.854168"
+ x="121.70833"
+ height="21.166666"
+ width="52.916668"
+ id="rect12-8-3"
+ style="fill:none;stroke:#000000;stroke-width:0.264999;stroke-miterlimit:4;stroke-dasharray:none;stroke-dashoffset:0;stroke-opacity:1" />
+ <text
+ id="text839-6-3"
+ y="67.426483"
+ x="125.74102"
+ style="font-size:4.9389px;line-height:1.1;font-family:sans-serif;text-align:start;word-spacing:0px;text-anchor:start;stroke-width:0.264583"
+ xml:space="preserve"><tspan
+ style="font-style:normal;font-variant:normal;font-weight:normal;font-stretch:normal;font-size:4.9389px;font-family:monospace;-inkscape-font-specification:monospace;text-align:start;text-anchor:start;stroke-width:0.264583"
+ y="67.426483"
+ x="125.74102"
+ id="tspan837-3-7"
+ sodipodi:role="line">// Pre: x is ⊥</tspan><tspan
+ style="font-style:normal;font-variant:normal;font-weight:normal;font-stretch:normal;font-size:4.9389px;font-family:monospace;-inkscape-font-specification:monospace;text-align:start;text-anchor:start;stroke-width:0.264583"
+ y="72.910019"
+ x="125.74102"
+ sodipodi:role="line"
+ id="tspan878-1">if (n == 42)</tspan><tspan
+ style="font-style:normal;font-variant:normal;font-weight:normal;font-stretch:normal;font-size:4.9389px;font-family:monospace;-inkscape-font-specification:monospace;text-align:start;text-anchor:start;stroke-width:0.264583"
+ y="78.851234"
+ x="125.74102"
+ sodipodi:role="line"
+ id="tspan874-8">// Post: x is ⊥</tspan></text>
+ <rect
+ style="fill:none;stroke:#000000;stroke-width:0.264999;stroke-miterlimit:4;stroke-dasharray:none;stroke-dashoffset:0;stroke-opacity:1"
+ id="rect12-8-3-3"
+ width="58.208344"
+ height="21.16667"
+ x="84.666664"
+ y="92.604164" />
+ <text
+ xml:space="preserve"
+ style="font-size:4.9389px;line-height:1.1;font-family:sans-serif;text-align:start;word-spacing:0px;text-anchor:start;stroke-width:0.264583"
+ x="88.860504"
+ y="99.025513"
+ id="text839-6-3-7"><tspan
+ sodipodi:role="line"
+ id="tspan837-3-7-6"
+ x="88.860504"
+ y="99.025513"
+ style="font-style:normal;font-variant:normal;font-weight:normal;font-stretch:normal;font-size:4.9389px;font-family:monospace;-inkscape-font-specification:monospace;text-align:start;text-anchor:start;stroke-width:0.264583">// Pre: x is ⊥</tspan><tspan
+ id="tspan878-1-1"
+ sodipodi:role="line"
+ x="88.860504"
+ y="104.50905"
+ style="font-style:normal;font-variant:normal;font-weight:normal;font-stretch:normal;font-size:4.9389px;font-family:monospace;-inkscape-font-specification:monospace;text-align:start;text-anchor:start;stroke-width:0.264583">x = 5;</tspan><tspan
+ id="tspan874-8-5"
+ sodipodi:role="line"
+ x="88.860504"
+ y="109.99258"
+ style="font-style:normal;font-variant:normal;font-weight:normal;font-stretch:normal;font-size:4.9389px;font-family:monospace;-inkscape-font-specification:monospace;text-align:start;text-anchor:start;stroke-width:0.264583">// Post: x is {5}</tspan></text>
+ <rect
+ y="92.604164"
+ x="153.45834"
+ height="21.166677"
+ width="58.208328"
+ id="rect12-8-3-3-3"
+ style="fill:none;stroke:#000000;stroke-width:0.264999;stroke-miterlimit:4;stroke-dasharray:none;stroke-dashoffset:0;stroke-opacity:1" />
+ <text
+ id="text839-6-3-7-8"
+ y="99.025513"
+ x="156.17146"
+ style="font-size:4.9389px;line-height:1.1;font-family:sans-serif;text-align:start;word-spacing:0px;text-anchor:start;stroke-width:0.264583"
+ xml:space="preserve"><tspan
+ style="font-style:normal;font-variant:normal;font-weight:normal;font-stretch:normal;font-size:4.9389px;font-family:monospace;-inkscape-font-specification:monospace;text-align:start;text-anchor:start;stroke-width:0.264583"
+ y="99.025513"
+ x="156.17146"
+ id="tspan837-3-7-6-0"
+ sodipodi:role="line">// Pre: x is ⊥</tspan><tspan
+ style="font-style:normal;font-variant:normal;font-weight:normal;font-stretch:normal;font-size:4.9389px;font-family:monospace;-inkscape-font-specification:monospace;text-align:start;text-anchor:start;stroke-width:0.264583"
+ y="104.50905"
+ x="156.17146"
+ sodipodi:role="line"
+ id="tspan878-1-1-7">x = 44;</tspan><tspan
+ style="font-style:normal;font-variant:normal;font-weight:normal;font-stretch:normal;font-size:4.9389px;font-family:monospace;-inkscape-font-specification:monospace;text-align:start;text-anchor:start;stroke-width:0.264583"
+ y="109.99258"
+ x="156.17146"
+ sodipodi:role="line"
+ id="tspan874-8-5-9">// Post: x is {44}</tspan></text>
+ <rect
+ style="fill:none;stroke:#000000;stroke-width:0.264999;stroke-miterlimit:4;stroke-dasharray:none;stroke-dashoffset:0;stroke-opacity:1"
+ id="rect12-8-3-35"
+ width="68.791672"
+ height="21.166672"
+ x="113.77083"
+ y="124.35416" />
+ <text
+ xml:space="preserve"
+ style="font-size:4.9389px;line-height:1.1;font-family:sans-serif;text-align:start;word-spacing:0px;text-anchor:start;stroke-width:0.264583"
+ x="117.2491"
+ y="130.77551"
+ id="text839-6-3-8"><tspan
+ sodipodi:role="line"
+ id="tspan837-3-7-7"
+ x="117.2491"
+ y="130.77551"
+ style="font-style:normal;font-variant:normal;font-weight:normal;font-stretch:normal;font-size:4.9389px;font-family:monospace;-inkscape-font-specification:monospace;text-align:start;text-anchor:start;stroke-width:0.264583">// Pre: x is {5; 44}</tspan><tspan
+ id="tspan878-1-2"
+ sodipodi:role="line"
+ x="117.2491"
+ y="136.25905"
+ style="font-style:normal;font-variant:normal;font-weight:normal;font-stretch:normal;font-size:4.9389px;font-family:monospace;-inkscape-font-specification:monospace;text-align:start;text-anchor:start;stroke-width:0.264583">print(x);</tspan><tspan
+ id="tspan874-8-54"
+ sodipodi:role="line"
+ x="117.2491"
+ y="141.74258"
+ style="font-style:normal;font-variant:normal;font-weight:normal;font-stretch:normal;font-size:4.9389px;font-family:monospace;-inkscape-font-specification:monospace;text-align:start;text-anchor:start;stroke-width:0.264583">// Post: x is {5; 44}</tspan></text>
+ <rect
+ style="fill:none;stroke:#000000;stroke-width:0.264999;stroke-miterlimit:4;stroke-dasharray:none;stroke-dashoffset:0;stroke-opacity:1"
+ id="rect12-8-6-3"
+ width="52.916668"
+ height="21.166666"
+ x="50.270832"
+ y="156.10417" />
+ <text
+ xml:space="preserve"
+ style="font-size:4.9389px;line-height:1.1;font-family:sans-serif;text-align:start;word-spacing:0px;text-anchor:start;stroke-width:0.264583"
+ x="53.695339"
+ y="162.79588"
+ id="text839-6-0-3"><tspan
+ sodipodi:role="line"
+ id="tspan837-3-1-7"
+ x="53.695339"
+ y="162.79588"
+ style="font-style:normal;font-variant:normal;font-weight:normal;font-stretch:normal;font-size:4.9389px;font-family:monospace;-inkscape-font-specification:monospace;text-align:start;text-anchor:start;stroke-width:0.264583">// Pre: x is ⊤</tspan><tspan
+ id="tspan878-2-0"
+ sodipodi:role="line"
+ x="53.695339"
+ y="168.49834"
+ style="font-style:normal;font-variant:normal;font-weight:normal;font-stretch:normal;font-size:4.9389px;font-family:monospace;-inkscape-font-specification:monospace;text-align:start;text-anchor:start;stroke-width:0.264583">print(x);</tspan><tspan
+ id="tspan874-3-8"
+ sodipodi:role="line"
+ x="53.695339"
+ y="173.98187"
+ style="font-style:normal;font-variant:normal;font-weight:normal;font-stretch:normal;font-size:4.9389px;font-family:monospace;-inkscape-font-specification:monospace;text-align:start;text-anchor:start;stroke-width:0.264583">// Post: x is ⊤</tspan></text>
+ <path
+ id="path1086"
+ d="M 76.729166,13.229166 V 23.812499"
+ style="fill:none;stroke:#000000;stroke-width:0.264583px;stroke-linecap:butt;stroke-linejoin:miter;stroke-opacity:1;marker-end:url(#Arrow2Lend)" />
+ <path
+ sodipodi:nodetypes="cc"
+ style="fill:none;stroke:#000000;stroke-width:0.264583px;stroke-linecap:butt;stroke-linejoin:miter;stroke-opacity:1;marker-end:url(#Arrow2Lend-6)"
+ d="M 95.249999,50.270833 129.64583,60.854166"
+ id="path1086-0" />
+ <path
+ sodipodi:nodetypes="cc"
+ style="fill:none;stroke:#000000;stroke-width:0.264583px;stroke-linecap:butt;stroke-linejoin:miter;stroke-opacity:1;marker-end:url(#Arrow2Lend-1)"
+ d="M 58.208333,50.270833 29.104166,92.604166"
+ id="path1086-08" />
+ <path
+ sodipodi:nodetypes="cc"
+ style="fill:none;stroke:#000000;stroke-width:0.264583px;stroke-linecap:butt;stroke-linejoin:miter;stroke-opacity:1;marker-end:url(#Arrow2Lend-8)"
+ d="M 129.64583,82.020833 111.125,92.604166"
+ id="path1086-2" />
+ <path
+ sodipodi:nodetypes="cc"
+ style="fill:none;stroke:#000000;stroke-width:0.264583px;stroke-linecap:butt;stroke-linejoin:miter;stroke-opacity:1;marker-end:url(#Arrow2Lend-81)"
+ d="m 166.6875,82.020833 15.875,10.583333"
+ id="path1086-5" />
+ <path
+ sodipodi:nodetypes="cc"
+ style="fill:none;stroke:#000000;stroke-width:0.264583px;stroke-linecap:butt;stroke-linejoin:miter;stroke-opacity:1;marker-end:url(#Arrow2Lend-7)"
+ d="m 111.125,113.77084 10.58333,10.58333"
+ id="path1086-9" />
+ <path
+ sodipodi:nodetypes="cc"
+ style="fill:none;stroke:#000000;stroke-width:0.264583px;stroke-linecap:butt;stroke-linejoin:miter;stroke-opacity:1;marker-end:url(#Arrow2Lend-2)"
+ d="m 182.5625,113.77084 -7.9375,10.58333"
+ id="path1086-6" />
+ <path
+ sodipodi:nodetypes="cc"
+ style="fill:none;stroke:#000000;stroke-width:0.264583px;stroke-linecap:butt;stroke-linejoin:miter;stroke-opacity:1;marker-end:url(#Arrow2Lend-83)"
+ d="M 148.16667,145.52084 95.249999,156.10417"
+ id="path1086-59" />
+ <path
+ sodipodi:nodetypes="cc"
+ style="fill:none;stroke:#000000;stroke-width:0.264583px;stroke-linecap:butt;stroke-linejoin:miter;stroke-opacity:1;marker-end:url(#Arrow2Lend-0)"
+ d="m 29.104166,113.77084 29.104167,42.33333"
+ id="path1086-8" />
+ <rect
+ style="fill:none;stroke:#000000;stroke-width:0.264999;stroke-miterlimit:4;stroke-dasharray:none;stroke-dashoffset:0;stroke-opacity:1"
+ id="rect12-3"
+ width="42.333332"
+ height="10.583333"
+ x="55.5625"
+ y="187.85417" />
+ <text
+ xml:space="preserve"
+ style="font-size:4.9389px;line-height:1;font-family:sans-serif;text-align:center;word-spacing:0px;text-anchor:middle;stroke-width:0.264583"
+ x="76.561569"
+ y="194.44447"
+ id="text839-3"><tspan
+ sodipodi:role="line"
+ id="tspan837-6"
+ x="76.561569"
+ y="194.44447"
+ style="font-size:4.9389px;text-align:center;text-anchor:middle;stroke-width:0.264583">Exit</tspan></text>
+ <path
+ style="fill:none;stroke:#000000;stroke-width:0.264583px;stroke-linecap:butt;stroke-linejoin:miter;stroke-opacity:1;marker-end:url(#Arrow2Lend-15)"
+ d="m 76.729166,177.27084 v 10.58334"
+ id="path1086-1" />
+ <text
+ xml:space="preserve"
+ style="font-size:4.9389px;line-height:1;font-family:sans-serif;text-align:center;word-spacing:0px;text-anchor:middle;stroke-width:0.264583"
+ x="119.0625"
+ y="55.562504"
+ id="text839-1"><tspan
+ sodipodi:role="line"
+ id="tspan837-4"
+ x="119.0625"
+ y="55.562504"
+ style="font-size:4.9389px;text-align:center;text-anchor:middle;stroke-width:0.264583">True</tspan></text>
+ <text
+ id="text839-1-4"
+ y="87.3125"
+ x="179.91667"
+ style="font-size:4.9389px;line-height:1;font-family:sans-serif;text-align:center;word-spacing:0px;text-anchor:middle;stroke-width:0.264583"
+ xml:space="preserve"><tspan
+ style="font-size:4.9389px;text-align:center;text-anchor:middle;stroke-width:0.264583"
+ y="87.3125"
+ x="179.91667"
+ id="tspan837-4-2"
+ sodipodi:role="line">True</tspan></text>
+ <text
+ id="text839-1-5"
+ y="87.3125"
+ x="113.77083"
+ style="font-size:4.9389px;line-height:1;font-family:sans-serif;text-align:center;word-spacing:0px;text-anchor:middle;stroke-width:0.264583"
+ xml:space="preserve"><tspan
+ style="font-size:4.9389px;text-align:center;text-anchor:middle;stroke-width:0.264583"
+ y="87.3125"
+ x="113.77083"
+ id="tspan837-4-7"
+ sodipodi:role="line">False</tspan></text>
+ <text
+ xml:space="preserve"
+ style="font-size:4.9389px;line-height:1;font-family:sans-serif;text-align:center;word-spacing:0px;text-anchor:middle;stroke-width:0.264583"
+ x="44.979164"
+ y="58.208332"
+ id="text839-1-5-5"><tspan
+ sodipodi:role="line"
+ id="tspan837-4-7-4"
+ x="44.979164"
+ y="58.208332"
+ style="font-size:4.9389px;text-align:center;text-anchor:middle;stroke-width:0.264583">False</tspan></text>
+ </g>
+</svg>
diff --git a/docs/DataFlowAnalysisIntroImages/CFGJoinRule.svg b/docs/DataFlowAnalysisIntroImages/CFGJoinRule.svg
new file mode 100644
index 0000000..95daffa
--- /dev/null
+++ b/docs/DataFlowAnalysisIntroImages/CFGJoinRule.svg
@@ -0,0 +1,222 @@
+<?xml version="1.0" encoding="UTF-8" standalone="no"?>
+<svg
+ xmlns:dc="http://purl.org/dc/elements/1.1/"
+ xmlns:cc="http://creativecommons.org/ns#"
+ xmlns:rdf="http://www.w3.org/1999/02/22-rdf-syntax-ns#"
+ xmlns:svg="http://www.w3.org/2000/svg"
+ xmlns="http://www.w3.org/2000/svg"
+ xmlns:sodipodi="http://sodipodi.sourceforge.net/DTD/sodipodi-0.dtd"
+ xmlns:inkscape="http://www.inkscape.org/namespaces/inkscape"
+ id="svg8"
+ version="1.1"
+ viewBox="0 0 180 70"
+ height="70mm"
+ width="180mm">
+ <defs
+ id="defs2">
+ <marker
+ inkscape:isstock="true"
+ style="overflow:visible"
+ id="marker1412"
+ refX="0"
+ refY="0"
+ orient="auto"
+ inkscape:stockid="Arrow2Lend">
+ <path
+ transform="matrix(-1.1,0,0,-1.1,-1.1,0)"
+ d="M 8.7185878,4.0337352 -2.2072895,0.01601326 8.7185884,-4.0017078 c -1.7454984,2.3720609 -1.7354408,5.6174519 -6e-7,8.035443 z"
+ style="fill:#000000;fill-opacity:1;fill-rule:evenodd;stroke:#000000;stroke-width:0.625;stroke-linejoin:round;stroke-opacity:1"
+ id="path1410" />
+ </marker>
+ <marker
+ inkscape:isstock="true"
+ style="overflow:visible"
+ id="Arrow1Lend"
+ refX="0"
+ refY="0"
+ orient="auto"
+ inkscape:stockid="Arrow1Lend">
+ <path
+ transform="matrix(-0.8,0,0,-0.8,-10,0)"
+ style="fill:#000000;fill-opacity:1;fill-rule:evenodd;stroke:#000000;stroke-width:1pt;stroke-opacity:1"
+ d="M 0,0 5,-5 -12.5,0 5,5 Z"
+ id="path1083" />
+ </marker>
+ </defs>
+ <g
+ id="layer1"
+ inkscape:groupmode="layer"
+ inkscape:label="Layer 1">
+ <text
+ id="text32"
+ y="5.2916665"
+ x="2.6458333"
+ style="font-size:4.93889px;line-height:1.25;font-family:sans-serif;word-spacing:0px;stroke-width:0.264583"
+ xml:space="preserve"><tspan
+ style="font-size:4.93889px;stroke-width:0.264583"
+ y="5.2916665"
+ x="2.6458333"
+ id="tspan30"
+ sodipodi:role="line">(Given)</tspan></text>
+ <text
+ xml:space="preserve"
+ style="font-size:4.9389px;line-height:1.25;font-family:sans-serif;word-spacing:0px;stroke-width:0.264583"
+ x="2.6458333"
+ y="66.145836"
+ id="text32-2"><tspan
+ sodipodi:role="line"
+ id="tspan30-8"
+ x="2.6458333"
+ y="66.145836"
+ style="font-size:4.9389px;stroke-width:0.264583">(Conclusion)</tspan></text>
+ <text
+ xml:space="preserve"
+ style="font-size:4.9389px;line-height:1.25;font-family:sans-serif;word-spacing:0px;stroke-width:0.264583"
+ x="29.104166"
+ y="5.2916665"
+ id="text32-1"><tspan
+ sodipodi:role="line"
+ id="tspan30-9"
+ x="29.104166"
+ y="5.2916665"
+ style="font-size:4.9389px;text-align:center;text-anchor:middle;stroke-width:0.264583"><tspan
+ id="tspan72"
+ style="font-style:italic;font-variant:normal;font-weight:normal;font-stretch:normal;font-size:4.9389px;font-family:sans-serif;-inkscape-font-specification:'sans-serif, Italic';font-variant-ligatures:normal;font-variant-caps:normal;font-variant-numeric:normal;font-variant-east-asian:normal;text-align:center;text-anchor:middle">in</tspan><tspan
+ id="tspan70"
+ style="font-size:65%;text-align:center;baseline-shift:sub;text-anchor:middle">1</tspan></tspan></text>
+ <text
+ id="text32-1-5"
+ y="5.2916665"
+ x="43.65625"
+ style="font-size:4.9389px;line-height:1.25;font-family:sans-serif;word-spacing:0px;stroke-width:0.264583"
+ xml:space="preserve"><tspan
+ style="font-size:4.9389px;text-align:center;text-anchor:middle;stroke-width:0.264583"
+ y="5.2916665"
+ x="43.65625"
+ id="tspan30-9-7"
+ sodipodi:role="line"><tspan
+ style="font-style:italic;font-variant:normal;font-weight:normal;font-stretch:normal;font-size:4.9389px;font-family:sans-serif;-inkscape-font-specification:'sans-serif, Italic';font-variant-ligatures:normal;font-variant-caps:normal;font-variant-numeric:normal;font-variant-east-asian:normal;text-align:center;text-anchor:middle;stroke-width:0.264583"
+ id="tspan72-5">in</tspan><tspan
+ style="font-size:3.2103px;text-align:center;baseline-shift:sub;text-anchor:middle;stroke-width:0.264583"
+ id="tspan70-9">2</tspan></tspan></text>
+ <text
+ xml:space="preserve"
+ style="font-size:4.9389px;line-height:1.25;font-family:sans-serif;word-spacing:0px;stroke-width:0.264583"
+ x="70.114578"
+ y="5.2916665"
+ id="text32-1-5-3"><tspan
+ sodipodi:role="line"
+ id="tspan30-9-7-0"
+ x="70.114578"
+ y="5.2916665"
+ style="font-size:4.9389px;text-align:center;text-anchor:middle;stroke-width:0.264583"><tspan
+ id="tspan72-5-9"
+ style="font-style:italic;font-variant:normal;font-weight:normal;font-stretch:normal;font-size:4.9389px;font-family:sans-serif;-inkscape-font-specification:'sans-serif, Italic';font-variant-ligatures:normal;font-variant-caps:normal;font-variant-numeric:normal;font-variant-east-asian:normal;text-align:center;text-anchor:middle;stroke-width:0.264583">in</tspan><tspan
+ id="tspan70-9-5"
+ style="font-size:3.2103px;text-align:center;baseline-shift:sub;text-anchor:middle;stroke-width:0.264583">n</tspan></tspan></text>
+ <text
+ id="text32-1-56"
+ y="31.75"
+ x="50.270832"
+ style="font-size:4.9389px;line-height:1.25;font-family:sans-serif;word-spacing:0px;stroke-width:0.264583"
+ xml:space="preserve"><tspan
+ style="font-style:normal;font-variant:normal;font-weight:normal;font-stretch:normal;font-size:4.9389px;font-family:sans-serif;-inkscape-font-specification:'sans-serif, Normal';font-variant-ligatures:normal;font-variant-caps:normal;font-variant-numeric:normal;font-variant-east-asian:normal;text-align:center;text-anchor:middle;stroke-width:0.264583"
+ y="31.75"
+ x="50.270832"
+ id="tspan30-9-5"
+ sodipodi:role="line"><tspan
+ id="tspan148"
+ style="font-style:italic;font-variant:normal;font-weight:normal;font-stretch:normal;font-size:4.9389px;font-family:sans-serif;-inkscape-font-specification:'sans-serif, Italic';font-variant-ligatures:normal;font-variant-caps:normal;font-variant-numeric:normal;font-variant-east-asian:normal">join</tspan>(<tspan
+ id="tspan156"
+ style="font-style:italic;font-variant:normal;font-weight:normal;font-stretch:normal;font-size:4.9389px;font-family:sans-serif;-inkscape-font-specification:'sans-serif, Italic';font-variant-ligatures:normal;font-variant-caps:normal;font-variant-numeric:normal;font-variant-east-asian:normal">in</tspan><tspan
+ id="tspan150"
+ style="font-size:65%;baseline-shift:sub">1</tspan>, <tspan
+ id="tspan158"
+ style="font-style:italic;font-variant:normal;font-weight:normal;font-stretch:normal;font-size:4.9389px;font-family:sans-serif;-inkscape-font-specification:'sans-serif, Italic';font-variant-ligatures:normal;font-variant-caps:normal;font-variant-numeric:normal;font-variant-east-asian:normal">in</tspan><tspan
+ id="tspan152"
+ style="font-size:65%;baseline-shift:sub">2</tspan>, …, <tspan
+ id="tspan160"
+ style="font-style:italic;font-variant:normal;font-weight:normal;font-stretch:normal;font-size:4.9389px;font-family:sans-serif;-inkscape-font-specification:'sans-serif, Italic';font-variant-ligatures:normal;font-variant-caps:normal;font-variant-numeric:normal;font-variant-east-asian:normal">in</tspan><tspan
+ id="tspan154"
+ style="font-size:65%;baseline-shift:sub">n</tspan>)</tspan></text>
+ <text
+ xml:space="preserve"
+ style="font-size:4.9389px;line-height:1.25;font-family:sans-serif;text-align:start;word-spacing:0px;text-anchor:start;stroke-width:0.264583"
+ x="52.916668"
+ y="66.145836"
+ id="text32-1-56-8"><tspan
+ sodipodi:role="line"
+ id="tspan30-9-5-4"
+ x="52.916668"
+ y="66.145836"
+ style="font-style:normal;font-variant:normal;font-weight:normal;font-stretch:normal;font-size:4.9389px;font-family:sans-serif;-inkscape-font-specification:'sans-serif, Normal';font-variant-ligatures:normal;font-variant-caps:normal;font-variant-numeric:normal;font-variant-east-asian:normal;text-align:start;text-anchor:start;stroke-width:0.264583"><tspan
+ style="font-style:italic;font-variant:normal;font-weight:normal;font-stretch:normal;font-size:4.9389px;font-family:sans-serif;-inkscape-font-specification:'sans-serif, Italic';font-variant-ligatures:normal;font-variant-caps:normal;font-variant-numeric:normal;font-variant-east-asian:normal;text-align:start;text-anchor:start;stroke-width:0.264583"
+ id="tspan148-3">out<tspan
+ id="tspan203"
+ style="font-style:normal;font-variant:normal;font-weight:normal;font-stretch:normal;font-size:4.9389px;font-family:sans-serif;-inkscape-font-specification:'sans-serif, Normal';font-variant-ligatures:normal;font-variant-caps:normal;font-variant-numeric:normal;font-variant-east-asian:normal;text-align:start;text-anchor:start"> = </tspan>transfer<tspan
+ id="tspan201"
+ style="font-style:normal;font-variant:normal;font-weight:normal;font-stretch:normal;font-size:4.9389px;font-family:sans-serif;-inkscape-font-specification:'sans-serif, Normal';font-variant-ligatures:normal;font-variant-caps:normal;font-variant-numeric:normal;font-variant-east-asian:normal;text-align:start;text-anchor:start">(<tspan
+ id="tspan205"
+ style="font-style:italic;font-variant:normal;font-weight:normal;font-stretch:normal;font-size:4.9389px;font-family:sans-serif;-inkscape-font-specification:'sans-serif, Italic';font-variant-ligatures:normal;font-variant-caps:normal;font-variant-numeric:normal;font-variant-east-asian:normal;text-align:start;text-anchor:start">basic_block</tspan>, </tspan>join</tspan>(<tspan
+ style="font-style:italic;font-variant:normal;font-weight:normal;font-stretch:normal;font-size:4.9389px;font-family:sans-serif;-inkscape-font-specification:'sans-serif, Italic';font-variant-ligatures:normal;font-variant-caps:normal;font-variant-numeric:normal;font-variant-east-asian:normal;text-align:start;text-anchor:start;stroke-width:0.264583"
+ id="tspan156-6">in</tspan><tspan
+ style="font-size:3.2103px;text-align:start;baseline-shift:sub;text-anchor:start;stroke-width:0.264583"
+ id="tspan150-4">1</tspan>, <tspan
+ style="font-style:italic;font-variant:normal;font-weight:normal;font-stretch:normal;font-size:4.9389px;font-family:sans-serif;-inkscape-font-specification:'sans-serif, Italic';font-variant-ligatures:normal;font-variant-caps:normal;font-variant-numeric:normal;font-variant-east-asian:normal;text-align:start;text-anchor:start;stroke-width:0.264583"
+ id="tspan158-3">in</tspan><tspan
+ style="font-size:3.2103px;text-align:start;baseline-shift:sub;text-anchor:start;stroke-width:0.264583"
+ id="tspan152-8">2</tspan>, …, <tspan
+ style="font-style:italic;font-variant:normal;font-weight:normal;font-stretch:normal;font-size:4.9389px;font-family:sans-serif;-inkscape-font-specification:'sans-serif, Italic';font-variant-ligatures:normal;font-variant-caps:normal;font-variant-numeric:normal;font-variant-east-asian:normal;text-align:start;text-anchor:start;stroke-width:0.264583"
+ id="tspan160-3">in</tspan><tspan
+ style="font-size:3.2103px;text-align:start;baseline-shift:sub;text-anchor:start;stroke-width:0.264583"
+ id="tspan154-1">n</tspan>))</tspan></text>
+ <rect
+ y="23.8125"
+ x="15.874998"
+ height="31.75"
+ width="68.791664"
+ id="rect207"
+ style="fill:none;stroke:#000000;stroke-width:0.264999" />
+ <text
+ id="text32-2-8"
+ y="44.979168"
+ x="50.270836"
+ style="font-size:4.9389px;line-height:1.25;font-family:sans-serif;word-spacing:0px;stroke-width:0.264583"
+ xml:space="preserve"><tspan
+ style="font-size:4.9389px;text-align:center;text-anchor:middle;stroke-width:0.264583"
+ y="44.979168"
+ x="50.270836"
+ id="tspan30-8-8"
+ sodipodi:role="line">Basic block</tspan></text>
+ <path
+ sodipodi:nodetypes="cc"
+ id="path227"
+ d="M 27.781249,6.6145827 50.270832,23.8125"
+ style="fill:none;stroke:#000000;stroke-width:0.264583px;stroke-linecap:butt;stroke-linejoin:miter;stroke-opacity:1" />
+ <path
+ sodipodi:nodetypes="cc"
+ id="path229"
+ d="M 42.333333,6.6145827 50.270832,23.8125"
+ style="fill:none;stroke:#000000;stroke-width:0.264583px;stroke-linecap:butt;stroke-linejoin:miter;stroke-opacity:1" />
+ <text
+ xml:space="preserve"
+ style="font-size:4.9389px;line-height:1.25;font-family:sans-serif;word-spacing:0px;stroke-width:0.264583"
+ x="56.885418"
+ y="5.2916665"
+ id="text32-1-5-35"><tspan
+ sodipodi:role="line"
+ id="tspan30-9-7-00"
+ x="56.885418"
+ y="5.2916665"
+ style="font-size:4.9389px;text-align:center;text-anchor:middle;stroke-width:0.264583">…</tspan></text>
+ <path
+ sodipodi:nodetypes="cc"
+ id="path255"
+ d="M 68.791666,6.6145827 50.270832,23.8125"
+ style="fill:none;stroke:#000000;stroke-width:0.265;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:4;stroke-dasharray:none;stroke-opacity:1" />
+ <path
+ id="path1492"
+ d="M 50.270832,55.562499 V 70.114582"
+ style="fill:none;stroke:#000000;stroke-width:0.264583px;stroke-linecap:butt;stroke-linejoin:miter;stroke-opacity:1;marker-end:url(#marker1412)" />
+ </g>
+</svg>
diff --git a/docs/DataFlowAnalysisIntroImages/DefinitiveInitializationLattice.svg b/docs/DataFlowAnalysisIntroImages/DefinitiveInitializationLattice.svg
new file mode 100644
index 0000000..861a3f9
--- /dev/null
+++ b/docs/DataFlowAnalysisIntroImages/DefinitiveInitializationLattice.svg
@@ -0,0 +1,114 @@
+<?xml version="1.0" encoding="UTF-8" standalone="no"?>
+<svg
+ xmlns:dc="http://purl.org/dc/elements/1.1/"
+ xmlns:cc="http://creativecommons.org/ns#"
+ xmlns:rdf="http://www.w3.org/1999/02/22-rdf-syntax-ns#"
+ xmlns:svg="http://www.w3.org/2000/svg"
+ xmlns="http://www.w3.org/2000/svg"
+ xmlns:sodipodi="http://sodipodi.sourceforge.net/DTD/sodipodi-0.dtd"
+ xmlns:inkscape="http://www.inkscape.org/namespaces/inkscape"
+ id="svg8"
+ version="1.1"
+ viewBox="0 0 120 40"
+ height="40mm"
+ width="120mm">
+ <defs
+ id="defs2">
+ <marker
+ inkscape:stockid="Arrow2Lend"
+ orient="auto"
+ refY="0.0"
+ refX="0.0"
+ id="marker1184"
+ style="overflow:visible;"
+ inkscape:isstock="true">
+ <path
+ id="path1182"
+ style="fill-rule:evenodd;stroke-width:0.625;stroke-linejoin:round;stroke:#000000;stroke-opacity:1;fill:#000000;fill-opacity:1"
+ d="M 8.7185878,4.0337352 L -2.2072895,0.016013256 L 8.7185884,-4.0017078 C 6.9730900,-1.6296469 6.9831476,1.6157441 8.7185878,4.0337352 z "
+ transform="scale(1.1) rotate(180) translate(1,0)" />
+ </marker>
+ <marker
+ inkscape:stockid="Arrow2Lend"
+ orient="auto"
+ refY="0.0"
+ refX="0.0"
+ id="marker1174"
+ style="overflow:visible;"
+ inkscape:isstock="true">
+ <path
+ id="path1172"
+ style="fill-rule:evenodd;stroke-width:0.625;stroke-linejoin:round;stroke:#000000;stroke-opacity:1;fill:#000000;fill-opacity:1"
+ d="M 8.7185878,4.0337352 L -2.2072895,0.016013256 L 8.7185884,-4.0017078 C 6.9730900,-1.6296469 6.9831476,1.6157441 8.7185878,4.0337352 z "
+ transform="scale(1.1) rotate(180) translate(1,0)" />
+ </marker>
+ </defs>
+ <g
+ id="layer1"
+ inkscape:groupmode="layer"
+ inkscape:label="Layer 1">
+ <text
+ id="text837"
+ y="10.639833"
+ x="60.836075"
+ style="font-size:4.93889px;line-height:1.25;font-family:sans-serif;text-align:center;word-spacing:0px;text-anchor:middle;stroke-width:0.264583"
+ xml:space="preserve"><tspan
+ style="font-size:4.93889px;text-align:center;text-anchor:middle;stroke-width:0.264583"
+ y="10.639833"
+ x="60.836075"
+ id="tspan835"
+ sodipodi:role="line">Maybe uninitialized</tspan></text>
+ <text
+ xml:space="preserve"
+ style="font-size:4.9389px;line-height:1.25;font-family:sans-serif;text-align:center;word-spacing:0px;text-anchor:middle;stroke-width:0.264583"
+ x="29.162045"
+ y="34.911739"
+ id="text837-3"><tspan
+ sodipodi:role="line"
+ id="tspan835-8"
+ x="29.162045"
+ y="34.911739"
+ style="font-size:4.9389px;text-align:center;text-anchor:middle;stroke-width:0.264583">Initialized</tspan></text>
+ <text
+ id="text837-3-3"
+ y="34.911739"
+ x="92.612602"
+ style="font-size:4.9389px;line-height:1.25;font-family:sans-serif;text-align:center;word-spacing:0px;text-anchor:middle;stroke-width:0.264583"
+ xml:space="preserve"><tspan
+ style="font-size:4.9389px;text-align:center;text-anchor:middle;stroke-width:0.264583"
+ y="34.911739"
+ x="92.612602"
+ id="tspan835-8-3"
+ sodipodi:role="line">Uninitialized</tspan></text>
+ <rect
+ y="2.6458333"
+ x="34.395832"
+ height="13.229168"
+ width="52.91666"
+ id="rect875"
+ style="fill:none;stroke:#000000;stroke-width:0.264999" />
+ <rect
+ style="fill:none;stroke:#000000;stroke-width:0.264999"
+ id="rect875-9"
+ width="52.916664"
+ height="13.229168"
+ x="66.145828"
+ y="26.458334" />
+ <rect
+ style="fill:none;stroke:#000000;stroke-width:0.264999"
+ id="rect875-0"
+ width="52.916664"
+ height="13.229168"
+ x="2.6458352"
+ y="26.458334" />
+ <path
+ id="path898"
+ d="M 29.104166,26.458333 60.854166,15.875"
+ style="fill:none;stroke:#000000;stroke-width:0.265;stroke-linecap:butt;stroke-linejoin:miter;stroke-opacity:1;stroke-miterlimit:4;stroke-dasharray:none;marker-end:url(#marker1184)" />
+ <path
+ sodipodi:nodetypes="cc"
+ id="path900"
+ d="M 92.604167,26.458333 60.854166,15.875"
+ style="fill:none;stroke:#000000;stroke-width:0.265;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:4;stroke-dasharray:none;stroke-opacity:1;marker-end:url(#marker1174)" />
+ </g>
+</svg>
diff --git a/docs/DataFlowAnalysisIntroImages/IntegerSetsFiniteLattice.svg b/docs/DataFlowAnalysisIntroImages/IntegerSetsFiniteLattice.svg
new file mode 100644
index 0000000..aab7d3e
--- /dev/null
+++ b/docs/DataFlowAnalysisIntroImages/IntegerSetsFiniteLattice.svg
@@ -0,0 +1,403 @@
+<?xml version="1.0" encoding="UTF-8" standalone="no"?>
+<svg
+ xmlns:dc="http://purl.org/dc/elements/1.1/"
+ xmlns:cc="http://creativecommons.org/ns#"
+ xmlns:rdf="http://www.w3.org/1999/02/22-rdf-syntax-ns#"
+ xmlns:svg="http://www.w3.org/2000/svg"
+ xmlns="http://www.w3.org/2000/svg"
+ xmlns:sodipodi="http://sodipodi.sourceforge.net/DTD/sodipodi-0.dtd"
+ xmlns:inkscape="http://www.inkscape.org/namespaces/inkscape"
+ id="svg8"
+ version="1.1"
+ viewBox="0 0 170 110"
+ height="110mm"
+ width="170mm">
+ <defs
+ id="defs2" />
+ <g
+ id="layer1"
+ inkscape:groupmode="layer"
+ inkscape:label="Layer 1">
+ <text
+ id="text1921"
+ y="105.83334"
+ x="89.958336"
+ style="font-size:4.93889px;line-height:1.25;font-family:sans-serif;word-spacing:0px;stroke-width:0.264583"
+ xml:space="preserve"><tspan
+ style="font-size:4.93889px;text-align:center;text-anchor:middle;stroke-width:0.264583"
+ y="105.83334"
+ x="89.958336"
+ id="tspan1919"
+ sodipodi:role="line">⊥ = {}</tspan></text>
+ <text
+ id="text1925"
+ y="76.729172"
+ x="4.0951862"
+ style="font-size:4.93889px;line-height:1.25;font-family:sans-serif;text-align:center;word-spacing:0px;text-anchor:middle;stroke-width:0.264583"
+ xml:space="preserve"><tspan
+ style="font-size:4.93889px;text-align:center;text-anchor:middle;stroke-width:0.264583"
+ y="76.729172"
+ x="4.0951862"
+ id="tspan1923"
+ sodipodi:role="line">…</tspan></text>
+ <text
+ xml:space="preserve"
+ style="font-size:4.9389px;line-height:1.25;font-family:sans-serif;text-align:center;word-spacing:0px;text-anchor:middle;stroke-width:0.264583"
+ x="27.907686"
+ y="76.729172"
+ id="text1925-6"><tspan
+ sodipodi:role="line"
+ id="tspan1923-9"
+ x="27.907686"
+ y="76.729172"
+ style="font-size:4.9389px;text-align:center;text-anchor:middle;stroke-width:0.264583">…</tspan></text>
+ <text
+ xml:space="preserve"
+ style="font-size:4.9389px;line-height:1.25;font-family:sans-serif;text-align:center;word-spacing:0px;text-anchor:middle;stroke-width:0.264583"
+ x="16.001438"
+ y="76.729172"
+ id="text1925-7"><tspan
+ sodipodi:role="line"
+ id="tspan1923-8"
+ x="16.001438"
+ y="76.729172"
+ style="font-size:4.9389px;text-align:center;text-anchor:middle;stroke-width:0.264583">{−9}</tspan></text>
+ <text
+ id="text1925-7-7"
+ y="76.729172"
+ x="39.813934"
+ style="font-size:4.9389px;line-height:1.25;font-family:sans-serif;text-align:center;word-spacing:0px;text-anchor:middle;stroke-width:0.264583"
+ xml:space="preserve"><tspan
+ style="font-size:4.9389px;text-align:center;text-anchor:middle;stroke-width:0.264583"
+ y="76.729172"
+ x="39.813934"
+ id="tspan1923-8-1"
+ sodipodi:role="line">{−5}</tspan></text>
+ <text
+ id="text1925-6-4"
+ y="76.729172"
+ x="51.720184"
+ style="font-size:4.9389px;line-height:1.25;font-family:sans-serif;text-align:center;word-spacing:0px;text-anchor:middle;stroke-width:0.264583"
+ xml:space="preserve"><tspan
+ style="font-size:4.9389px;text-align:center;text-anchor:middle;stroke-width:0.264583"
+ y="76.729172"
+ x="51.720184"
+ id="tspan1923-9-4"
+ sodipodi:role="line">…</tspan></text>
+ <text
+ xml:space="preserve"
+ style="font-size:4.9389px;line-height:1.25;font-family:sans-serif;text-align:center;word-spacing:0px;text-anchor:middle;stroke-width:0.264583"
+ x="63.626438"
+ y="76.729172"
+ id="text1925-7-7-6"><tspan
+ sodipodi:role="line"
+ id="tspan1923-8-1-9"
+ x="63.626438"
+ y="76.729172"
+ style="font-size:4.9389px;text-align:center;text-anchor:middle;stroke-width:0.264583">{−3}</tspan></text>
+ <text
+ xml:space="preserve"
+ style="font-size:4.9389px;line-height:1.25;font-family:sans-serif;text-align:center;word-spacing:0px;text-anchor:middle;stroke-width:0.264583"
+ x="79.501442"
+ y="76.729172"
+ id="text1925-7-7-67"><tspan
+ sodipodi:role="line"
+ id="tspan1923-8-1-8"
+ x="79.501442"
+ y="76.729172"
+ style="font-size:4.9389px;text-align:center;text-anchor:middle;stroke-width:0.264583">{−2}</tspan></text>
+ <text
+ xml:space="preserve"
+ style="font-size:4.9389px;line-height:1.25;font-family:sans-serif;text-align:center;word-spacing:0px;text-anchor:middle;stroke-width:0.264583"
+ x="95.37645"
+ y="76.729172"
+ id="text1925-7-7-9"><tspan
+ sodipodi:role="line"
+ id="tspan1923-8-1-1"
+ x="95.37645"
+ y="76.729172"
+ style="font-size:4.9389px;text-align:center;text-anchor:middle;stroke-width:0.264583">{−1}</tspan></text>
+ <text
+ xml:space="preserve"
+ style="font-size:4.9389px;line-height:1.25;font-family:sans-serif;text-align:center;word-spacing:0px;text-anchor:middle;stroke-width:0.264583"
+ x="109.92851"
+ y="76.729172"
+ id="text1925-7-7-7"><tspan
+ sodipodi:role="line"
+ id="tspan1923-8-1-0"
+ x="109.92851"
+ y="76.729172"
+ style="font-size:4.9389px;text-align:center;text-anchor:middle;stroke-width:0.264583">{0}</tspan></text>
+ <text
+ xml:space="preserve"
+ style="font-size:4.9389px;line-height:1.25;font-family:sans-serif;text-align:center;word-spacing:0px;text-anchor:middle;stroke-width:0.264583"
+ x="123.15768"
+ y="76.729172"
+ id="text1925-7-7-3"><tspan
+ sodipodi:role="line"
+ id="tspan1923-8-1-6"
+ x="123.15768"
+ y="76.729172"
+ style="font-size:4.9389px;text-align:center;text-anchor:middle;stroke-width:0.264583">{1}</tspan></text>
+ <text
+ id="text1925-7-7-3-3"
+ y="76.729172"
+ x="136.38686"
+ style="font-size:4.9389px;line-height:1.25;font-family:sans-serif;text-align:center;word-spacing:0px;text-anchor:middle;stroke-width:0.264583"
+ xml:space="preserve"><tspan
+ style="font-size:4.9389px;text-align:center;text-anchor:middle;stroke-width:0.264583"
+ y="76.729172"
+ x="136.38686"
+ id="tspan1923-8-1-6-8"
+ sodipodi:role="line">{2}</tspan></text>
+ <text
+ id="text1925-7-7-3-31"
+ y="76.729172"
+ x="149.61603"
+ style="font-size:4.9389px;line-height:1.25;font-family:sans-serif;text-align:center;word-spacing:0px;text-anchor:middle;stroke-width:0.264583"
+ xml:space="preserve"><tspan
+ style="font-size:4.9389px;text-align:center;text-anchor:middle;stroke-width:0.264583"
+ y="76.729172"
+ x="149.61603"
+ id="tspan1923-8-1-6-5"
+ sodipodi:role="line">{3}</tspan></text>
+ <text
+ xml:space="preserve"
+ style="font-size:4.9389px;line-height:1.25;font-family:sans-serif;text-align:center;word-spacing:0px;text-anchor:middle;stroke-width:0.264583"
+ x="160.19936"
+ y="76.729172"
+ id="text1925-6-4-0"><tspan
+ sodipodi:role="line"
+ id="tspan1923-9-4-8"
+ x="160.19936"
+ y="76.729172"
+ style="font-size:4.9389px;text-align:center;text-anchor:middle;stroke-width:0.264583">…</tspan></text>
+ <path
+ sodipodi:nodetypes="cc"
+ id="path2089"
+ d="M 16.001436,78.052083 90.084773,100.54166"
+ style="fill:none;stroke:#000000;stroke-width:0.264583px;stroke-linecap:butt;stroke-linejoin:miter;stroke-opacity:1" />
+ <path
+ sodipodi:nodetypes="cc"
+ id="path2091"
+ d="M 39.813936,78.052083 90.084773,100.54166"
+ style="fill:none;stroke:#000000;stroke-width:0.264583px;stroke-linecap:butt;stroke-linejoin:miter;stroke-opacity:1" />
+ <path
+ sodipodi:nodetypes="cc"
+ id="path2093"
+ d="M 63.626436,78.052083 90.084773,100.54166"
+ style="fill:none;stroke:#000000;stroke-width:0.264583px;stroke-linecap:butt;stroke-linejoin:miter;stroke-opacity:1" />
+ <path
+ sodipodi:nodetypes="cc"
+ id="path2095"
+ d="M 79.501436,78.052083 90.084773,100.54166"
+ style="fill:none;stroke:#000000;stroke-width:0.264583px;stroke-linecap:butt;stroke-linejoin:miter;stroke-opacity:1" />
+ <path
+ sodipodi:nodetypes="cc"
+ id="path2097"
+ d="m 95.376433,78.052083 -5.29166,22.489577"
+ style="fill:none;stroke:#000000;stroke-width:0.264583px;stroke-linecap:butt;stroke-linejoin:miter;stroke-opacity:1" />
+ <path
+ sodipodi:nodetypes="cc"
+ id="path2099"
+ d="M 109.92852,78.052083 90.084773,100.54166"
+ style="fill:none;stroke:#000000;stroke-width:0.264583px;stroke-linecap:butt;stroke-linejoin:miter;stroke-opacity:1" />
+ <path
+ sodipodi:nodetypes="cc"
+ id="path2101"
+ d="M 123.15768,78.052083 90.084773,100.54166"
+ style="fill:none;stroke:#000000;stroke-width:0.264583px;stroke-linecap:butt;stroke-linejoin:miter;stroke-opacity:1" />
+ <path
+ id="path2121"
+ d="M 136.38685,78.052082 90.084773,100.54166"
+ style="fill:none;stroke:#000000;stroke-width:0.264583px;stroke-linecap:butt;stroke-linejoin:miter;stroke-opacity:1" />
+ <path
+ id="path2123"
+ d="M 149.61601,78.052082 90.084773,100.54166"
+ style="fill:none;stroke:#000000;stroke-width:0.264583px;stroke-linecap:butt;stroke-linejoin:miter;stroke-opacity:1" />
+ <text
+ xml:space="preserve"
+ style="font-size:4.9389px;line-height:1.25;font-family:sans-serif;text-align:center;word-spacing:0px;text-anchor:middle;stroke-width:0.264583"
+ x="9.3868532"
+ y="50.270832"
+ id="text1925-62"><tspan
+ sodipodi:role="line"
+ id="tspan1923-98"
+ x="9.3868532"
+ y="50.270832"
+ style="font-size:4.9389px;text-align:center;text-anchor:middle;stroke-width:0.264583">…</tspan></text>
+ <text
+ id="text1925-6-6"
+ y="50.270832"
+ x="53.043102"
+ style="font-size:4.9389px;line-height:1.25;font-family:sans-serif;text-align:center;word-spacing:0px;text-anchor:middle;stroke-width:0.264583"
+ xml:space="preserve"><tspan
+ style="font-size:4.9389px;text-align:center;text-anchor:middle;stroke-width:0.264583"
+ y="50.270832"
+ x="53.043102"
+ id="tspan1923-9-0"
+ sodipodi:role="line">…</tspan></text>
+ <text
+ id="text1925-7-6"
+ y="50.270832"
+ x="29.230604"
+ style="font-size:4.9389px;line-height:1.25;font-family:sans-serif;text-align:center;word-spacing:0px;text-anchor:middle;stroke-width:0.264583"
+ xml:space="preserve"><tspan
+ style="font-size:4.9389px;text-align:center;text-anchor:middle;stroke-width:0.264583"
+ y="50.270832"
+ x="29.230604"
+ id="tspan1923-8-18"
+ sodipodi:role="line">{−9, −5}</tspan></text>
+ <text
+ xml:space="preserve"
+ style="font-size:4.9389px;line-height:1.25;font-family:sans-serif;text-align:center;word-spacing:0px;text-anchor:middle;stroke-width:0.264583"
+ x="79.501442"
+ y="50.270832"
+ id="text1925-7-7-31"><tspan
+ sodipodi:role="line"
+ id="tspan1923-8-1-87"
+ x="79.501442"
+ y="50.270832"
+ style="font-size:4.9389px;text-align:center;text-anchor:middle;stroke-width:0.264583">{−3, −1}</tspan></text>
+ <text
+ xml:space="preserve"
+ style="font-size:4.9389px;line-height:1.25;font-family:sans-serif;text-align:center;word-spacing:0px;text-anchor:middle;stroke-width:0.264583"
+ x="108.60561"
+ y="50.270832"
+ id="text1925-6-4-5"><tspan
+ sodipodi:role="line"
+ id="tspan1923-9-4-85"
+ x="108.60561"
+ y="50.270832"
+ style="font-size:4.9389px;text-align:center;text-anchor:middle;stroke-width:0.264583">…</tspan></text>
+ <text
+ id="text1925-7-7-6-0"
+ y="50.270832"
+ x="129.77228"
+ style="font-size:4.9389px;line-height:1.25;font-family:sans-serif;text-align:center;word-spacing:0px;text-anchor:middle;stroke-width:0.264583"
+ xml:space="preserve"><tspan
+ style="font-size:4.9389px;text-align:center;text-anchor:middle;stroke-width:0.264583"
+ y="50.270832"
+ x="129.77228"
+ id="tspan1923-8-1-9-0"
+ sodipodi:role="line">{1, 2}</tspan></text>
+ <text
+ id="text1925-6-4-5-3"
+ y="50.270832"
+ x="149.61603"
+ style="font-size:4.9389px;line-height:1.25;font-family:sans-serif;text-align:center;word-spacing:0px;text-anchor:middle;stroke-width:0.264583"
+ xml:space="preserve"><tspan
+ style="font-size:4.9389px;text-align:center;text-anchor:middle;stroke-width:0.264583"
+ y="50.270832"
+ x="149.61603"
+ id="tspan1923-9-4-85-4"
+ sodipodi:role="line">…</tspan></text>
+ <path
+ id="path2191"
+ d="M 16.001436,71.437499 29.230603,51.59375"
+ style="fill:none;stroke:#000000;stroke-width:0.264583px;stroke-linecap:butt;stroke-linejoin:miter;stroke-opacity:1"
+ sodipodi:nodetypes="cc" />
+ <path
+ id="path2193"
+ d="M 39.813936,71.437499 29.230603,51.59375"
+ style="fill:none;stroke:#000000;stroke-width:0.264583px;stroke-linecap:butt;stroke-linejoin:miter;stroke-opacity:1"
+ sodipodi:nodetypes="cc" />
+ <path
+ id="path2195"
+ d="M 63.626435,71.437499 79.501436,51.59375"
+ style="fill:none;stroke:#000000;stroke-width:0.264583px;stroke-linecap:butt;stroke-linejoin:miter;stroke-opacity:1"
+ sodipodi:nodetypes="cc" />
+ <path
+ id="path2197"
+ d="M 95.376433,71.437499 79.501436,51.59375"
+ style="fill:none;stroke:#000000;stroke-width:0.264583px;stroke-linecap:butt;stroke-linejoin:miter;stroke-opacity:1"
+ sodipodi:nodetypes="cc" />
+ <path
+ id="path2199"
+ d="M 124.4806,71.437499 129.77227,51.59375"
+ style="fill:none;stroke:#000000;stroke-width:0.264583px;stroke-linecap:butt;stroke-linejoin:miter;stroke-opacity:1"
+ sodipodi:nodetypes="cc" />
+ <path
+ id="path2201"
+ d="M 135.06393,71.437499 129.77227,51.59375"
+ style="fill:none;stroke:#000000;stroke-width:0.264583px;stroke-linecap:butt;stroke-linejoin:miter;stroke-opacity:1"
+ sodipodi:nodetypes="cc" />
+ <path
+ sodipodi:nodetypes="cc"
+ style="fill:none;stroke:#000000;stroke-width:0.264583px;stroke-linecap:butt;stroke-linejoin:miter;stroke-opacity:1"
+ d="M 129.77226,44.979165 128.44935,25.135416"
+ id="path2201-1" />
+ <text
+ xml:space="preserve"
+ style="font-size:4.9389px;line-height:1.25;font-family:sans-serif;text-align:center;word-spacing:0px;text-anchor:middle;stroke-width:0.264583"
+ x="128.44936"
+ y="23.812502"
+ id="text1925-7-7-6-0-2"><tspan
+ sodipodi:role="line"
+ id="tspan1923-8-1-9-0-9"
+ x="128.44936"
+ y="23.812502"
+ style="font-size:4.9389px;text-align:center;text-anchor:middle;stroke-width:0.264583">{1, 2, 3}</tspan></text>
+ <path
+ style="fill:none;stroke:#000000;stroke-width:0.264583px;stroke-linecap:butt;stroke-linejoin:miter;stroke-opacity:1"
+ d="M 149.61601,71.437499 128.44935,25.135416"
+ id="path205" />
+ <text
+ id="text1925-6-4-5-0"
+ y="23.812502"
+ x="112.57436"
+ style="font-size:4.9389px;line-height:1.25;font-family:sans-serif;text-align:center;word-spacing:0px;text-anchor:middle;stroke-width:0.264583"
+ xml:space="preserve"><tspan
+ style="font-size:4.9389px;text-align:center;text-anchor:middle;stroke-width:0.264583"
+ y="23.812502"
+ x="112.57436"
+ id="tspan1923-9-4-85-5"
+ sodipodi:role="line">…</tspan></text>
+ <text
+ id="text1925-6-4-5-7"
+ y="23.812502"
+ x="143.00143"
+ style="font-size:4.9389px;line-height:1.25;font-family:sans-serif;text-align:center;word-spacing:0px;text-anchor:middle;stroke-width:0.264583"
+ xml:space="preserve"><tspan
+ style="font-size:4.9389px;text-align:center;text-anchor:middle;stroke-width:0.264583"
+ y="23.812502"
+ x="143.00143"
+ id="tspan1923-9-4-85-0"
+ sodipodi:role="line">…</tspan></text>
+ <text
+ id="text1925-7-7-6-0-2-0"
+ y="6.6145835"
+ x="90.084763"
+ style="font-size:4.9389px;line-height:1.25;font-family:sans-serif;text-align:center;word-spacing:0px;text-anchor:middle;stroke-width:0.264583"
+ xml:space="preserve"><tspan
+ style="font-size:4.9389px;text-align:center;text-anchor:middle;stroke-width:0.264583"
+ y="6.6145835"
+ x="90.084763"
+ id="tspan1923-8-1-9-0-9-0"
+ sodipodi:role="line">⊤ = ℤ</tspan></text>
+ <path
+ style="fill:none;stroke:#000000;stroke-width:0.265;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:4;stroke-dasharray:none;stroke-dashoffset:0;stroke-opacity:1"
+ d="M 90.084773,7.9374993 128.44935,18.520833"
+ id="path253" />
+ <path
+ id="path253-2"
+ d="M 90.084773,7.9375003 108.6056,44.979166"
+ style="fill:none;stroke:#000000;stroke-width:0.265;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:4;stroke-dasharray:none;stroke-dashoffset:0;stroke-opacity:1"
+ sodipodi:nodetypes="cc" />
+ <path
+ id="path253-8"
+ d="M 90.084773,7.9375003 79.501436,44.979166"
+ style="fill:none;stroke:#000000;stroke-width:0.265;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:4;stroke-dasharray:none;stroke-dashoffset:0;stroke-opacity:1"
+ sodipodi:nodetypes="cc" />
+ <path
+ id="path253-6"
+ d="M 90.084773,7.9375003 53.043103,44.979166"
+ style="fill:none;stroke:#000000;stroke-width:0.265;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:4;stroke-dasharray:none;stroke-dashoffset:0;stroke-opacity:1"
+ sodipodi:nodetypes="cc" />
+ <path
+ id="path253-4"
+ d="M 90.084773,7.9375003 29.230603,44.979166"
+ style="fill:none;stroke:#000000;stroke-width:0.26499901;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:4;stroke-dasharray:none;stroke-dashoffset:0;stroke-opacity:1"
+ sodipodi:nodetypes="cc" />
+ </g>
+</svg>
diff --git a/docs/DataFlowAnalysisIntroImages/IntegerSetsInfiniteLattice.svg b/docs/DataFlowAnalysisIntroImages/IntegerSetsInfiniteLattice.svg
new file mode 100644
index 0000000..380aa2a
--- /dev/null
+++ b/docs/DataFlowAnalysisIntroImages/IntegerSetsInfiniteLattice.svg
@@ -0,0 +1,403 @@
+<?xml version="1.0" encoding="UTF-8" standalone="no"?>
+<svg
+ xmlns:dc="http://purl.org/dc/elements/1.1/"
+ xmlns:cc="http://creativecommons.org/ns#"
+ xmlns:rdf="http://www.w3.org/1999/02/22-rdf-syntax-ns#"
+ xmlns:svg="http://www.w3.org/2000/svg"
+ xmlns="http://www.w3.org/2000/svg"
+ xmlns:sodipodi="http://sodipodi.sourceforge.net/DTD/sodipodi-0.dtd"
+ xmlns:inkscape="http://www.inkscape.org/namespaces/inkscape"
+ width="170mm"
+ height="110mm"
+ viewBox="0 0 170 110"
+ version="1.1"
+ id="svg8">
+ <defs
+ id="defs2" />
+ <g
+ inkscape:label="Layer 1"
+ inkscape:groupmode="layer"
+ id="layer1">
+ <text
+ xml:space="preserve"
+ style="font-size:4.93889px;line-height:1.25;font-family:sans-serif;word-spacing:0px;stroke-width:0.264583"
+ x="89.958336"
+ y="105.83334"
+ id="text1921"><tspan
+ sodipodi:role="line"
+ id="tspan1919"
+ x="89.958336"
+ y="105.83334"
+ style="font-size:4.93889px;text-align:center;text-anchor:middle;stroke-width:0.264583">⊥ = {}</tspan></text>
+ <text
+ xml:space="preserve"
+ style="font-size:4.93889px;line-height:1.25;font-family:sans-serif;text-align:center;word-spacing:0px;text-anchor:middle;stroke-width:0.264583"
+ x="4.0951862"
+ y="76.729172"
+ id="text1925"><tspan
+ sodipodi:role="line"
+ id="tspan1923"
+ x="4.0951862"
+ y="76.729172"
+ style="font-size:4.93889px;text-align:center;text-anchor:middle;stroke-width:0.264583">…</tspan></text>
+ <text
+ id="text1925-6"
+ y="76.729172"
+ x="27.907686"
+ style="font-size:4.9389px;line-height:1.25;font-family:sans-serif;text-align:center;word-spacing:0px;text-anchor:middle;stroke-width:0.264583"
+ xml:space="preserve"><tspan
+ style="font-size:4.9389px;text-align:center;text-anchor:middle;stroke-width:0.264583"
+ y="76.729172"
+ x="27.907686"
+ id="tspan1923-9"
+ sodipodi:role="line">…</tspan></text>
+ <text
+ id="text1925-7"
+ y="76.729172"
+ x="16.001438"
+ style="font-size:4.9389px;line-height:1.25;font-family:sans-serif;text-align:center;word-spacing:0px;text-anchor:middle;stroke-width:0.264583"
+ xml:space="preserve"><tspan
+ style="font-size:4.9389px;text-align:center;text-anchor:middle;stroke-width:0.264583"
+ y="76.729172"
+ x="16.001438"
+ id="tspan1923-8"
+ sodipodi:role="line">{−9}</tspan></text>
+ <text
+ xml:space="preserve"
+ style="font-size:4.9389px;line-height:1.25;font-family:sans-serif;text-align:center;word-spacing:0px;text-anchor:middle;stroke-width:0.264583"
+ x="39.813934"
+ y="76.729172"
+ id="text1925-7-7"><tspan
+ sodipodi:role="line"
+ id="tspan1923-8-1"
+ x="39.813934"
+ y="76.729172"
+ style="font-size:4.9389px;text-align:center;text-anchor:middle;stroke-width:0.264583">{−5}</tspan></text>
+ <text
+ xml:space="preserve"
+ style="font-size:4.9389px;line-height:1.25;font-family:sans-serif;text-align:center;word-spacing:0px;text-anchor:middle;stroke-width:0.264583"
+ x="51.720184"
+ y="76.729172"
+ id="text1925-6-4"><tspan
+ sodipodi:role="line"
+ id="tspan1923-9-4"
+ x="51.720184"
+ y="76.729172"
+ style="font-size:4.9389px;text-align:center;text-anchor:middle;stroke-width:0.264583">…</tspan></text>
+ <text
+ id="text1925-7-7-6"
+ y="76.729172"
+ x="63.626438"
+ style="font-size:4.9389px;line-height:1.25;font-family:sans-serif;text-align:center;word-spacing:0px;text-anchor:middle;stroke-width:0.264583"
+ xml:space="preserve"><tspan
+ style="font-size:4.9389px;text-align:center;text-anchor:middle;stroke-width:0.264583"
+ y="76.729172"
+ x="63.626438"
+ id="tspan1923-8-1-9"
+ sodipodi:role="line">{−3}</tspan></text>
+ <text
+ id="text1925-7-7-67"
+ y="76.729172"
+ x="79.501442"
+ style="font-size:4.9389px;line-height:1.25;font-family:sans-serif;text-align:center;word-spacing:0px;text-anchor:middle;stroke-width:0.264583"
+ xml:space="preserve"><tspan
+ style="font-size:4.9389px;text-align:center;text-anchor:middle;stroke-width:0.264583"
+ y="76.729172"
+ x="79.501442"
+ id="tspan1923-8-1-8"
+ sodipodi:role="line">{−2}</tspan></text>
+ <text
+ id="text1925-7-7-9"
+ y="76.729172"
+ x="95.37645"
+ style="font-size:4.9389px;line-height:1.25;font-family:sans-serif;text-align:center;word-spacing:0px;text-anchor:middle;stroke-width:0.264583"
+ xml:space="preserve"><tspan
+ style="font-size:4.9389px;text-align:center;text-anchor:middle;stroke-width:0.264583"
+ y="76.729172"
+ x="95.37645"
+ id="tspan1923-8-1-1"
+ sodipodi:role="line">{−1}</tspan></text>
+ <text
+ id="text1925-7-7-7"
+ y="76.729172"
+ x="109.92851"
+ style="font-size:4.9389px;line-height:1.25;font-family:sans-serif;text-align:center;word-spacing:0px;text-anchor:middle;stroke-width:0.264583"
+ xml:space="preserve"><tspan
+ style="font-size:4.9389px;text-align:center;text-anchor:middle;stroke-width:0.264583"
+ y="76.729172"
+ x="109.92851"
+ id="tspan1923-8-1-0"
+ sodipodi:role="line">{0}</tspan></text>
+ <text
+ id="text1925-7-7-3"
+ y="76.729172"
+ x="123.15768"
+ style="font-size:4.9389px;line-height:1.25;font-family:sans-serif;text-align:center;word-spacing:0px;text-anchor:middle;stroke-width:0.264583"
+ xml:space="preserve"><tspan
+ style="font-size:4.9389px;text-align:center;text-anchor:middle;stroke-width:0.264583"
+ y="76.729172"
+ x="123.15768"
+ id="tspan1923-8-1-6"
+ sodipodi:role="line">{1}</tspan></text>
+ <text
+ xml:space="preserve"
+ style="font-size:4.9389px;line-height:1.25;font-family:sans-serif;text-align:center;word-spacing:0px;text-anchor:middle;stroke-width:0.264583"
+ x="136.38686"
+ y="76.729172"
+ id="text1925-7-7-3-3"><tspan
+ sodipodi:role="line"
+ id="tspan1923-8-1-6-8"
+ x="136.38686"
+ y="76.729172"
+ style="font-size:4.9389px;text-align:center;text-anchor:middle;stroke-width:0.264583">{2}</tspan></text>
+ <text
+ xml:space="preserve"
+ style="font-size:4.9389px;line-height:1.25;font-family:sans-serif;text-align:center;word-spacing:0px;text-anchor:middle;stroke-width:0.264583"
+ x="149.61603"
+ y="76.729172"
+ id="text1925-7-7-3-31"><tspan
+ sodipodi:role="line"
+ id="tspan1923-8-1-6-5"
+ x="149.61603"
+ y="76.729172"
+ style="font-size:4.9389px;text-align:center;text-anchor:middle;stroke-width:0.264583">{3}</tspan></text>
+ <text
+ id="text1925-6-4-0"
+ y="76.729172"
+ x="160.19936"
+ style="font-size:4.9389px;line-height:1.25;font-family:sans-serif;text-align:center;word-spacing:0px;text-anchor:middle;stroke-width:0.264583"
+ xml:space="preserve"><tspan
+ style="font-size:4.9389px;text-align:center;text-anchor:middle;stroke-width:0.264583"
+ y="76.729172"
+ x="160.19936"
+ id="tspan1923-9-4-8"
+ sodipodi:role="line">…</tspan></text>
+ <path
+ style="fill:none;stroke:#000000;stroke-width:0.264583px;stroke-linecap:butt;stroke-linejoin:miter;stroke-opacity:1"
+ d="M 16.001436,78.052083 90.084773,100.54166"
+ id="path2089"
+ sodipodi:nodetypes="cc" />
+ <path
+ style="fill:none;stroke:#000000;stroke-width:0.264583px;stroke-linecap:butt;stroke-linejoin:miter;stroke-opacity:1"
+ d="M 39.813936,78.052083 90.084773,100.54166"
+ id="path2091"
+ sodipodi:nodetypes="cc" />
+ <path
+ style="fill:none;stroke:#000000;stroke-width:0.264583px;stroke-linecap:butt;stroke-linejoin:miter;stroke-opacity:1"
+ d="M 63.626436,78.052083 90.084773,100.54166"
+ id="path2093"
+ sodipodi:nodetypes="cc" />
+ <path
+ style="fill:none;stroke:#000000;stroke-width:0.264583px;stroke-linecap:butt;stroke-linejoin:miter;stroke-opacity:1"
+ d="M 79.501436,78.052083 90.084773,100.54166"
+ id="path2095"
+ sodipodi:nodetypes="cc" />
+ <path
+ style="fill:none;stroke:#000000;stroke-width:0.264583px;stroke-linecap:butt;stroke-linejoin:miter;stroke-opacity:1"
+ d="m 95.376433,78.052083 -5.29166,22.489577"
+ id="path2097"
+ sodipodi:nodetypes="cc" />
+ <path
+ style="fill:none;stroke:#000000;stroke-width:0.264583px;stroke-linecap:butt;stroke-linejoin:miter;stroke-opacity:1"
+ d="M 109.92852,78.052083 90.084773,100.54166"
+ id="path2099"
+ sodipodi:nodetypes="cc" />
+ <path
+ style="fill:none;stroke:#000000;stroke-width:0.264583px;stroke-linecap:butt;stroke-linejoin:miter;stroke-opacity:1"
+ d="M 123.15768,78.052083 90.084773,100.54166"
+ id="path2101"
+ sodipodi:nodetypes="cc" />
+ <path
+ style="fill:none;stroke:#000000;stroke-width:0.264583px;stroke-linecap:butt;stroke-linejoin:miter;stroke-opacity:1"
+ d="M 136.38685,78.052082 90.084773,100.54166"
+ id="path2121" />
+ <path
+ style="fill:none;stroke:#000000;stroke-width:0.264583px;stroke-linecap:butt;stroke-linejoin:miter;stroke-opacity:1"
+ d="M 149.61601,78.052082 90.084773,100.54166"
+ id="path2123" />
+ <text
+ id="text1925-62"
+ y="50.270832"
+ x="9.3868532"
+ style="font-size:4.9389px;line-height:1.25;font-family:sans-serif;text-align:center;word-spacing:0px;text-anchor:middle;stroke-width:0.264583"
+ xml:space="preserve"><tspan
+ style="font-size:4.9389px;text-align:center;text-anchor:middle;stroke-width:0.264583"
+ y="50.270832"
+ x="9.3868532"
+ id="tspan1923-98"
+ sodipodi:role="line">…</tspan></text>
+ <text
+ xml:space="preserve"
+ style="font-size:4.9389px;line-height:1.25;font-family:sans-serif;text-align:center;word-spacing:0px;text-anchor:middle;stroke-width:0.264583"
+ x="53.043102"
+ y="50.270832"
+ id="text1925-6-6"><tspan
+ sodipodi:role="line"
+ id="tspan1923-9-0"
+ x="53.043102"
+ y="50.270832"
+ style="font-size:4.9389px;text-align:center;text-anchor:middle;stroke-width:0.264583">…</tspan></text>
+ <text
+ xml:space="preserve"
+ style="font-size:4.9389px;line-height:1.25;font-family:sans-serif;text-align:center;word-spacing:0px;text-anchor:middle;stroke-width:0.264583"
+ x="29.230604"
+ y="50.270832"
+ id="text1925-7-6"><tspan
+ sodipodi:role="line"
+ id="tspan1923-8-18"
+ x="29.230604"
+ y="50.270832"
+ style="font-size:4.9389px;text-align:center;text-anchor:middle;stroke-width:0.264583">{−9, −5}</tspan></text>
+ <text
+ id="text1925-7-7-31"
+ y="50.270832"
+ x="79.501442"
+ style="font-size:4.9389px;line-height:1.25;font-family:sans-serif;text-align:center;word-spacing:0px;text-anchor:middle;stroke-width:0.264583"
+ xml:space="preserve"><tspan
+ style="font-size:4.9389px;text-align:center;text-anchor:middle;stroke-width:0.264583"
+ y="50.270832"
+ x="79.501442"
+ id="tspan1923-8-1-87"
+ sodipodi:role="line">{−3, −1}</tspan></text>
+ <text
+ id="text1925-6-4-5"
+ y="50.270832"
+ x="108.60561"
+ style="font-size:4.9389px;line-height:1.25;font-family:sans-serif;text-align:center;word-spacing:0px;text-anchor:middle;stroke-width:0.264583"
+ xml:space="preserve"><tspan
+ style="font-size:4.9389px;text-align:center;text-anchor:middle;stroke-width:0.264583"
+ y="50.270832"
+ x="108.60561"
+ id="tspan1923-9-4-85"
+ sodipodi:role="line">…</tspan></text>
+ <text
+ xml:space="preserve"
+ style="font-size:4.9389px;line-height:1.25;font-family:sans-serif;text-align:center;word-spacing:0px;text-anchor:middle;stroke-width:0.264583"
+ x="129.77228"
+ y="50.270832"
+ id="text1925-7-7-6-0"><tspan
+ sodipodi:role="line"
+ id="tspan1923-8-1-9-0"
+ x="129.77228"
+ y="50.270832"
+ style="font-size:4.9389px;text-align:center;text-anchor:middle;stroke-width:0.264583">{1, 2}</tspan></text>
+ <text
+ xml:space="preserve"
+ style="font-size:4.9389px;line-height:1.25;font-family:sans-serif;text-align:center;word-spacing:0px;text-anchor:middle;stroke-width:0.264583"
+ x="149.61603"
+ y="50.270832"
+ id="text1925-6-4-5-3"><tspan
+ sodipodi:role="line"
+ id="tspan1923-9-4-85-4"
+ x="149.61603"
+ y="50.270832"
+ style="font-size:4.9389px;text-align:center;text-anchor:middle;stroke-width:0.264583">…</tspan></text>
+ <path
+ sodipodi:nodetypes="cc"
+ style="fill:none;stroke:#000000;stroke-width:0.264583px;stroke-linecap:butt;stroke-linejoin:miter;stroke-opacity:1"
+ d="M 16.001436,71.437499 29.230603,51.59375"
+ id="path2191" />
+ <path
+ sodipodi:nodetypes="cc"
+ style="fill:none;stroke:#000000;stroke-width:0.264583px;stroke-linecap:butt;stroke-linejoin:miter;stroke-opacity:1"
+ d="M 39.813936,71.437499 29.230603,51.59375"
+ id="path2193" />
+ <path
+ sodipodi:nodetypes="cc"
+ style="fill:none;stroke:#000000;stroke-width:0.264583px;stroke-linecap:butt;stroke-linejoin:miter;stroke-opacity:1"
+ d="M 63.626435,71.437499 79.501436,51.59375"
+ id="path2195" />
+ <path
+ sodipodi:nodetypes="cc"
+ style="fill:none;stroke:#000000;stroke-width:0.264583px;stroke-linecap:butt;stroke-linejoin:miter;stroke-opacity:1"
+ d="M 95.376433,71.437499 79.501436,51.59375"
+ id="path2197" />
+ <path
+ sodipodi:nodetypes="cc"
+ style="fill:none;stroke:#000000;stroke-width:0.264583px;stroke-linecap:butt;stroke-linejoin:miter;stroke-opacity:1"
+ d="M 124.4806,71.437499 129.77227,51.59375"
+ id="path2199" />
+ <path
+ sodipodi:nodetypes="cc"
+ style="fill:none;stroke:#000000;stroke-width:0.264583px;stroke-linecap:butt;stroke-linejoin:miter;stroke-opacity:1"
+ d="M 135.06393,71.437499 129.77227,51.59375"
+ id="path2201" />
+ <path
+ id="path2201-1"
+ d="M 129.77226,44.979165 128.44935,25.135416"
+ style="fill:none;stroke:#000000;stroke-width:0.264583px;stroke-linecap:butt;stroke-linejoin:miter;stroke-opacity:1"
+ sodipodi:nodetypes="cc" />
+ <text
+ id="text1925-7-7-6-0-2"
+ y="23.812502"
+ x="128.44936"
+ style="font-size:4.9389px;line-height:1.25;font-family:sans-serif;text-align:center;word-spacing:0px;text-anchor:middle;stroke-width:0.264583"
+ xml:space="preserve"><tspan
+ style="font-size:4.9389px;text-align:center;text-anchor:middle;stroke-width:0.264583"
+ y="23.812502"
+ x="128.44936"
+ id="tspan1923-8-1-9-0-9"
+ sodipodi:role="line">{1, 2, 3}</tspan></text>
+ <path
+ id="path205"
+ d="M 149.61601,71.437499 128.44935,25.135416"
+ style="fill:none;stroke:#000000;stroke-width:0.264583px;stroke-linecap:butt;stroke-linejoin:miter;stroke-opacity:1" />
+ <text
+ xml:space="preserve"
+ style="font-size:4.9389px;line-height:1.25;font-family:sans-serif;text-align:center;word-spacing:0px;text-anchor:middle;stroke-width:0.264583"
+ x="112.57436"
+ y="23.812502"
+ id="text1925-6-4-5-0"><tspan
+ sodipodi:role="line"
+ id="tspan1923-9-4-85-5"
+ x="112.57436"
+ y="23.812502"
+ style="font-size:4.9389px;text-align:center;text-anchor:middle;stroke-width:0.264583">…</tspan></text>
+ <text
+ xml:space="preserve"
+ style="font-size:4.9389px;line-height:1.25;font-family:sans-serif;text-align:center;word-spacing:0px;text-anchor:middle;stroke-width:0.264583"
+ x="143.00143"
+ y="23.812502"
+ id="text1925-6-4-5-7"><tspan
+ sodipodi:role="line"
+ id="tspan1923-9-4-85-0"
+ x="143.00143"
+ y="23.812502"
+ style="font-size:4.9389px;text-align:center;text-anchor:middle;stroke-width:0.264583">…</tspan></text>
+ <text
+ xml:space="preserve"
+ style="font-size:4.9389px;line-height:1.25;font-family:sans-serif;text-align:center;word-spacing:0px;text-anchor:middle;stroke-width:0.264583"
+ x="90.084763"
+ y="6.6145835"
+ id="text1925-7-7-6-0-2-0"><tspan
+ sodipodi:role="line"
+ id="tspan1923-8-1-9-0-9-0"
+ x="90.084763"
+ y="6.6145835"
+ style="font-size:4.9389px;text-align:center;text-anchor:middle;stroke-width:0.264583">(goes up infinitely)</tspan></text>
+ <path
+ id="path253"
+ d="M 90.084773,7.9374993 128.44935,18.520833"
+ style="fill:none;stroke:#000000;stroke-width:0.265;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:4;stroke-dasharray:2.12, 2.12;stroke-dashoffset:0;stroke-opacity:1" />
+ <path
+ sodipodi:nodetypes="cc"
+ style="fill:none;stroke:#000000;stroke-width:0.264999;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:4;stroke-dasharray:2.12, 2.12;stroke-dashoffset:0;stroke-opacity:1"
+ d="M 90.084773,7.9375003 108.6056,44.979166"
+ id="path253-2" />
+ <path
+ sodipodi:nodetypes="cc"
+ style="fill:none;stroke:#000000;stroke-width:0.264999;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:4;stroke-dasharray:2.12, 2.12;stroke-dashoffset:0;stroke-opacity:1"
+ d="M 90.084773,7.9375003 79.501436,44.979166"
+ id="path253-8" />
+ <path
+ sodipodi:nodetypes="cc"
+ style="fill:none;stroke:#000000;stroke-width:0.264999;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:4;stroke-dasharray:2.12, 2.12;stroke-dashoffset:0;stroke-opacity:1"
+ d="M 90.084773,7.9375003 53.043103,44.979166"
+ id="path253-6" />
+ <path
+ sodipodi:nodetypes="cc"
+ style="fill:none;stroke:#000000;stroke-width:0.264999;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:4;stroke-dasharray:2.12, 2.12;stroke-dashoffset:0;stroke-opacity:1"
+ d="M 90.084773,7.9375003 29.230603,44.979166"
+ id="path253-4" />
+ </g>
+</svg>
diff --git a/docs/DataFlowAnalysisIntroImages/OutputParameterIdentificationLattice.svg b/docs/DataFlowAnalysisIntroImages/OutputParameterIdentificationLattice.svg
new file mode 100644
index 0000000..5658587
--- /dev/null
+++ b/docs/DataFlowAnalysisIntroImages/OutputParameterIdentificationLattice.svg
@@ -0,0 +1,340 @@
+<?xml version="1.0" encoding="UTF-8" standalone="no"?>
+<svg
+ xmlns:dc="http://purl.org/dc/elements/1.1/"
+ xmlns:cc="http://creativecommons.org/ns#"
+ xmlns:rdf="http://www.w3.org/1999/02/22-rdf-syntax-ns#"
+ xmlns:svg="http://www.w3.org/2000/svg"
+ xmlns="http://www.w3.org/2000/svg"
+ xmlns:sodipodi="http://sodipodi.sourceforge.net/DTD/sodipodi-0.dtd"
+ xmlns:inkscape="http://www.inkscape.org/namespaces/inkscape"
+ id="svg8"
+ version="1.1"
+ viewBox="0 0 200 150"
+ height="150mm"
+ width="200mm">
+ <defs
+ id="defs2">
+ <marker
+ inkscape:stockid="Arrow2Lend"
+ orient="auto"
+ refY="0"
+ refX="0"
+ id="marker1403"
+ style="overflow:visible"
+ inkscape:isstock="true">
+ <path
+ id="path1401"
+ style="fill:#000000;fill-opacity:1;fill-rule:evenodd;stroke:#000000;stroke-width:0.625;stroke-linejoin:round;stroke-opacity:1"
+ d="M 8.7185878,4.0337352 -2.2072895,0.01601326 8.7185884,-4.0017078 c -1.7454984,2.3720609 -1.7354408,5.6174519 -6e-7,8.035443 z"
+ transform="matrix(-1.1,0,0,-1.1,-1.1,0)" />
+ </marker>
+ <marker
+ inkscape:stockid="Arrow2Lend"
+ orient="auto"
+ refY="0"
+ refX="0"
+ id="marker1393"
+ style="overflow:visible"
+ inkscape:isstock="true">
+ <path
+ id="path1391"
+ style="fill:#000000;fill-opacity:1;fill-rule:evenodd;stroke:#000000;stroke-width:0.625;stroke-linejoin:round;stroke-opacity:1"
+ d="M 8.7185878,4.0337352 -2.2072895,0.01601326 8.7185884,-4.0017078 c -1.7454984,2.3720609 -1.7354408,5.6174519 -6e-7,8.035443 z"
+ transform="matrix(-1.1,0,0,-1.1,-1.1,0)" />
+ </marker>
+ <marker
+ inkscape:stockid="Arrow2Lend"
+ orient="auto"
+ refY="0"
+ refX="0"
+ id="marker1383"
+ style="overflow:visible"
+ inkscape:isstock="true">
+ <path
+ id="path1381"
+ style="fill:#000000;fill-opacity:1;fill-rule:evenodd;stroke:#000000;stroke-width:0.625;stroke-linejoin:round;stroke-opacity:1"
+ d="M 8.7185878,4.0337352 -2.2072895,0.01601326 8.7185884,-4.0017078 c -1.7454984,2.3720609 -1.7354408,5.6174519 -6e-7,8.035443 z"
+ transform="matrix(-1.1,0,0,-1.1,-1.1,0)" />
+ </marker>
+ <marker
+ inkscape:stockid="Arrow2Lend"
+ orient="auto"
+ refY="0"
+ refX="0"
+ id="marker1373"
+ style="overflow:visible"
+ inkscape:isstock="true">
+ <path
+ id="path1371"
+ style="fill:#000000;fill-opacity:1;fill-rule:evenodd;stroke:#000000;stroke-width:0.625;stroke-linejoin:round;stroke-opacity:1"
+ d="M 8.7185878,4.0337352 -2.2072895,0.01601326 8.7185884,-4.0017078 c -1.7454984,2.3720609 -1.7354408,5.6174519 -6e-7,8.035443 z"
+ transform="matrix(-1.1,0,0,-1.1,-1.1,0)" />
+ </marker>
+ <marker
+ inkscape:stockid="Arrow2Lend"
+ orient="auto"
+ refY="0"
+ refX="0"
+ id="marker1363"
+ style="overflow:visible"
+ inkscape:isstock="true">
+ <path
+ id="path1361"
+ style="fill:#000000;fill-opacity:1;fill-rule:evenodd;stroke:#000000;stroke-width:0.625;stroke-linejoin:round;stroke-opacity:1"
+ d="M 8.7185878,4.0337352 -2.2072895,0.01601326 8.7185884,-4.0017078 c -1.7454984,2.3720609 -1.7354408,5.6174519 -6e-7,8.035443 z"
+ transform="matrix(-1.1,0,0,-1.1,-1.1,0)" />
+ </marker>
+ <marker
+ inkscape:stockid="Arrow2Lend"
+ orient="auto"
+ refY="0"
+ refX="0"
+ id="marker1353"
+ style="overflow:visible"
+ inkscape:isstock="true">
+ <path
+ id="path1351"
+ style="fill:#000000;fill-opacity:1;fill-rule:evenodd;stroke:#000000;stroke-width:0.625;stroke-linejoin:round;stroke-opacity:1"
+ d="M 8.7185878,4.0337352 -2.2072895,0.01601326 8.7185884,-4.0017078 c -1.7454984,2.3720609 -1.7354408,5.6174519 -6e-7,8.035443 z"
+ transform="matrix(-1.1,0,0,-1.1,-1.1,0)" />
+ </marker>
+ <marker
+ inkscape:stockid="Arrow2Lend"
+ orient="auto"
+ refY="0"
+ refX="0"
+ id="marker1343"
+ style="overflow:visible"
+ inkscape:isstock="true">
+ <path
+ id="path1341"
+ style="fill:#000000;fill-opacity:1;fill-rule:evenodd;stroke:#000000;stroke-width:0.625;stroke-linejoin:round;stroke-opacity:1"
+ d="M 8.7185878,4.0337352 -2.2072895,0.01601326 8.7185884,-4.0017078 c -1.7454984,2.3720609 -1.7354408,5.6174519 -6e-7,8.035443 z"
+ transform="matrix(-1.1,0,0,-1.1,-1.1,0)" />
+ </marker>
+ <marker
+ inkscape:stockid="Arrow2Lend"
+ orient="auto"
+ refY="0"
+ refX="0"
+ id="marker1333"
+ style="overflow:visible"
+ inkscape:isstock="true">
+ <path
+ id="path1331"
+ style="fill:#000000;fill-opacity:1;fill-rule:evenodd;stroke:#000000;stroke-width:0.625;stroke-linejoin:round;stroke-opacity:1"
+ d="M 8.7185878,4.0337352 -2.2072895,0.01601326 8.7185884,-4.0017078 c -1.7454984,2.3720609 -1.7354408,5.6174519 -6e-7,8.035443 z"
+ transform="matrix(-1.1,0,0,-1.1,-1.1,0)" />
+ </marker>
+ <marker
+ inkscape:stockid="Arrow2Lend"
+ orient="auto"
+ refY="0"
+ refX="0"
+ id="marker1323"
+ style="overflow:visible"
+ inkscape:isstock="true">
+ <path
+ id="path1321"
+ style="fill:#000000;fill-opacity:1;fill-rule:evenodd;stroke:#000000;stroke-width:0.625;stroke-linejoin:round;stroke-opacity:1"
+ d="M 8.7185878,4.0337352 -2.2072895,0.01601326 8.7185884,-4.0017078 c -1.7454984,2.3720609 -1.7354408,5.6174519 -6e-7,8.035443 z"
+ transform="matrix(-1.1,0,0,-1.1,-1.1,0)" />
+ </marker>
+ </defs>
+ <g
+ id="layer1"
+ inkscape:groupmode="layer"
+ inkscape:label="Layer 1">
+ <text
+ id="text855"
+ y="140.22917"
+ x="15.875002"
+ style="font-size:4.93889px;line-height:1.25;font-family:sans-serif;word-spacing:0px;stroke-width:0.264583"
+ xml:space="preserve"><tspan
+ dx="0"
+ style="font-size:4.93889px;stroke-width:0.264583"
+ y="140.22917"
+ x="15.875002"
+ id="tspan853"
+ sodipodi:role="line">Overwritten: {p->x, p->y, p->z}</tspan></text>
+ <text
+ xml:space="preserve"
+ style="font-size:4.9389px;line-height:1.25;font-family:sans-serif;word-spacing:0px;stroke-width:0.264583"
+ x="108.47917"
+ y="140.22917"
+ id="text855-4"><tspan
+ sodipodi:role="line"
+ id="tspan853-1"
+ x="108.47917"
+ y="140.22917"
+ style="font-size:4.9389px;stroke-width:0.264583"
+ dx="0">Overwritten: {p->x, p->z}</tspan></text>
+ <text
+ id="text855-4-1"
+ y="119.06249"
+ x="66.145836"
+ style="font-size:4.9389px;line-height:1.25;font-family:sans-serif;word-spacing:0px;stroke-width:0.264583"
+ xml:space="preserve"><tspan
+ dx="0"
+ style="font-size:4.9389px;stroke-width:0.264583"
+ y="119.06249"
+ x="66.145836"
+ id="tspan853-1-1"
+ sodipodi:role="line">Overwritten: {p->x, p->z}</tspan></text>
+ <text
+ id="text855-4-19"
+ y="111.12498"
+ x="140.22916"
+ style="font-size:4.9389px;line-height:1.25;font-family:sans-serif;word-spacing:0px;stroke-width:0.264583"
+ xml:space="preserve"><tspan
+ dx="0"
+ style="font-size:4.9389px;stroke-width:0.264583"
+ y="111.12498"
+ x="140.22916"
+ id="tspan853-1-0"
+ sodipodi:role="line">Overwritten: {p->q}</tspan></text>
+ <text
+ id="text855-4-2"
+ y="95.249992"
+ x="103.1875"
+ style="font-size:4.9389px;line-height:1.25;font-family:sans-serif;word-spacing:0px;stroke-width:0.264583"
+ xml:space="preserve"><tspan
+ dx="0"
+ style="font-size:4.9389px;stroke-width:0.264583"
+ y="95.249992"
+ x="103.1875"
+ id="tspan853-1-00"
+ sodipodi:role="line">Overwritten: {}</tspan></text>
+ <path
+ sodipodi:nodetypes="cc"
+ id="path909"
+ d="M 66.145835,134.93749 100.54167,121.70832"
+ style="fill:none;stroke:#000000;stroke-width:0.265;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:4;stroke-dasharray:none;stroke-opacity:1;marker-end:url(#marker1393)" />
+ <path
+ sodipodi:nodetypes="cc"
+ id="path911"
+ d="m 140.22917,134.93749 -39.6875,-13.22917"
+ style="fill:none;stroke:#000000;stroke-width:0.265;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:4;stroke-dasharray:none;stroke-opacity:1;marker-end:url(#marker1403)" />
+ <path
+ sodipodi:nodetypes="cc"
+ id="path913"
+ d="M 100.54167,113.77082 123.03126,96.572903"
+ style="fill:none;stroke:#000000;stroke-width:0.265;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:4;stroke-dasharray:none;stroke-opacity:1;marker-end:url(#marker1373)" />
+ <path
+ sodipodi:nodetypes="cc"
+ id="path915"
+ d="M 161.39584,105.83332 123.03126,96.572903"
+ style="fill:none;stroke:#000000;stroke-width:0.265;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:4;stroke-dasharray:none;stroke-opacity:1;marker-end:url(#marker1383)" />
+ <text
+ xml:space="preserve"
+ style="font-size:6.35px;line-height:1.25;font-family:sans-serif;word-spacing:0px;stroke-width:0.264583"
+ x="7.9375"
+ y="92.604179"
+ id="text855-4-2-6"><tspan
+ sodipodi:role="line"
+ id="tspan853-1-00-3"
+ x="7.9375"
+ y="92.604179"
+ style="font-size:6.35px;stroke-width:0.264583">Normal states</tspan></text>
+ <rect
+ y="84.666672"
+ x="2.6458333"
+ height="60.854164"
+ width="195.79167"
+ id="rect935"
+ style="fill:none;stroke:#000000;stroke-width:0.264999" />
+ <rect
+ y="2.6458333"
+ x="2.6458333"
+ height="71.4375"
+ width="195.79167"
+ id="rect937"
+ style="fill:none;stroke:#000000;stroke-width:0.264999" />
+ <text
+ id="text855-4-2-6-8"
+ y="10.583333"
+ x="7.9375"
+ style="font-size:6.35px;line-height:1.25;font-family:sans-serif;word-spacing:0px;stroke-width:0.264583"
+ xml:space="preserve"><tspan
+ style="font-size:6.35px;stroke-width:0.264583"
+ y="10.583333"
+ x="7.9375"
+ id="tspan853-1-00-3-4"
+ sodipodi:role="line">Failure states</tspan></text>
+ <text
+ xml:space="preserve"
+ style="font-size:4.9389px;line-height:1.25;font-family:sans-serif;word-spacing:0px;stroke-width:0.264583"
+ x="5.2916665"
+ y="68.791672"
+ id="text855-4-2-8"><tspan
+ sodipodi:role="line"
+ id="tspan853-1-00-5"
+ x="5.2916665"
+ y="68.791672"
+ style="font-size:4.9389px;stroke-width:0.264583">{Unsafe read at line 3}</tspan></text>
+ <text
+ id="text855-4-2-8-1"
+ y="68.791672"
+ x="66.145836"
+ style="font-size:4.9389px;line-height:1.25;font-family:sans-serif;word-spacing:0px;stroke-width:0.264583"
+ xml:space="preserve"><tspan
+ style="font-size:4.9389px;stroke-width:0.264583"
+ y="68.791672"
+ x="66.145836"
+ id="tspan853-1-00-5-1"
+ sodipodi:role="line">{Pointer escape at line 5}</tspan></text>
+ <text
+ id="text855-4-2-8-8"
+ y="68.791672"
+ x="134.9375"
+ style="font-size:4.9389px;line-height:1.25;font-family:sans-serif;word-spacing:0px;stroke-width:0.264583"
+ xml:space="preserve"><tspan
+ style="font-size:4.9389px;stroke-width:0.264583"
+ y="68.791672"
+ x="134.9375"
+ id="tspan853-1-00-5-8"
+ sodipodi:role="line">{Unsafe read at line 7}</tspan></text>
+ <text
+ id="text855-4-2-8-9"
+ y="44.979164"
+ x="7.9375"
+ style="font-size:4.9389px;line-height:1.25;font-family:sans-serif;word-spacing:0px;stroke-width:0.264583"
+ xml:space="preserve"><tspan
+ style="font-size:4.9389px;stroke-width:0.264583"
+ y="44.979164"
+ x="7.9375"
+ id="tspan853-1-00-5-4"
+ sodipodi:role="line">{Unsafe read at line 3, Pointer escape at line 5}</tspan></text>
+ <path
+ id="path1019"
+ d="m 31.75,63.499999 31.749999,-15.875"
+ style="fill:none;stroke:#000000;stroke-width:0.265;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:4;stroke-dasharray:none;stroke-opacity:1;marker-end:url(#marker1333)" />
+ <path
+ id="path1021"
+ d="m 100.54167,63.499999 -37.041671,-15.875"
+ style="fill:none;stroke:#000000;stroke-width:0.265;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:4;stroke-dasharray:none;stroke-opacity:1;marker-end:url(#marker1343)" />
+ <text
+ xml:space="preserve"
+ style="font-size:4.9389px;line-height:1.25;font-family:sans-serif;word-spacing:0px;stroke-width:0.264583"
+ x="10.583333"
+ y="23.812502"
+ id="text855-4-2-8-9-8"><tspan
+ id="tspan1041"
+ sodipodi:role="line"
+ x="10.583333"
+ y="23.812502"
+ style="font-size:4.9389px;stroke-width:0.264583">{Unsafe read at line 3, Pointer escape at line 5, Unsafe read at line 7}</tspan></text>
+ <path
+ id="path1045"
+ d="M 74.083332,39.687499 124.35417,26.458333"
+ style="fill:none;stroke:#000000;stroke-width:0.265;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:4;stroke-dasharray:none;stroke-opacity:1;marker-end:url(#marker1353)" />
+ <path
+ id="path1047"
+ d="M 161.39583,63.499999 124.35417,26.458333"
+ style="fill:none;stroke:#000000;stroke-width:0.265;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:4;stroke-dasharray:none;stroke-opacity:1;marker-end:url(#marker1363)" />
+ <path
+ id="path1049"
+ d="M 100.54167,84.666666 V 74.083333"
+ style="fill:none;stroke:#000000;stroke-width:0.265;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:4;stroke-dasharray:none;stroke-opacity:1;marker-end:url(#marker1323)" />
+ </g>
+</svg>
diff --git a/docs/DataFlowAnalysisIntroImages/UniquePtrLattice.svg b/docs/DataFlowAnalysisIntroImages/UniquePtrLattice.svg
new file mode 100644
index 0000000..f7a618a
--- /dev/null
+++ b/docs/DataFlowAnalysisIntroImages/UniquePtrLattice.svg
@@ -0,0 +1,114 @@
+<?xml version="1.0" encoding="UTF-8" standalone="no"?>
+<svg
+ xmlns:dc="http://purl.org/dc/elements/1.1/"
+ xmlns:cc="http://creativecommons.org/ns#"
+ xmlns:rdf="http://www.w3.org/1999/02/22-rdf-syntax-ns#"
+ xmlns:svg="http://www.w3.org/2000/svg"
+ xmlns="http://www.w3.org/2000/svg"
+ xmlns:sodipodi="http://sodipodi.sourceforge.net/DTD/sodipodi-0.dtd"
+ xmlns:inkscape="http://www.inkscape.org/namespaces/inkscape"
+ id="svg8"
+ version="1.1"
+ viewBox="0 0 120 40"
+ height="40mm"
+ width="120mm">
+ <defs
+ id="defs2">
+ <marker
+ inkscape:stockid="Arrow2Lend"
+ orient="auto"
+ refY="0.0"
+ refX="0.0"
+ id="marker1184"
+ style="overflow:visible;"
+ inkscape:isstock="true">
+ <path
+ id="path1182"
+ style="fill-rule:evenodd;stroke-width:0.625;stroke-linejoin:round;stroke:#000000;stroke-opacity:1;fill:#000000;fill-opacity:1"
+ d="M 8.7185878,4.0337352 L -2.2072895,0.016013256 L 8.7185884,-4.0017078 C 6.9730900,-1.6296469 6.9831476,1.6157441 8.7185878,4.0337352 z "
+ transform="scale(1.1) rotate(180) translate(1,0)" />
+ </marker>
+ <marker
+ inkscape:stockid="Arrow2Lend"
+ orient="auto"
+ refY="0.0"
+ refX="0.0"
+ id="marker1174"
+ style="overflow:visible;"
+ inkscape:isstock="true">
+ <path
+ id="path1172"
+ style="fill-rule:evenodd;stroke-width:0.625;stroke-linejoin:round;stroke:#000000;stroke-opacity:1;fill:#000000;fill-opacity:1"
+ d="M 8.7185878,4.0337352 L -2.2072895,0.016013256 L 8.7185884,-4.0017078 C 6.9730900,-1.6296469 6.9831476,1.6157441 8.7185878,4.0337352 z "
+ transform="scale(1.1) rotate(180) translate(1,0)" />
+ </marker>
+ </defs>
+ <g
+ id="layer1"
+ inkscape:groupmode="layer"
+ inkscape:label="Layer 1">
+ <text
+ id="text837"
+ y="10.639833"
+ x="60.836075"
+ style="font-size:4.93889px;line-height:1.25;font-family:sans-serif;text-align:center;word-spacing:0px;text-anchor:middle;stroke-width:0.264583"
+ xml:space="preserve"><tspan
+ style="font-size:4.93889px;text-align:center;text-anchor:middle;stroke-width:0.264583"
+ y="10.639833"
+ x="60.836075"
+ id="tspan835"
+ sodipodi:role="line">Conflicting</tspan></text>
+ <text
+ xml:space="preserve"
+ style="font-size:4.9389px;line-height:1.25;font-family:sans-serif;text-align:center;word-spacing:0px;text-anchor:middle;stroke-width:0.264583"
+ x="29.162045"
+ y="34.911739"
+ id="text837-3"><tspan
+ sodipodi:role="line"
+ id="tspan835-8"
+ x="29.162045"
+ y="34.911739"
+ style="font-size:4.9389px;text-align:center;text-anchor:middle;stroke-width:0.264583">Defined</tspan></text>
+ <text
+ id="text837-3-3"
+ y="34.911739"
+ x="92.612602"
+ style="font-size:4.9389px;line-height:1.25;font-family:sans-serif;text-align:center;word-spacing:0px;text-anchor:middle;stroke-width:0.264583"
+ xml:space="preserve"><tspan
+ style="font-size:4.9389px;text-align:center;text-anchor:middle;stroke-width:0.264583"
+ y="34.911739"
+ x="92.612602"
+ id="tspan835-8-3"
+ sodipodi:role="line">Compatible</tspan></text>
+ <rect
+ y="2.6458333"
+ x="34.395832"
+ height="13.229168"
+ width="52.91666"
+ id="rect875"
+ style="fill:none;stroke:#000000;stroke-width:0.264999" />
+ <rect
+ style="fill:none;stroke:#000000;stroke-width:0.264999"
+ id="rect875-9"
+ width="52.916664"
+ height="13.229168"
+ x="66.145828"
+ y="26.458334" />
+ <rect
+ style="fill:none;stroke:#000000;stroke-width:0.264999"
+ id="rect875-0"
+ width="52.916664"
+ height="13.229168"
+ x="2.6458352"
+ y="26.458334" />
+ <path
+ id="path898"
+ d="M 29.104166,26.458333 60.854166,15.875"
+ style="fill:none;stroke:#000000;stroke-width:0.265;stroke-linecap:butt;stroke-linejoin:miter;stroke-opacity:1;stroke-miterlimit:4;stroke-dasharray:none;marker-end:url(#marker1184)" />
+ <path
+ sodipodi:nodetypes="cc"
+ id="path900"
+ d="M 92.604167,26.458333 60.854166,15.875"
+ style="fill:none;stroke:#000000;stroke-width:0.265;stroke-linecap:butt;stroke-linejoin:miter;stroke-miterlimit:4;stroke-dasharray:none;stroke-opacity:1;marker-end:url(#marker1174)" />
+ </g>
+</svg>
diff --git a/docs/conf.py b/docs/conf.py
index 3af05ba..690c843 100644
--- a/docs/conf.py
+++ b/docs/conf.py
@@ -33,7 +33,24 @@
templates_path = ['_templates']
# The suffix of source filenames.
-source_suffix = '.rst'
+source_suffix = {
+ '.rst': 'restructuredtext',
+}
+
+try:
+ import recommonmark
+except ImportError:
+ # manpages do not use any .md sources
+ if not tags.has('builder-man'):
+ raise
+else:
+ import sphinx
+ if sphinx.version_info >= (3, 0):
+ # This requires 0.5 or later.
+ extensions.append('recommonmark')
+ else:
+ source_parsers = {'.md': 'recommonmark.parser.CommonMarkParser'}
+ source_suffix['.md'] = 'markdown'
# The encoding of source files.
#source_encoding = 'utf-8-sig'
diff --git a/docs/index.rst b/docs/index.rst
index b7caa65..604985c 100644
--- a/docs/index.rst
+++ b/docs/index.rst
@@ -25,6 +25,7 @@
CrossCompilation
ClangStaticAnalyzer
ThreadSafetyAnalysis
+ DataFlowAnalysisIntro
AddressSanitizer
ThreadSanitizer
MemorySanitizer
