Prune Away Trivially-Proven Assertions

[shaobo-he]

For memory safety checking and integer overflow checking, we instrument the relevant instructions with checks uniformly whereas a lot of them can be trivially proven. For example, dereferencing a stack variable can be obviously correct.

For memory safety checking, we can adopt SeaHorn's approach where a simple analysis at the LLVM IR level is used to remove trivially proven checks.

For integer overflow checking, we can use an interval analysis (i.e., those provided by crab to do similar things.