Open
Description
This issue is to remind us to develop a new option in ESBMC (e.g., --undef-behaviour-check) to check for undefined behaviour. In particular, this check would add an assert(const >= 0) or assert(const <= type-bit-width) statement for shift operations. It should be something similar to the --overflow-check (available in the goto_check.cpp file).