From 4b477f8108a2a92012ff138725f6c6f26ccb23e5 Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Thu, 29 Aug 2013 17:30:33 +0100 Subject: Implemented runtime check for overshift (controllable with --check-overshift command line argument). Overshift is where a Shl, AShr or LShr has a shift width greater than the bit width of the first operand. This is undefined behaviour in LLVM so we report this as an error. --- test/Feature/OvershiftCheck.c | 26 ++++++++++++++++++++++++++ 1 file changed, 26 insertions(+) create mode 100644 test/Feature/OvershiftCheck.c (limited to 'test/Feature') diff --git a/test/Feature/OvershiftCheck.c b/test/Feature/OvershiftCheck.c new file mode 100644 index 00000000..bb967166 --- /dev/null +++ b/test/Feature/OvershiftCheck.c @@ -0,0 +1,26 @@ +// RUN: %llvmgcc %s -emit-llvm -g -O0 -c -o %t.bc +// RUN: %klee -check-overshift %t.bc 2> %t.log +// RUN: grep -c "overshift error" %t.log +// RUN: grep -c "OvershiftCheck.c:19: overshift error" %t.log +// RUN: grep -c "OvershiftCheck.c:23: overshift error" %t.log + +/* This test checks that two consecutive potential overshifts + * are reported as errors. + */ +int main() +{ + unsigned int x=15; + unsigned int y; + unsigned int z; + volatile unsigned int result; + + /* Overshift if y>= sizeof(x) */ + klee_make_symbolic(&y,sizeof(y),"shift_amount1"); + result = x << y; + + /* Overshift is z>= sizeof(x) */ + klee_make_symbolic(&z,sizeof(z),"shift_amount2"); + result = x >> z; + + return 0; +} -- cgit 1.4.1