| 142 | | * variable definition |
| 143 | | * with possible initialization expression |
| 144 | | * possible array extents information and other information modifying type? |
| 145 | | * storage class: automatic, static, extern, ...? |
| 146 | | * expressions: these are considered a kind of statement (as in C) |
| 147 | | * pure expressions (side-effect-free) |
| 148 | | * literals (including named literals): integers, reals, strings, chars |
| 149 | | * variable |
| 150 | | * operators |
| | 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 |
| 151 | 153 | * +,-,*,/,%,<,<=,>,>=,==,!=,!,&&, | |, (x?y:z), bitand, bitor, bitxor, lshift, rshift, & (address-of), * (dereference) |
| 152 | | * cast-to-t |
| 153 | | * a[i] (array index) |
| 154 | | * x.a (record navigation) |
| 155 | | * quantifiers: \forall, \exists, \uniform, \sum |
| 156 | | * initializers (special kind of expression used to initialize variables in their decl) |
| 157 | | * sizeof (type, expression, or string literal) |
| 158 | | * startOf(a): &a[0] -- that is the Cil way of converting an array to pointer to first element |
| 159 | | * function invocation f(x) when f is abstract (pure) function |
| 160 | | * expressions with side-effects |
| 161 | | * assignments: x=expr, x++, x--, ++x, --x |
| 162 | | * function invocation f(x) when f is concrete |
| | 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 |
