Responsible for compiling the declarations, statements and expression found in a WhileyFile into WyIL declarations and bytecode blocks. For example:
type nat is (int x) where x >= 0 function f(nat x) => int: return x-1
The code generator is responsible for generating the code for the constraint on nat, as well as compiling the function's statements into their corresponding WyIL bytecodes. For example, the code generated constraint on type nat would look like this:
type nat is int where: load x const 0 ifge goto exit fail("type constraint not satisfied") .exit: This WyIL bytecode simply compares the local variable x against 0. Here, x represents the value held in a variable of type nat. If the constraint fails, then the given message is printed.
@author David J. Pearce
| |