SMTChecker

Setup

Compiler Setup

  1. solc-select installation - the link includes a number of ways to download and install, but the easiest is probably pip3 install solc-select
  2. Run solc --version
    1. If you see Version: 0.8.0 you can skip the next step
  3. solc-select install 0.8.0 && solc-select use 0.8.0
    1. Run solc --version you should see Version: 0.8.0

Download files

  1. Download this file

tutorial1.sol

  1. run solc tutorial1.sol
    1. You should seeā€¦ Compiler run successful, no output requested.

Instructions

  1. Uncomment line 3 in tutorial1.sol
  2. run solc tutorial.sol
    1. The model checker should return a Warning that the Overflow property could not be verified. It also includes a counterexample and the line number where it found the overflow.
  3. Add one or more require statements to prevent the code from overflowing.
    1. Hint: type(uint).max returns the max value for a uint