add bound checking in pargs

[alxest]

No description provided.

[dongjaelee1]

This is regarding the overflow of int(also perhaps ptroffs) type.
Currently, Imp only imposes intrange_64 condition on int for only certain cases (comparison, system call arguments).
For memory offset, load/store(by Imp), alloc(by Mem).
For CompCert compilation, overflow is handled by performing modular arithmetics. Therefore, there are some valid programs in Imp, but executes UB if intrange_64 is checked upon pargs(as @alxest mentioned).

f (x: int) { return x + 1; }
main () {a = f(INTMAX + 1); print(a); }

What we want is to erase all the overflow checks (extra assume (intrange_64))s) from 0-level specs(MutF0.v).
Some possible solutions:

• Have two types: Tint: checks overflow, Tz: does not.
• Include intrange_64 condition in Tint type, following CompCert.
  The second one needs more work, including fixing the compiler.