= Multiple Changes to CIVL Code =

== Model Changes ==

* make sure the parameter type of a function call is never an array type.   ABC should already be doing this.
* add a method to expressions like `SymbolicExpression getConstantValue()` and a corresponding setter, to cache the value of any expression that has a constant value, such as a literal expression
* add a new `CIVLType`: `CIVLDynamicType.`
 * A CIVL Expression of that type, when evaluated, will yield a `SymbolicExpression` `x`.  A method in the `Evaluator`, `SymbolicType getSymbolicType(SymbolicExpression x);`, will take such an `x` and return a `SymbolicType` and that is basically the only operation that can be performed on `x`.  Hence this gives you a way to take a (dynamic, symbolic) type and wrap it up into a value that can be stored in a variable in your model.
* add a new kind of CIVL `Expression`: `DynamicTypeOf(t)`, where `t` is a (static) CIVL type.
 * The type of this expression is `CIVLDynamicType`.  When evaluated, it returns the dynamic type determined by the current state and the given static type.  (This assumes extent expressions are stored in array types.)  For example, if `t` is the static type `struct foo { double a[n]; }` from the source code above, then `DynamicTypeOf(t)`, evaluated in the state that arises at that point in the source code, will yield the symbolic type which is a record type with one field which is an array of doubles of length 2.  Now you can store that dynamic type in a variable if you want to save it, e.g., insert a statement like this into the model:
  * `CIVLDynamicType __struct_foo__ = DynamicTypeOf(struct foo { double a[n]; });`
* add a new kind of CIVL expression: `InitialValue[variable, dynamicType]`. Here, `variable` is a (static) `Variable`, and `dynamicType` is an expression of type `CIVLDynamicType`.   The type of this expression is the type of the variable.  When evaluated, it returns a default initial value for a variable with the given dynamic type.  This can be used to initialize arrays and structs.
* add a new `CIVLType`: `CIVLScopeType`
* add new subtype of `Variable`: `CIVLScopeVariable` with method
 * `Scope getScope();`
* add to the CIVL pointer type a method to get the scope variable, implement appropriate constructors and modifications to the factory, etc.

== Semantics Changes ==

* use interfaces for `Executor`, `Evaluator`, etc.
* finish javadocs for all methods
* don't use `Vector`.  Use `LinkedList` if you only need to iterate; use `ArrayList` if you need constant time access
* use `switch` instead of big `if...else if…` sequence (mostly DONE)
* implement pointer subtraction
* construct and set the heap type in the constructor for `Evaluator`, just like the other special types

== Translation ==

Thoughts on processing struct definitions:

* transform the AST to factor out all struct definitions embedded in declarations.  This is really part of "side-effect-removal".
* translate a struct definition `struct foo { … } ` as follows.
 * Let `t` be the `CIVLType` resulting from translating the ABC type.
 * Create a new `Variable` of type `CIVLDynamicType` and add it to the current scope. Call the variable `__struct_foo__`.
 * Create as assignment statement at the current location: `__struct_foo__ = DynamicTypeOf(t)`
* any variable declaration with a compound type (struct, union, array) should be translated as follows:
 * add the variable `v` to the current scope with the translated type `t` as usual
 * add an assignment statement at the current location: `v=InitialValue[v, CIVLDynamicType(t)]`
* Evaluation of `CIVLDynamicType(t)` in a state `s` is defined as follows:
 * if `t` is a struct type, say with tag `foo`, then the result is the result of evaluating the variable (in s) `__struct_foo__`
 * if `t` is an array type with element type `E` and length expression `l`, the result is obtained by evaluating `CIVLDynamicType(E)`, call the result `de`; evaluating `l`, call the result `dl`; and return `completeArrayType(de,dl)` (eliding the wrapping and unwrapping of the symbolic type into a symbolic expression value)
* Evaluation of `InitialValue[v,d]` is as follows:
 * for a primitive dynamic type, some undefined value (null expression)?
 * if `d` is a tuple, create the concrete tuple of type `d` with each component obtained by evaluating `InitialValue[component, componentType]`
  * XXX problem: maybe take address argument instead of variable, or LHS expression???. Or just `Initialize(LHSExpression, DynamicType)` statement.
 * if `d` is an array type, create a unique symbolic constant name based on the LHS expression and a symbolic constant with that name and type `d` (no recursion in this case)