let's say we have a complex arithmetic expression. is there a simple
clean way to assert that no intermediate results (subexpressions)
contain an overflow?
e.g., if we have
unsigned a,b,c,d;
a+b+c+d
i'd like to assert that a+b+c+d does not overflow. however i'm worried
that the way klee works subexpressions can overflow, but the entire
expression won't. for example, if a+b overflows, KLEE could perform
the addition, truncate the result to 32 bits, then do the rest of the
additions with the result that the entire expression does not overflow,
but the subexpression does.
i believe we had this problem w/ FT when doing underconstrained, but
don't know if it also shows up in KLEE.
