Not all Ada compilers will behave like this. You must be using a version of the GNAT GPL compiler prior to 2015, or FSF GCC prior to 5; at that point, GNAT didn’t check for integer overflow by default - you had to compile with
This was stated to be in the pursuit of efficiency, but many users thought that the gain in efficiency wasn’t worth the cost of explaining this behaviour to new (and, sometimes, not-so-new) users. And, of course, using compiler-provided types such as
Integer isn’t best practice.
Nowadays, your program compiles OK without
-gnato (admittedly without warnings, even with
-gnatwa) but runs with
raised CONSTRAINT_ERROR : overflow.adb:7 overflow check failed
SPARK Ada would detect this problem:
$ /opt/gnat-gpl-2016/bin/gnatprove -P overflow.gpr
Phase 1 of 2: generation of Global contracts ...
Phase 2 of 2: flow analysis and proof ...
overflow.adb:4:14: warning: subprogram "p" has no effect
overflow.adb:7:15: medium: overflow check might fail, in call inlined at overflow.adb:11 (e.g. when x = 2147483647)
overflow.adb:8:07: warning: no Global contract available for "Put_Line"
overflow.adb:8:07: warning: assuming "Put_Line" has no effect on global items
Summary logged in /Users/simon/tmp/so/gnatprove/gnatprove.out