Add feature that allows functions to require type variables are constant

can now write e.g.

forall (constant 'n : Int) rather than forall ('n: Int)

which requires 'n to be a constant integer value whenever the function
is called. I added this to the 'addrsize variable on memory
reads/writes to absolutely guarantee in the SMT generation that we
don't have to worry about the address being a variable length
bitvector.

0 files changed, 0 insertions, 0 deletions