diff options
author | Andrea Mattavelli <andreamattavelli@gmail.com> | 2017-02-13 09:30:41 +0000 |
---|---|---|
committer | Dan Liew <delcypher@gmail.com> | 2017-02-14 13:47:59 +0000 |
commit | 89e11e68ae336b6b4530c0e03b85519efa35a29d (patch) | |
tree | 24589ed6a267feb5038aed1bf2f4f1ebff95c82b /include | |
parent | 449d520c07a4d2a356b155f593d9e39db76e6c85 (diff) | |
download | klee-89e11e68ae336b6b4530c0e03b85519efa35a29d.tar.gz |
Added pre/post conditions as assertions
Diffstat (limited to 'include')
-rw-r--r-- | include/klee/util/Bits.h | 17 |
1 files changed, 14 insertions, 3 deletions
diff --git a/include/klee/util/Bits.h b/include/klee/util/Bits.h index f228b289..7d1797f5 100644 --- a/include/klee/util/Bits.h +++ b/include/klee/util/Bits.h @@ -12,12 +12,14 @@ #include "klee/Config/Version.h" #include "llvm/Support/DataTypes.h" +#include <assert.h> namespace klee { namespace bits32 { // @pre(0 <= N <= 32) // @post(retval = max([truncateToNBits(i,N) for i in naturals()])) inline unsigned maxValueOfNBits(unsigned N) { + assert(N <= 32); if (N==0) return 0; return ((unsigned) -1) >> (32 - N); @@ -25,6 +27,7 @@ namespace klee { // @pre(0 < N <= 32) inline unsigned truncateToNBits(unsigned x, unsigned N) { + assert(N > 0 && N <= 32); return x&(((unsigned) -1) >> (32 - N)); } @@ -44,12 +47,15 @@ namespace klee { // @pre(withoutRightmostBit(x) == 0) // @post((1 << retval) == x) inline unsigned indexOfSingleBit(unsigned x) { + assert(withoutRightmostBit(x) == 0); unsigned res = 0; if (x&0xFFFF0000) res += 16; if (x&0xFF00FF00) res += 8; if (x&0xF0F0F0F0) res += 4; if (x&0xCCCCCCCC) res += 2; if (x&0xAAAAAAAA) res += 1; + assert(res < 32); + assert((UINT32_C(1) << res) == x); return res; } @@ -59,9 +65,10 @@ namespace klee { } namespace bits64 { - // @pre(0 <= N <= 32) + // @pre(0 <= N <= 64) // @post(retval = max([truncateToNBits(i,N) for i in naturals()])) inline uint64_t maxValueOfNBits(unsigned N) { + assert(N <= 64); if (N==0) return 0; return ((uint64_t) (int64_t) -1) >> (64 - N); @@ -69,6 +76,7 @@ namespace klee { // @pre(0 < N <= 64) inline uint64_t truncateToNBits(uint64_t x, unsigned N) { + assert(N > 0 && N <= 64); return x&(((uint64_t) (int64_t) -1) >> (64 - N)); } @@ -88,9 +96,12 @@ namespace klee { // @pre((x&(x-1)) == 0) // @post((1 << retval) == x) inline unsigned indexOfSingleBit(uint64_t x) { + assert((x & (x - 1)) == 0); unsigned res = bits32::indexOfSingleBit((unsigned) (x | (x>>32))); - if (x&((uint64_t) 0xFFFFFFFF << 32)) - res += 32; + if (x & ((uint64_t)0xFFFFFFFF << 32)) + res += 32; + assert(res < 64); + assert((UINT64_C(1) << res) == x); return res; } |