| 73 | | * scope |
| 74 | | * name |
| 75 | | * type |
| 76 | | * function definition: a function with a body. As with variables, one def. can have many decls, but each decl is associated to at most one definition. |
| 77 | | * name |
| 78 | | * list of formal names and types |
| 79 | | * return type |
| 80 | | * statement (body) |
| 81 | | * function declaration: no body, just "prototype" in C |
| 82 | | * type definition node |
| 83 | | * name: string |
| 84 | | * theType: type (type being assigned a name) |
| 85 | | * statements |
| 86 | | * labels: set of labels associated to this statement. The labels all correspond to the point of control just before the statement. |
| 87 | | * assert: this could come from a program language assert or a TASS pragma |
| 88 | | * expr: Expression |
| 89 | | * assume: these come from TASS pragmas |
| 90 | | * expr: Expression |
| 91 | | * pragma (any kind of pragma, represented as just a string) |
| 92 | | * string: this is an initial form, where the text of the pragma is uninterpreted. After a certain processing stage, TASS pragmas will be parsed and replaced with more specific nodes. Non-tass pragmas will just remain as strings and will be ignored by TASS. |
| 93 | | * switch statement: this can be used to model C's switch |
| 94 | | * expression: expression that is evaluated |
| 95 | | * list of cases |
| 96 | | * value |
| 97 | | * statement (or something like that) |
| 98 | | * if-then, if-then-else |
| 99 | | * while: loop. associated invariant (derived from TASS invariant pragma) |
| 100 | | * for |
| 101 | | * do...until |
| | 73 | * methods |
| | 74 | * definition: VariableDeclarationNodeIF (may be null) |
| | 75 | * scope: ScopeIF |
| | 76 | * name: IdentifierNodeIF |
| | 77 | * type: TypeNodeIF |
| | 78 | * FunctionDefinitionNodeIF: a function with a body. As with variables, one def. can have many decls, but each decl is associated to at most one definition. |
| | 79 | * methods |
| | 80 | * name: IdentifierNodeIF |
| | 81 | * numInputs: int |
| | 82 | * input(int i): NameTypePairNodeIF |
| | 83 | * outputType: TypeNodeIF |
| | 84 | * body: BlockNodeIF |
| | 85 | * FunctionDeclarationNodeIF: no body, just "prototype" in C |
| | 86 | * methods |
| | 87 | * definition: FunctionDefinitionNodeIF (may be null) |
| | 88 | * name: IdentifierNodeIF |
| | 89 | * numInputs: int |
| | 90 | * input(int i): NameTypePairNodeIF |
| | 91 | * outputType: TypeNodeIF |
| | 92 | * TypeDefinitionNodeIF: "typedef" in C |
| | 93 | * methods |
| | 94 | * name: IdentifierNodeIF |
| | 95 | * type: TypeNodeIF (type being assigned a name) |
| | 96 | * StatementNodeIF |
| | 97 | * methods |
| | 98 | * labels: Collection<ASTLabelIF>: set of labels associated to this statement. The labels all correspond to the point of control just before the statement. |
| | 99 | * AssertStatementNodeIF: this could come from a program language assert or a TASS pragma |
| | 100 | * methods |
| | 101 | * expr: Expression |
| | 102 | * AssumeStatementNodeIF: these come from TASS pragmas |
| | 103 | * methods |
| | 104 | * expr: Expression |
| | 105 | * PragmaNodeIF:(any kind of pragma, represented as just a string |
| | 106 | * methods |
| | 107 | * string: this is an initial form, where the text of the pragma is uninterpreted. After a certain processing stage, TASS pragmas will be parsed and replaced with more specific nodes. Non-tass pragmas will just remain as strings and will be ignored by TASS. |
| | 108 | * SwitchStatementNodeIF: this can be used to model C's switch |
| | 109 | * methods |
| | 110 | * expression: expression that is evaluated |
| | 111 | * numCases: int |
| | 112 | * case(int i): ValueLocationPairNodeIF (ordered pair (v,l), where v is a ValueNodeIF, and l is an ASTStatementNodeIF) |
| | 113 | * default: ValueLocationPairNodeIF |
| | 114 | * IfThenElseStatementNodeIF |
| | 115 | * methods |
| | 116 | * condition: ExpressionNodeIF |
| | 117 | * trueBranch: StatementNodeIF |
| | 118 | * falseBranch: StatementNodeIF (may be null) |
| | 119 | * WhileLoopNodeIF: loop. associated invariant (derived from TASS invariant pragma) |
| | 120 | * methods |
| | 121 | * condition: ExpressionNodeIF |
| | 122 | * body: StatementNodeIF |
| | 123 | * invariants: Collection<ExpressionNodeIF> ? |
| | 124 | * ForLoopNodeIF |
| | 125 | * methods |
| | 126 | * initializer: StatementNodeIF |
| | 127 | * condition: ExpressionNodeIF |
| | 128 | * incrementer: StatementNodeIF |
| | 129 | * body: StatementNodeIF |
| | 130 | * DoUntilNodeIF |
