== 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  ** details... **
     a. figure out purely local variables
     b. figure out purely local statements
     b. figure out purely local locations
 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, there is only one analyzer: `abs` (absolute value) call analyzer
 1. for locations:
     a. computing the set of variables writable at/from a location ** details... **
     b. purely local analysis
     c. loop analysis
  1. memory unit analysis:
      a. reachable memory units
      b. impact memory units