Fix UINT and INT Hack

To get uint and int to work in SMV, values must be restricted. This is currently done with the line:

next(b) := case
    state = c1f1_ln2 : max(0, (b - 1) mod 200);
    state = c1f2_ln1 : max(0, (b + a) mod 200);
    TRUE : b;
esac;

There is a hack we can do to allow for larger int and uint spaces in our program:

Suggested Solution

/*!UINT_MAX: 400;*/
/*!UINT_MIN: 0;*/
/*!INT_MAX: 200;*/
/*!INT_MIN: -200;*/

Allow these lines to exists at the top of the solidity file.

TODO

• Update the parser (ANTLR) file to support reading these lines
• Update the parser to read the values in and store them into the DApp
• Use values in DApp to set the max and min for the UINT and INT data types