From: Phil Thornley <phil.jpthornley@gmail.com>
Subject: Re: Constraint_Error from arithmetic operations
Date: Thu, 27 Dec 2012 10:33:00 -0000
Date: 2012-12-27T10:33:00+00:00 [thread overview]
Message-ID: <MPG.2b46340f43edd90398969f@news.zen.co.uk> (raw)
In-Reply-To: 87r4mbrgl8.fsf@mid.deneb.enyo.de
In article <87r4mbrgl8.fsf@mid.deneb.enyo.de>, fw@deneb.enyo.de says...
>
> This is somewhat related to the recent discussion on exception
> contracts, but I'm more interested in what can be right now (with
> current tools).
>
> I recently browsed through Barnes' 2006 SPARK book and noticed that
> SPARK has a rather drastic approach to arithmetic operations which
> overflow and fail to deliver the mathematically correct result
> (program termination). The SPARK tools do not seem to be able to
> statically show that arithmetic operators do not overflow, which is
> obviously difficult in the general case, but should be doable with
> help from the programmer.
>
(The publication dates of the three SPARK books are 1997, 2003, and 2012
so I'm not sure which one you mean).
I don't know how you read the any of books to get that understanding,
but SPARK has always included the option to generate overflow checks
(and they are now always included whenever VCs are generated).
With this code:
======================================
package P
is
type My_Int is new Short_Integer range -20_000 .. 20_000;
-- Short_Integer is -32768 .. 32767.
function Op (A, B : My_Int) return My_Int;
end P;
package body P
is
function Op (A, B : My_Int) return My_Int
is
begin
return (A + B) / 2;
end Op;
end P;
======================================
There is an unprovable VC remaining after simplification:
function_op_1.
H1: a >= - 20000 .
H2: a <= 20000 .
H3: b >= - 20000 .
H4: b <= 20000 .
H5: my_int__size >= 0 .
->
C1: a + b >= - 32768 .
C2: a + b <= 32767 .
which comes from the overflow check on the plus operation in the return
expression.
(You have to specify the ranges for Short_Integer of course - this is in
the configuration file for the particular compiler you are using).
Originally the base range had to be specified using a 'base type
assertion' but the recent versions of the language have included the use
of derived types, as above.
Cheers,
Phil
next prev parent reply other threads:[~2012-12-27 10:33 UTC|newest]
Thread overview: 5+ messages / expand[flat|nested] mbox.gz Atom feed top
2012-12-27 9:26 Constraint_Error from arithmetic operations Florian Weimer
2012-12-27 10:33 ` Phil Thornley [this message]
2012-12-27 11:11 ` Brian Drummond
2012-12-27 13:19 ` Florian Weimer
2012-12-27 15:38 ` Phil Thornley
replies disabled
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox