[CN] underflow/overflow error messages

[jwshii]

(Ported from the CN heuristic evaluation results.) One participant said:

Underflow/overflow exceptions both become the overly general “an exceptional condition occurs during the evaluation of an expression”, while I believe the state trace contains enough information to be more specific.

For example, the code here

int add(int x, int y)
/*@ requires let sum = (i64) x + (i64) y;
             -2147483648i64 <= sum;
             sum <= 2147483647i64;
    ensures return == (i32) sum;
@*/
{
  return x+y;
}

produces the same error

example.c:7:10: error: Undefined behaviour
  return x+y;
         ~^~ 
an exceptional condition occurs during the evaluation of an expression (§6.5#5)

if either the <= sum or the sum <= constraints are removed.

Would a more explicit error message here indicating the possibility of underflow / overflow be possible?

[septract]

Just poking around in the CN checking code, it looks like this particular flavor of UB only ever happens when the value is not representable at an integer type (see here).

This error message does not say this specifically - I think it is defined here. A simple solution would be to make this message more descriptive, eg:

"This expression may compute an integer value that cannot be represented at the current type - typically, this means the value may underflow or overflow"

To distinguish over / underflow, I suppose we'd need to modify is_representable_integer (defined here). It looks like the current version doesn't discriminate between under and overflow, but maybe these could be proved separately?

Btw, it might be good to have each distinct UB print an error code, since such codes already exist internally here. Then we could have some kind of per-error lookup table to help users triage messges.

[jwshii]

(I think generally having some "typically, this means" in error messages would be extremely helpful!)