== Overview of Static Analysis ==

* Static analysis is applied after a CIVL-C model is obtained from an AST such that
 1. all concurrency dialect features are translated using CIVL-C primitives/libraries;
 1. side effects are only contained by assignment or function call;
 1. all unused code (statically) is removed;
 1. the main function doesn't take any parameters.

Therefore, the CIVL-C model which is the input of the static analysis also has the above features.

* Static analysis done by CIVL includes:
 1. purely local analysis
 1. identifying variable used as operand of address-of operator
 1. identifying assignment with left hand side being dereference expression (`*p=...`)
 1. identifying the applicable analyzer for each statement
     * currently...