Jiri Slaby
e18feb65f3
OBS-URL: https://build.opensuse.org/package/show/devel:tools:statica/klee?expand=0&rev=51
72 lines
2.2 KiB
Diff
72 lines
2.2 KiB
Diff
From: Jiri Slaby <jirislaby@gmail.com>
|
|
Date: Fri, 15 Jun 2018 10:32:26 +0200
|
|
Subject: test: remove undefined behaviour
|
|
Patch-mainline: no
|
|
|
|
Shifting negative values is implementation-defined.
|
|
|
|
Shifting by equal number of the bits as is the size of the type is
|
|
undefined.
|
|
|
|
So fix both of these.
|
|
|
|
This fixes #911.
|
|
|
|
Signed-off-by: Jiri Slaby <jirislaby@gmail.com>
|
|
---
|
|
.../Feature/arithmetic-right-overshift-sym-conc.c | 15 +++++++++------
|
|
1 file changed, 9 insertions(+), 6 deletions(-)
|
|
|
|
diff --git a/test/Feature/arithmetic-right-overshift-sym-conc.c b/test/Feature/arithmetic-right-overshift-sym-conc.c
|
|
index 7af6f9d7f08f..63b93db32ed9 100644
|
|
--- a/test/Feature/arithmetic-right-overshift-sym-conc.c
|
|
+++ b/test/Feature/arithmetic-right-overshift-sym-conc.c
|
|
@@ -13,14 +13,17 @@ typedef enum
|
|
UNKNOWN
|
|
} overshift_t;
|
|
|
|
+#define INT_31_BITS (0xffffffff >> 1)
|
|
+
|
|
// We're using signed ints so should be doing
|
|
// arithmetic right shift.
|
|
// lhs should be a constant
|
|
-int overshift(signed int lhs, volatile unsigned int y, const char * type)
|
|
+unsigned int overshift(unsigned int lhs, volatile unsigned int y,
|
|
+ const char *type)
|
|
{
|
|
overshift_t ret;
|
|
- volatile signed int x = lhs;
|
|
- unsigned int limit = sizeof(x)*8;
|
|
+ volatile unsigned int x = lhs;
|
|
+ unsigned int limit = sizeof(x)*8 - 1;
|
|
assert(!klee_is_symbolic(x));
|
|
|
|
volatile signed int result;
|
|
@@ -47,12 +50,12 @@ int overshift(signed int lhs, volatile unsigned int y, const char * type)
|
|
|
|
int main(int argc, char** argv)
|
|
{
|
|
- volatile unsigned int y = sizeof(unsigned int)*8;
|
|
+ volatile unsigned int y = sizeof(unsigned int)*8 - 1;
|
|
// Try with +ve lhs
|
|
overshift_t conc = overshift(15, y, "Concrete");
|
|
assert(conc == TO_ZERO);
|
|
// Try with -ve lhs
|
|
- conc = overshift(-1, y, "Concrete");
|
|
+ conc = overshift(INT_31_BITS, y, "Concrete");
|
|
assert(conc == TO_ZERO);
|
|
|
|
// Symbolic overshift
|
|
@@ -65,7 +68,7 @@ int main(int argc, char** argv)
|
|
overshift_t sym = overshift(15, y2, "Symbolic");
|
|
assert(sym == TO_ZERO);
|
|
// Try with -ve lhs
|
|
- sym = overshift(-1, y2, "Symbolic");
|
|
+ sym = overshift(INT_31_BITS, y2, "Symbolic");
|
|
assert(sym == TO_ZERO);
|
|
|
|
// Concrete and symbolic behaviour should be the same
|
|
--
|
|
2.17.1
|
|
|