Overflow and correctness

Eiffel is a programming language that strives for correctness.
In C instead most of the times speed is regarded as more important than correctness (paraphrasing a comment of Eric Sosman ).
Most Eiffel compilers use C as an intermediate language (Liberty/SmartEiffel, ISE), so a programming language striving for correctness relies on one that trade correctness for speed.
I've been thinkering about
I think we cannot blame C as this is a issue that has no "solution"; let's see a little panoramic of the efforts poured into something "as simple" as correctness in integer calculations:

• Best way to detect integer overflow in C (from Stackoverflow.com)
• CERT's "as-if" infinitely ranged (AIR) integer model and "Ensure that operations on signed integers do not result in overflow"
• Integer security 
• Catching Integer Overflows in C

Sadly there is no magic wand for this issue.
An answer may be saturation arithmetic; digging my fading knowledge of assembler, mainly from my days on 6502 I was wondering why no one seems to use the overflow flag present in almost all CPU: it seems there is no portable way to do it access it. Oh it would be so nice to write in INTEGER_GENERAL 

«infix "+" (another: like Current): like Current is external "built_in" ensure has_overflowed=False end»

I naively thought that an arithmetic overflow would have triggered a SIGFPE signal in POSIX systems. It seems I'm wrong:

class OVERFLOW
    -- Test integer overflow
insert PLATFORM
creation make
feature make is
        local i,j: INTEGER
        do
            i := Maximum_integer
            j := i+1 -- SIGFPE expected
            ("i:=#(1), j=i+1=#(2)%N"# (&i) # (&j) ).print_on(std_output)
        end
    end

When compiled with "compile  overflow.e" Liberty Eiffel correctly says:

*** Error at Run Time ***: Require Assertion Violated.
*** Error at Run Time ***: no_overflow
3 frames in current stack.
=====  Bottom of run-time stack  =====
<system root>
Current = OVERFLOW#0x925b038
line 5 column 9 file /media/Liberty/tybor-liberty/work/tybor-sandbox/overflow.e
======================================
make OVERFLOW
Current = OVERFLOW#0x925b038
i = 2147483647
j = 0
line 9 column 4 file /media/Liberty/tybor-liberty/work/tybor-sandbox/overflow.e
======================================
infix + (infix + INTEGER_32)
Current = 2147483647
other = 1
Result = 0
line 21 column 80 file /home/paolo/current-liberty/src/lib/numeric/integral.e
=====   Top of run-time stack    =====
*** Error at Run Time ***: Require Assertion Violated.
*** Error at Run Time ***: no_overflow

but when we compile it with "compile --boost overflow.e" it happily says: "i:=2147483647, j=i+1=-2147483648" which is obviously wrong. You have to compile it with "compile --boost overflow.e --cc gcc -ftrapv" to laconically receive the answer

"Received signal 6.
Eiffel program crash at run time.
No trace when using option "-boost"

Which is not what I would expect, since signal 6 is ABRT on my system.