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