Analysis Design Choices

This page was created to document some of the various design choices made by Manticore:

Ethereum

• CALLDATALOAD with a symbolic offset: offset is constrained to be within sizeof the data + 32. +32 is arbitrary. an offset outside the range of the data is valid, and just returns zeros, so this constrain will account for some out of bounds read, but not too much.