The CIVL-IR.  Also known as "CIVL model".

Grammar?

Example:

{{{
int f() {
L1 :
  $choose {
    $when (g1) stmt1; goto L2;
    $when (g2) stmt2; goto L3;
  }
L2 :
  $choose {
    $when (g3) stmt3; goto L4;
    ...
  }
...
}
// etc.
}}}

==  Static Types ==

* `$bool` : boolean type, values are `$true` and `$false`
* `$proc`
* `$scope`
* `$char`
* `$mem`
* `$bundle`
* `$heap`
* `$range`
* `$domain`
 * `$domain(Integer n)`
* `enum` types
* Integer types
 * `$integer` : the mathematical integers
 * `$int(lo,hi,wrap)`
  * lo, hi are integers, wrap is a Boolean
  * finite interval of integers [lo,hi].  If `wrap` is true then all operations "wrap", otherwise, any operation resulting in a value outside of the interval results in an exception being thrown.
* Real types
 * `$real` : the mathematical real numbers
 * `$float(e,f)`
 * e, f are integers
 * IEEE754 floating point numbers
* `struct` types
 * list of name-type pairs
 * bit-widths?
* `union` types : similar to struct
* `T[]` : array-of-T
 * `T[n]` : array-of-length-n-of-T, subtype of above
* `Function<S1,...,Sn;T>`
* `T*` : pointer-to-T

When are two types equal?

What are two types compatible?

== Values ==



== Expressions ==

* `e1+e2` : addition
* `e1-e2` : subtraction
* `e1*e2` : multiplication
* `e1/e2` : division
* `e1%e2` : modulus
* `e1[e2]` : array index
* `*e` : pointer dereference
* `&e` : address-of
* `(T)e` : cast expression
 * cast of integer to array-of-boolean, and vice-versa?
* 


== Statements ==

* Assign
* Call
* Spawn
* Wait



== Program Graph ==

== Model ==


== Libraries ==