= Notes on TASS AST and Translation to Model = == Elements of a TASS AST == Preprocessing: first, the file is preprocessed to create a stream of tokens with original source information. All AST nodes have source information. Types of AST Node * identifiers * type expressions * integer, real, boolean, char, t[], t*, record{...} * function definitions (body) * function declarations (no body) * type definitions (typedef...) * statements * assign * assert * pragma * string * assert, assume, invariant, input, output, ... * switch * if-then, if-then-else * while * for * until * break * compound ({...}) * variable declaration section * sequence of statements * variable declaration * with possible initialization expression * possible array extents information and other information modifying type? * static, ...? * expressions (may have side-effects) * literals (including named literals) * variable * operators: +,-,*,/,%,<,<=,>,>=,==,!=,!,&&,\|\| * special kinds of assignments: x++, x--, ++x, --x, x+=a, x*=a, ... * bit-wise operators? * &,* (pointer operations) * cast-to-t * a[i] (array index) * x.a (record navigation) * function invocation f(x) == Processing Stages == The AST can be used to represent the program at different stages of translation. Stages # All variables, types, etc., are represented simply as identifiers # Symbol table information is used to annotate the AST # (Static) types are created and associated to every expression # Variable objects are created and inserted into AST # Variables may be moved around to facilitate translation to model, .... Questions: * How to handle pre-processor macros? Include in AST? == C Example == {{{ #include #include int main(int argc, char *argv[]) { double result = 0.0; int n = atoi(argv[1]); int i; double a[n]; FILE *fp = fopen("data","r"); for (i=0; i 0.000000e+00 1 0 0 0 }}}