| 70 | | ASTNodeIF extends SourceableIF |
| 71 | | * methods |
| 72 | | * numChildren: int |
| 73 | | * child(int i): ASTNodeIF |
| 74 | | * children: Iterator<ASTNodeIF> |
| 75 | | |
| 76 | | The following extend ASTNodeIF: |
| 77 | | * ReferenceNodeIF |
| 78 | | * has no children |
| 79 | | * used to refer to another node u when u might be referenced from several places (shared) |
| 80 | | * methods |
| 81 | | * referent: ASTNodeIF |
| 82 | | * identifier: string ? |
| 83 | | * IdentifierNodeIF: wraps a string. represents an identifier occurrence in code. Has 0 children, i.e., is a leaf node. |
| 84 | | * methods |
| 85 | | * name: string |
| 86 | | * TypeNodeIF: a type expression |
| 87 | | * TypeReferenceNodeIF |
| 88 | | * no children |
| 89 | | * methods |
| 90 | | * referent: TypeNodeIF: the type being referred to |
| 91 | | * VoidTypeNodeIF: the type "void" used, for example, as the return type for a function that does not return anything |
| 92 | | * no children |
| 93 | | * IntegerTypeNodeIF: an integer type, such as "int" or "long int" or "short int" in C |
| 94 | | * integer sub-types, specified by parameters |
| 95 | | * no children |
| 96 | | * RealTypeNodeIF: a real type, such as "float" or "double" in C |
| 97 | | * real sub-stypes, specified by parameters (e.g., IEEE754 floating point numbers) |
| 98 | | * no children |
| 99 | | * BooleanTypeNodeIF: the boolean type |
| 100 | | * no children |
| 101 | | * CharacterTypeNodeIF: the character type (char in C) |
| 102 | | * no children |
| 103 | | * ArrayTypeNodeIF: an array type |
| 104 | | * children |
| 105 | | * elementType: TypeNodeIF |
| 106 | | * extent: ? This is complicated. The extent might be an expression involving input variables. |
| 107 | | * PointerTypeNodeIF |
| 108 | | * children |
| 109 | | * baseType: TypeNodeIF |
| 110 | | * CompositeTypeNodeIF: "struct" or "union" in C |
| 111 | | * children |
| 112 | | * name: IdentifierNodeIF |
| 113 | | * fields: SequenceNode<PairNode<IdentifierNodeIF,TypeNodeIF>> |
| 114 | | * methods |
| 115 | | * isUnion: boolean |
| 116 | | * FunctionTypeNodeIF |
| 117 | | * children |
| 118 | | * inputTypes: SequenceNode<TypeNodeIF> |
| 119 | | * outputType: TypeNodeIF |
| 120 | | * EnumerationTypeNodeIF |
| 121 | | * children |
| 122 | | * SequenceNode<PairNode<IdentifierNodeIF, LiteralNodeIF>> |
| 123 | | * VariableDeclarationNodeIF |
| 124 | | * Every variable is defined at one unique location in the code. The variable can be declared in several places. Each declaration has an associated definition. There can be many decls associated to one def. This is a linking thing: a single variable that is to be used in several files will be defined in one file but be declared in all |
| 125 | | * children |
| 126 | | * name: IdentifierNodeIF |
| 127 | | * type: TypeNodeIF |
| 128 | | * initializer: ExpressionNodeIF : the initialization expression for this variable. May be null. Only a defining node an have such an expression. |
| 129 | | * definition: VariableDeclarationNodeIF : the defining declaration (may be null at first) |
| 130 | | * methods |
| 131 | | * isDefinition: boolean : is this the defining declaration? |
| 132 | | * scope: ScopeIF |
| 133 | | * typeQualifier: CONST, VOLATILE |
| 134 | | * storageClass: EXTERNAL, AUTO, STATIC, REGISTER |
| 135 | | * FunctionDeclarationNodeIF |
| 136 | | * analogous to situation with variables, with the function body playing the role of variable initializer. I.e., a function may have several declarations ("prototypes" in C), but only one definition (i.e., one with a body). |
| 137 | | * methods |
| 138 | | * isDefinition: boolean |
| 139 | | * definition: FunctionDeclarationNodeIF : the defining declaration (the one with a body) |
| 140 | | * name: IdentifierNodeIF |
| 141 | | * numFormals: int |
| 142 | | * formal(int i): VariableDeclarationNodeIF |
| 143 | | * formals: Iterator<VariableDeclarationNodeIF> |
| 144 | | * outputType: TypeNodeIF |
| 145 | | * body: BlockNodeIF (null iff !isDefinition) |
| 146 | | * TypeDefinitionNodeIF |
| 147 | | * a "typedef" in C |
| 148 | | * methods |
| 149 | | * name: IdentifierNodeIF |
| 150 | | * type: TypeNodeIF (type being assigned a name) |
| 151 | | * LabelNodeIF: a label preceding a statement |
| 152 | | * children |
| 153 | | * identifier: IdentifierNodeIF: the name of this label (child) |
| 154 | | * methods |
| 155 | | * statement: StatementNodeIF : the statement this label precedes (this may be null at first) |
| 156 | | * StatementNodeIF |
| 157 | | * methods |
| 158 | | * labels: Collection<LabelNodeIF>: set of labels associated to this statement. The labels all correspond to the point of control just before the statement. |
| 159 | | * AssertStatementNodeIF |
| 160 | | * this could come from a program language assert or a TASS pragma |
| 161 | | * methods |
| 162 | | * expr: ExpressionNodeIF |
| 163 | | * AssumeStatementNodeIF |
| 164 | | * these come from TASS pragmas |
| 165 | | * methods |
| 166 | | * expr: ExpressionNodeIF |
| 167 | | * PragmaNodeIF |
| 168 | | * any kind of pragma, represented as just a string |
| 169 | | * methods |
| 170 | | * 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. |
| 171 | | * SwitchStatementNodeIF |
| 172 | | * can be used to model C's switch, for example |
| 173 | | * methods |
| 174 | | * expression: ExpressionNodeIF: expression that is evaluated |
| 175 | | * numCases: int |
| 176 | | * case(int i): Pair<ExpressionNodeIF,LabelReferenceNodeIF> |
| 177 | | * the expression is the value (usually literal) the switch expression might match; the label refers to a point in body of the switch statement |
| 178 | | * default: LabelReferenceNodeIF : where to go if none of the other cases is matched |
| 179 | | * body : StatementNodeIF |
| 180 | | * IfThenElseStatementNodeIF |
| 181 | | * methods |
| 182 | | * condition: ExpressionNodeIF |
| 183 | | * trueBranch: StatementNodeIF |
| 184 | | * falseBranch: StatementNodeIF (may be null) |
| 185 | | * WhileLoopNodeIF: loop |
| 186 | | * associated invariant (derived from TASS invariant pragma) |
| 187 | | * methods |
| 188 | | * condition: ExpressionNodeIF |
| 189 | | * body: StatementNodeIF |
| 190 | | * invariants: Collection<ExpressionNodeIF> ? |
| 191 | | * ForLoopNodeIF |
| 192 | | * methods |
| 193 | | * initializer: StatementNodeIF |
| 194 | | * condition: ExpressionNodeIF |
| 195 | | * incrementer: StatementNodeIF |
| 196 | | * body: StatementNodeIF |
| 197 | | * DoUntilNodeIF |
| 198 | | * BreakNodeIF |
| 199 | | * ContinueNodeIF |
| 200 | | * GotoNodeIF |
| 201 | | * label: LabelReferenceNodeIF |
| 202 | | * ReturnNodeIF |
| 203 | | * expression (may be null) |
| 204 | | * NoopNodeIF |
| 205 | | * BlockNodeIF: ({...} in C) |
| 206 | | * sequence of variable definitions |
| 207 | | * sequence of statements |
| 208 | | * ExpressionNodeIF: expressions--these are considered a kind of statement (as in C) |
| 209 | | * PureExpressionNodeIF: side-effect-free expressions |
| 210 | | * LiteralNodeIF (including named literals): integers, reals, strings, chars, enumValue |
| 211 | | * EnumElementReferenceNodeIF extends LiteralNodeIF |
| 212 | | * 0 children |
| 213 | | * referent: PairNode<IdentifierNodeIF, LiteralNodeIF> |
| 214 | | * VariableReferenceNodeIF |
| 215 | | * 0 children |
| 216 | | * referent: VariableDeclarationNodeIF |
| 217 | | * FunctionReferenceNodeIF |
| 218 | | * 0 children |
| 219 | | * referent: FunctionDeclarationNodeIF |
| 220 | | * OperatorNodeIF |
| 221 | | * ADD, ADD_POINTER_INT, ADDRESS_OF, BIT_AND, BIT_NOT, BIT_OR, BIT_XOR, DEREFERENCE, DIVIDE, EQUALS, GREATER_THAN, GTE, IF_THEN_ELSE, LEQ, LESS_THAN, LOGICAL_AND, LOGICAL_NOT, LOGICAL_OR, MODULO, MULTIPLY, NAVIGATE (DOT), NEGATIVE, NOT_EQUALS, SHIFT_LEFT, SHIFT_RIGHT, SUBSCRIPT, SUBTRACT, SUBTRACT_POINTER_INT, SUBTRACT_POINTER_POINTER |
| 222 | | * CastNodeIF |
| 223 | | * newType: TypeNodeIF (type you are casting to) |
| 224 | | * expression: ExpressionNodeIF |
| 225 | | * QuantifierNodeIF |
| 226 | | * quantifier: {FORALL, EXISTS, LAMBDA, UNIFORM, SUM} |
| 227 | | * boundVariable: VariableDefinitionNodeIF |
| 228 | | * constraint: ExpressionNodeIF |
| 229 | | * expression: ExpressionNodeIF |
| 230 | | * InitializerNodeIF: special kind of expression used to initialize variables in their decl |
| 231 | | * SizeOfNodeIF: type, expression, or string literal |
| 232 | | * StartOfNodeIF: &a[0] -- that is the Cil way of converting an array to pointer to first element |
| 233 | | * FunctionApplicationNodeIF: invocation f(x) when f is abstract (pure) function |
| 234 | | * methods |
| 235 | | * function: ExpressionNodeIF |
| 236 | | * an expression that evaluates to function type, e.g., *fptr |
| 237 | | * numParameters: int |
| 238 | | * argument(int i): ExpressionNodeIF |
| 239 | | * arguments: Iterator<ExpressionNodeIF> |
| 240 | | * ProcessReferenceNodeIF: PROC[expr].x |
| 241 | | * SideEffectExpressionNodeIF: expressions with side-effects |
| 242 | | * AssignmentNodeIF: x=expr, x++, x--, ++x, --x |
| 243 | | * FunctionInvocationNodeIF: invocation f(x) when f is concrete |
| 244 | | |
| 245 | | |
| | 71 | The design is being implemented in the ast package in the source code. |
