all integers are treated as usize (unsigned word size) integers in Viper
overflows are checked with assertions after unrolling of arithmetic expressions into Three-Access Code.
fixed access permissions and bounds for returned values
fixed all the tests s.t. they work with bounded arithmetic
all integers are treated as
usize(unsigned word size) integers in Viper overflows are checked with assertions after unrolling of arithmetic expressions into Three-Access Code.