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:

• _Bool : boolean type
• char : character
• $int : mathematical integers
• $real : mathematical reals
• $float<e,f> : IEEE floating-point numbers e=significand bits, f=exponent bits
• $herbrand<T> : Herbrand type of non-Herbrand numeric type T
• $proc : process type
• $bundle: bundle type for sequence of any type (same as seq<T>?)
• $heap : heap type, for dynamic allocation
• $range : regular sequence of integers
• $domain : tuple of ranges
• $mem : set of memory locations
• enum tag : enumerated type
• struct tag : structured type
• union tag : union type
• T[] : array of T
• void * : pointer to anything
• T * : pointer to T
• T(T1, ..., Tn) : function consuming T1, ..., Tn and returning T
• $seq<T> : sequence of T
• $set<T> : set of T
• $map<T1,T2> : map from T1 to T2
• $rel<T1, ..., Tn> : relation, set of n-tuples