From mboxrd@z Thu Jan  1 00:00:00 1970
X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on polar.synack.me
X-Spam-Level: 
X-Spam-Status: No, score=-1.9 required=5.0 tests=BAYES_00,FREEMAIL_FROM
	autolearn=ham autolearn_force=no version=3.4.4
X-Google-Thread: a07f3367d7,78ff7923606282ea
X-Google-Attributes: gida07f3367d7,public,usenet
X-Google-NewGroupId: yes
X-Google-Language: ENGLISH,UTF8
X-Received: by 10.180.24.132 with SMTP id u4mr7127479wif.6.1366280886204;
        Thu, 18 Apr 2013 03:28:06 -0700 (PDT)
X-Received: by 10.49.104.144 with SMTP id ge16mr1042638qeb.19.1366280886050;
 Thu, 18 Apr 2013 03:28:06 -0700 (PDT)
Path: 
 hg5ni16271wib.1!nntp.google.com!gp5no377816qab.0!postnews.google.com!glegroupsg2000goo.googlegroups.com!not-for-mail
Newsgroups: comp.lang.ada
Date: Thu, 18 Apr 2013 03:28:05 -0700 (PDT)
In-Reply-To: <MPG.2bd9c09a49da8ab39896a4@news.zen.co.uk>
Complaints-To: groups-abuse@google.com
Injection-Info: glegroupsg2000goo.googlegroups.com;
 posting-host=195.182.34.201;
 posting-account=bMuEOQoAAACUUr_ghL3RBIi5neBZ5w_S
NNTP-Posting-Host: 195.182.34.201
References: <0dbac307-0c0c-4883-8644-d1ffc25419f8@googlegroups.com>
 <MPG.2bd9c09a49da8ab39896a4@news.zen.co.uk>
User-Agent: G2/1.0
MIME-Version: 1.0
Message-ID: <e7e5cead-7196-477a-ae8a-350c2efc5a91@googlegroups.com>
Subject: Re: SPARK - division by zero problem
From: Maciej Sobczak <see.my.homepage@gmail.com>
Cc: phil.jpthornley@gmail.com
Injection-Date: Thu, 18 Apr 2013 10:28:06 +0000
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: quoted-printable
Date: 2013-04-18T03:28:05-07:00
List-Id: <comp.lang.ada>

W dniu czwartek, 18 kwietnia 2013 10:35:48 UTC+2 u=C5=BCytkownik Phil Thorn=
ley napisa=C5=82:


> The undischarged VC I get is:
> procedure_divide_1.
> H1:    y <> 0 .
> H2:    x >=3D - 2147483648 .
> H3:    x <=3D 2147483647 .
> H4:    y >=3D - 2147483648 .
> H5:    y <=3D 2147483647 .
> H6:    integer__size >=3D 0 .
>        ->
> C1:    x div y <=3D 2147483647 .
>=20
> which is false for x =3D -2147483648, y =3D -1

Right, I fell into the trap by focusing on Y /=3D 0 condition. Indeed, the =
assymetry of Integer'Range is causing troubles in this case.
Thank you for response.

--=20
Maciej Sobczak * http://www.msobczak.com * http://www.inspirel.com