From: benjaminhocking <benjaminhocking@gmail.com>
Subject: Re: (SPARK Ada) Proving that bitwise and is associative?
Date: Tue, 29 Apr 2014 14:11:51 -0500
Date: 2014-04-29T14:11:51-05:00 [thread overview]
Message-ID: <toCdnaD_COzqZMLOnZ2dnUVZ_i2dnZ2d@giganews.com> (raw)
In-Reply-To: nd2dnZa1N-bwUcLOnZ2dnUVZ_gOdnZ2d@giganews.com
If it helps in the diagnosis, here is the VC:
function_u8_5.
H1: true .
H2: value >= unsigned_32__first .
H3: value <= unsigned_32__last .
H4: umask_8 mod unsigned_32__modulus >= unsigned_32__first .
H5: umask_8 mod unsigned_32__modulus <= unsigned_32__last .
H6: bit__and(umask_8 mod unsigned_32__modulus, lmask_8 mod
unsigned_32__modulus) = 0 .
H7: bit__and(value, umask_8 mod unsigned_32__modulus) < 2 ** 16 mod
unsigned_32__modulus .
H8: bit__and(value, bit__and(umask_8 mod unsigned_32__modulus,
lmask_8 mod unsigned_32__modulus)) = 0 .
->
C1: bit__and(bit__and(value, umask_8 mod unsigned_32__modulus),
lmask_8 mod unsigned_32__modulus) = 0 .
Note that H8 should imply C1. The simplified VC is less helpful, as it has lost the equivalent of H8:
function_u8_5.
H1: value >= 0 .
H2: value <= 4294967295 .
H3: bit__and(value, 65280) < 65536 .
H4: unsigned_32__size >= 0 .
H5: unsigned_16__size >= 0 .
H6: unsigned_8__size >= 0 .
->
C1: bit__and(value, 65280) mod 256 = 0 .
next prev parent reply other threads:[~2014-04-29 19:11 UTC|newest]
Thread overview: 4+ messages / expand[flat|nested] mbox.gz Atom feed top
2014-04-29 15:59 (SPARK Ada) Proving that bitwise and is associative? benjaminhocking
2014-04-29 19:11 ` benjaminhocking [this message]
2014-04-30 12:39 ` Phil Thornley
2014-04-30 7:12 ` Stephen Leake
replies disabled
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox