| | 1 | == Overview of Static Analysis == |
| | 2 | |
| | 3 | * Static analysis is applied after a CIVL-C model is obtained from an AST such that |
| | 4 | 1. all concurrency dialect features are translated using CIVL-C primitives/libraries; |
| | 5 | 1. side effects are only contained by assignment or function call; |
| | 6 | 1. all unused code (statically) is removed; |
| | 7 | 1. the main function doesn't take any parameters. |
| | 8 | |
| | 9 | Therefore, the CIVL-C model which is the input of the static analysis also has the above features. |
| | 10 | |
| | 11 | * Static analysis done by CIVL includes: |
| | 12 | 1. purely local analysis |
| | 13 | 1. identifying variable used as operand of address-of operator |
| | 14 | 1. identifying assignment with left hand side being dereference expression (`*p=...`) |
| | 15 | 1. identifying the applicable analyzer for each statement |
| | 16 | * currently... |
| | 17 | |
