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.

infix "#": Eiffel's printf

It's really nice to be able to write in Liberty/SmartEiffel:

("i:=#(1), j=i+1=#(2)%N"# (&i) # (&j) ).print_on(std_output)
("obviously foo := #(2), bar := #(1)%N" # &42 # &17).print_on(std_output)

which may look cryptic to most Eiffel programmers, but may look familiar when translated into C:

printf("i:=%d, j=i+1=%d\n", i,j)
printf("obviously foo := %d, bar := %d\n", 17,42)

Beside looking a little more convoluted it actually has quite a few advantages:

• like QString::arg of Qt fame it allows positional arguments,
• it does not rely on variable argument function calls,
• it does not allocate an unnecessary array to hold the arguments; each call to # actually return a ROPE which does is an ABSTRACT_STRING holding references to two substrings; the prefix "&" operator returns a LAZY_STRING (praises to Adrian for good idea) which will not be converted to a string until it gets iterated over, usually printing or copying it.
• it allows to write things like:
  

  local s,t,u: STRING
  do
  

  s := "Eiffel"; t:= "beautiful"
  u := s | " is a " |t| " language"
  assert (u.is_equal("Eiffel is a beautiful language")
  t.prepend("really ")
  assert (u.is_equal("Eiffel is a really beautiful language")
  -- which may also obtained with
  u := "#(1) is a #(2) language" # s # t

  end

• it does retain type-safety (AFAIK)