== CIVL IR == Language principles: * CIVL-IR is a subset of CIVL-C. A CIVL-IR program is a CIVL-C program, and has the same semantics. Types: * `$int` : mathematical integers * `$real` : mathematical reals * `$float` : IEEE floating-point numbers with e,f integer constants * `$herbrand` : Herbrand type of non-Herbrand numeric type T * `_Bool` * `$proc` * `char` * `$bundle` * `$heap` * `$range` * `$domain` * `enum tag` * `struct tag` * `union tag` * `T[]` : array of T * `void *` : pointer to anything * `T *` : pointer to T * `T(T1, T2, ...)` : function consuming T1, ... and returning T * `$mem` : set of memory locations * `$set` : set of T * `$map` : maps from T1 to T2 * `$rel` : relation, set of n-tuples