| 128 | | * body: StatementNodeIF |
| 129 | | * invariants: Collection<ExpressionNodeIF> ? |
| 130 | | * ForLoopNodeIF |
| 131 | | * methods |
| 132 | | * initializer: StatementNodeIF |
| 133 | | * condition: ExpressionNodeIF |
| 134 | | * incrementer: StatementNodeIF |
| 135 | | * body: StatementNodeIF |
| 136 | | * DoUntilNodeIF |
| 137 | | * BreakNodeIF |
| 138 | | * ContinueNodeIF |
| 139 | | * GotoNodeIF |
| 140 | | * label (this is the kind before processing) |
| 141 | | * statement (after processing) |
| 142 | | * ReturnNodeIF |
| 143 | | * expression (may be null) |
| 144 | | * NoopNodeIF |
| 145 | | * BlockNodeIF: ({...} in C) |
| 146 | | * sequence of variable definitions |
| 147 | | * sequence of statements |
| 148 | | * ExpressionNodeIF: expressions--these are considered a kind of statement (as in C) |
| 149 | | * PureExpressionNodeIF: side-effect-free expressions |
| 150 | | * LiteralNodeIF (including named literals): integers, reals, strings, chars |
| 151 | | * VariableExpressionNodeIF |
| 152 | | * OperatorNodeIF |
| 153 | | * +,-,*,/,%,<,<=,>,>=,==,!=,!,&&, | |, (x?y:z), bitand, bitor, bitxor, lshift, rshift, & (address-of), * (dereference) |
| 154 | | * CastNodeIF |
| 155 | | * newType: TypeNodeIF (type you are casting to) |
| 156 | | * expression: ExpressionNodeIF |
| 157 | | * ArrayIndexNodeIF (a[i]) |
| 158 | | * RecordNavigationNodeIF: (x.a) |
| 159 | | * QuantifierNodeIF |
| 160 | | * quantifier: {FORALL, EXISTS, LAMBDA, UNIFORM, SUM} |
| 161 | | * boundVariable: VariableDefinitionNodeIF |
| 162 | | * constraint: ExpressionNodeIF |
| 163 | | * expression: ExpressionNodeIF |
| 164 | | * InitializerNodeIF: special kind of expression used to initialize variables in their decl |
| 165 | | * SizeOfNodeIF: type, expression, or string literal |
| 166 | | * StartOfNodeIF: &a[0] -- that is the Cil way of converting an array to pointer to first element |
| 167 | | * FunctionApplicationNodeIF: invocation f(x) when f is abstract (pure) function |
| 168 | | * SideEffectExpressionNodeIF: expressions with side-effects |
| 169 | | * AssignmentNodeIF: x=expr, x++, x--, ++x, --x |
| 170 | | * FunctionInvocationNodeIF: invocation f(x) when f is concrete |
| | 123 | * trueBranch: StatementNodeIF |
| | 124 | * falseBranch: StatementNodeIF (may be null) |
| | 125 | * WhileLoopNodeIF: loop. associated invariant (derived from TASS invariant pragma) |
| | 126 | * methods |
| | 127 | * condition: ExpressionNodeIF |
| | 128 | * body: StatementNodeIF |
| | 129 | * invariants: Collection<ExpressionNodeIF> ? |
| | 130 | * ForLoopNodeIF |
| | 131 | * methods |
| | 132 | * initializer: StatementNodeIF |
| | 133 | * condition: ExpressionNodeIF |
| | 134 | * incrementer: StatementNodeIF |
| | 135 | * body: StatementNodeIF |
| | 136 | * DoUntilNodeIF |
| | 137 | * BreakNodeIF |
| | 138 | * ContinueNodeIF |
| | 139 | * GotoNodeIF |
| | 140 | * label (this is the kind before processing) |
| | 141 | * statement (after processing) |
| | 142 | * ReturnNodeIF |
| | 143 | * expression (may be null) |
| | 144 | * NoopNodeIF |
| | 145 | * BlockNodeIF: ({...} in C) |
| | 146 | * sequence of variable definitions |
| | 147 | * sequence of statements |
| | 148 | * ExpressionNodeIF: expressions--these are considered a kind of statement (as in C) |
| | 149 | * PureExpressionNodeIF: side-effect-free expressions |
| | 150 | * LiteralNodeIF (including named literals): integers, reals, strings, chars |
| | 151 | * VariableExpressionNodeIF |
| | 152 | * OperatorNodeIF |
| | 153 | * +,-,*,/,%,<,<=,>,>=,==,!=,!,&&, | |, (x?y:z), bitand, bitor, bitxor, lshift, rshift, & (address-of), * (dereference) |
| | 154 | * CastNodeIF |
| | 155 | * newType: TypeNodeIF (type you are casting to) |
| | 156 | * expression: ExpressionNodeIF |
| | 157 | * ArrayIndexNodeIF (a[i]) |
| | 158 | * RecordNavigationNodeIF: (x.a) |
| | 159 | * QuantifierNodeIF |
| | 160 | * quantifier: {FORALL, EXISTS, LAMBDA, UNIFORM, SUM} |
| | 161 | * boundVariable: VariableDefinitionNodeIF |
| | 162 | * constraint: ExpressionNodeIF |
| | 163 | * expression: ExpressionNodeIF |
| | 164 | * InitializerNodeIF: special kind of expression used to initialize variables in their decl |
| | 165 | * SizeOfNodeIF: type, expression, or string literal |
| | 166 | * StartOfNodeIF: &a[0] -- that is the Cil way of converting an array to pointer to first element |
| | 167 | * FunctionApplicationNodeIF: invocation f(x) when f is abstract (pure) function |
| | 168 | * SideEffectExpressionNodeIF: expressions with side-effects |
| | 169 | * AssignmentNodeIF: x=expr, x++, x--, ++x, --x |
| | 170 | * FunctionInvocationNodeIF: invocation f(x) when f is concrete |
