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;
  2. side effects are only contained by assignment or function call;
  3. all unused code (statically) is removed;
  4. 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
  2. identifying variable used as operand of address-of operator
  3. identifying assignment with left hand side being dereference expression (*p=...)
  4. identifying the applicable analyzer for each statement
     • currently...