| 1 | ABC: front end for C
|
|---|
| 2 | ast: this will have library functions and state like
|
|---|
| 3 | MPI_Send, blah blah blah
|
|---|
| 4 |
|
|---|
| 5 | SARL: symbolic algebra and reasoning library
|
|---|
| 6 | provides representation, manipulation of symbolic expressions
|
|---|
| 7 | interface to theorem provers, etc.
|
|---|
| 8 |
|
|---|
| 9 | GMC: generic model checker
|
|---|
| 10 | provides depth first search, printing traces, ...
|
|---|
| 11 |
|
|---|
| 12 | CIVL: Concurrency Intermeidate Verification Language
|
|---|
| 13 | ast: similar to ABC AST but simpler
|
|---|
| 14 | uses: (nothing)
|
|---|
| 15 | provides: AST
|
|---|
| 16 | notes: no type qualifiers or other complicated C stuff.
|
|---|
| 17 | functions can be defined in any scope
|
|---|
| 18 | eventually add pointer scope qualifiers, etc.
|
|---|
| 19 | provide a side-effect remover and ASTMerger (like a linker, for libraries)
|
|---|
| 20 |
|
|---|
| 21 | front: common interface for all CIVL front-ends
|
|---|
| 22 | uses: ast
|
|---|
| 23 | provides: FrontEnd
|
|---|
| 24 | notes: provides methods to parse a file and produce an AST
|
|---|
| 25 |
|
|---|
| 26 | civlc: grammar and parser for CIVL-C language
|
|---|
| 27 | uses: front, ast
|
|---|
| 28 | provides: CivlCFrontEnd
|
|---|
| 29 | notes: the grammar of the CIVL-C language should be very
|
|---|
| 30 | closely aligned with the CIVL AST.
|
|---|
| 31 | this module is like ABC, but results in a CIVL AST.
|
|---|
| 32 | also uses library files in lib
|
|---|
| 33 | could this use the AST preprocessor?
|
|---|
| 34 |
|
|---|
| 35 | lib: libraries written in CIVL-C: mp.civl, etc.
|
|---|
| 36 | how is state and definitions incorporated into the module?
|
|---|
| 37 | notes: this is not java source, just CIVL-C source
|
|---|
| 38 |
|
|---|
| 39 | c: translator from C code to CIVL AST
|
|---|
| 40 | uses: ABC, ast, front, civlc
|
|---|
| 41 | uses ABC to create ABC-AST, then translated that to CIVL-AST
|
|---|
| 42 | needs to translate library calls to CIVL libraries, e.g.,
|
|---|
| 43 | MPI_Send -> CIVL_MP_send, etc. Hence needs to civlc
|
|---|
| 44 | to parse and construct library modules, then merge them
|
|---|
| 45 | needs to introduce scopes for MPI processes etc
|
|---|
| 46 |
|
|---|
| 47 | model: representation of a CIVL model, like in CVT
|
|---|
| 48 | uses: ast
|
|---|
| 49 | provides: Model, ModelBuilder
|
|---|
| 50 | notes: ModelBuilder translates AST to Model
|
|---|
| 51 | Model elements maintain back-pointers to AST nodes
|
|---|
| 52 |
|
|---|
| 53 | translates AST to Model
|
|---|
| 54 |
|
|---|
| 55 | state: representation and manipulation of states of a Model
|
|---|
| 56 | note: like CVT, but no buffers
|
|---|
| 57 |
|
|---|
| 58 | transition:
|
|---|
| 59 |
|
|---|
| 60 | predicate:
|
|---|
| 61 |
|
|---|
| 62 | kripke:
|
|---|
| 63 |
|
|---|
