9

Silent failure for such trivial code. How can they claim high integrity?

with ada.text_io;
use  ada.text_io;
procedure overflow is
    procedure p (i: positive) is
        x: integer := integer'last;
    begin
        x := (x+i)/2;
        put_line (integer'image(x) & " should be positive");
    end;
begin
    p(10);
end;

Not even a compiler warning like "cannot ensure the lack of overflow" or smth.

This seems at least as error-prone as some of the C++ pitfalls the Ada folks like to point out. Correct me if I am wrong. I would like to have a better language than C++, but I keep facing language complexity that is supposed to protect from all pitfalls, and still.

5
  • ... or should I ask this on stackoverflow instead ?
    – cufizut
    Jul 13, 2016 at 18:54
  • This is exactly what Ada ranges are for. Jul 13, 2016 at 19:05
  • That's odd. According to the Integer overflow wiki page, Ada should through a NUMERIC_ERROR at x+1.
    – David Arno
    Jul 13, 2016 at 19:45
  • @DavidArno, it’s been Constraint_Error since Ada 95 (Numeric_Error became an obsolescent renaming of Constraint_Error). Jul 13, 2016 at 19:50
  • You are obviously not using a standards compliant Ada compiler. Jul 14, 2016 at 5:59

2 Answers 2

11

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 -gnato.

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

$ ./overflow 

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
3
  • 4
    Versions of GNAT that disable numeric overflow checking by default are not conforming Ada compilers in that default mode. The language itself requires Constraint_Error to be raised. Jul 13, 2016 at 20:10
  • Nice that I get at least a runtime error, but why no protection at compile-time? Can SPARK do that?
    – cufizut
    Jul 14, 2016 at 5:34
  • @cufizut I think surely it's because in some case it's easy to know in compile time, like if I see 4 - 5 I know it's a error because I don't want negative numbers, but if I see a - b and for example b get the value from some input I can't know the result in compile time, I'll need to check in runtime.
    – user191414
    Jun 27, 2018 at 10:13
3

If a compiler behaves like this, it isn't an Ada compiler.

My guess is that you use GCC (GNAT), which for some odd reason requires that you pass it a very specific combination of command line arguments, to behave like an Ada compiler:

  • -fstack-check -- Stack overflow
  • -gnato -- Arithmetic overflow
  • -gnat2012 -- Use Ada 2012 (instead of older versions of the language)

And if you want contracts to behave sensibly:

  • -gnata -- Contracts and assertions
2
  • 1
    As pointed out by @SimonWright's earlier answer, you no longer need -gnato when using recent versions of GNAT.
    – Jules
    Jul 14, 2016 at 9:04
  • 1
    Yes. But not everyone are using "recent" versions of GNAT. Debian/stable, which I'm using quite often, is a known example. Jul 14, 2016 at 14:55

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

Not the answer you're looking for? Browse other questions tagged or ask your own question.