Bug: Default config missing an error after overflowing shift

[Novak756]

Basic Info

• Version: Ultimate 0.2.4-dev-563c1d8 (563c1d8)
• Input file:

  extern void __VERIFIER_error(void);
  extern void reach_error(void){__VERIFIER_error();}
  int main() {
  int width = 4;
  18446744073709551615ULL << width;
  reach_error();
  }

• Settings: UAutomizer-linux/config/svcomp-Reach-64bit-Automizer_Default.epf
• Toolchain: UAutomizer-linux/config/AutomizerReach.xml
• logs.zip

Description

Hi again, running the default config (for any of Automizer, Taipan, Kojak, GemCutter) on the above file gives Ultimate proved your program to be correct!. Again the bitvector config is able to find the error. Clearly the assertion should be reachable, and while this program includes overflow, it should be well-defined (as it is unsigned). If this is expected, feel free to close this issue.

[schuessf]

Thank you for your report! There was indeed a bug that I just fixed. We added an assumption that the result of a left shift is always greater than the first operand, if the second operand is not zero. This is a reasonable assumption for signed types, since we assume that there are no overflows. However, for unsigned types this assumption was wrong (as there can be a legal wraparound), therefore I removed this assumption in that case.