wrap speculative mode around bounds computation

[DrMichaelPetter]

during inspection of SV-comp results, we encountered some unnecessary overflow flagging, e.g.

//SKIP PARAM:  --enable ana.int.interval  --set sem.int.signed_overflow assume_none  --set ana.activated[+] lin2vareq
int s = 1;
void f(){
  unsigned int n,i;
  n = i%(s+2);  // unnecessary overflow flagging
}

due to bounds computations not being wrapped in speculative mode.

This is also relevant for affeq and other apron related analyses.

[sim642]

Where exactly is the overflowing operation performed there? There's already a executing_speculative_computations wrapper a dozen lines above.

[DrMichaelPetter]

Where exactly is the overflowing operation performed there? There's already a executing_speculative_computations wrapper a dozen lines above.

There is a query to the value domain, that retrieves a range to bound the expression to cast in the non-injective case. This fragment might cause an overflow flag, if not done speculatively. I have now scoped the speculation a little bit more narrow now.