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