From: Maciej Sobczak <see.my.homepage@gmail.com>
Cc: phil.jpthornley@gmail.com
Subject: Re: SPARK - division by zero problem
Date: Thu, 18 Apr 2013 03:28:05 -0700 (PDT)
Date: 2013-04-18T03:28:05-07:00 [thread overview]
Message-ID: <e7e5cead-7196-477a-ae8a-350c2efc5a91@googlegroups.com> (raw)
In-Reply-To: <MPG.2bd9c09a49da8ab39896a4@news.zen.co.uk>
W dniu czwartek, 18 kwietnia 2013 10:35:48 UTC+2 użytkownik Phil Thornley napisał:
> The undischarged VC I get is:
> procedure_divide_1.
> H1: y <> 0 .
> H2: x >= - 2147483648 .
> H3: x <= 2147483647 .
> H4: y >= - 2147483648 .
> H5: y <= 2147483647 .
> H6: integer__size >= 0 .
> ->
> C1: x div y <= 2147483647 .
>
> which is false for x = -2147483648, y = -1
Right, I fell into the trap by focusing on Y /= 0 condition. Indeed, the assymetry of Integer'Range is causing troubles in this case.
Thank you for response.
--
Maciej Sobczak * http://www.msobczak.com * http://www.inspirel.com
prev parent reply other threads:[~2013-04-18 10:28 UTC|newest]
Thread overview: 3+ messages / expand[flat|nested] mbox.gz Atom feed top
2013-04-18 8:14 SPARK - division by zero problem Maciej Sobczak
2013-04-18 8:35 ` Phil Thornley
2013-04-18 10:28 ` Maciej Sobczak [this message]
replies disabled
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox