Use Manticore to find if an overflow is possible in Overflow.add. Propose a fix of the contract, and test your fix using your Manticore script.
Follow the pattern initialization, exploration and property for the script.
- Create one user account
- Create the contract account
- Call two times
addwith two symbolic values
- Check if it is possible for the value returned by sellerBalance() to be lower than the first input.
- The value returned by the last transaction can be accessed through:
- The data returned needs to be deserialized:
data = ABI.deserialize("uint256", data)
- You can use the template proposed in template.py