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<e,f> : IEEE floating-point numbers with e,f integer constants
• $herbrand<T> : 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<T> : set of T
• $map<T1,T2> : maps from T1 to T2
• $rel<T1, ..., Tn> : relation, set of n-tuples