diff options
Diffstat (limited to 'test')
| -rw-r--r-- | test/Feature/arithmetic-right-overshift-sym-conc.c | 25 | ||||
| -rw-r--r-- | test/Programs/pcregrep.c | 4 | ||||
| -rw-r--r-- | test/Runtime/Uclibc/2007-10-08-optimization-calls-wrong-libc-functions.c | 4 |
3 files changed, 22 insertions, 11 deletions
diff --git a/test/Feature/arithmetic-right-overshift-sym-conc.c b/test/Feature/arithmetic-right-overshift-sym-conc.c index a771bc75..7af6f9d7 100644 --- a/test/Feature/arithmetic-right-overshift-sym-conc.c +++ b/test/Feature/arithmetic-right-overshift-sym-conc.c @@ -15,11 +15,13 @@ typedef enum // We're using signed ints so should be doing // arithmetic right shift. -int overshift(volatile unsigned int y, const char * type) +// lhs should be a constant +int overshift(signed int lhs, volatile unsigned int y, const char * type) { overshift_t ret; - volatile signed int x=15; + volatile signed int x = lhs; unsigned int limit = sizeof(x)*8; + assert(!klee_is_symbolic(x)); volatile signed int result; result = x >> y; // Potential overshift @@ -45,10 +47,13 @@ int overshift(volatile unsigned int y, const char * type) int main(int argc, char** argv) { - // Concrete overshift volatile unsigned int y = sizeof(unsigned int)*8; - overshift_t conc = overshift(y, "Concrete"); - assert( conc == TO_ZERO); + // Try with +ve lhs + overshift_t conc = overshift(15, y, "Concrete"); + assert(conc == TO_ZERO); + // Try with -ve lhs + conc = overshift(-1, y, "Concrete"); + assert(conc == TO_ZERO); // Symbolic overshift volatile unsigned int y2; @@ -56,11 +61,15 @@ int main(int argc, char** argv) // Add constraints so only one value possible klee_assume(y2 > (y-1)); klee_assume(y2 < (y+1)); - overshift_t sym = overshift(y2, "Symbolic"); - assert( sym == TO_ZERO); + // Try with +ve lhs + overshift_t sym = overshift(15, y2, "Symbolic"); + assert(sym == TO_ZERO); + // Try with -ve lhs + sym = overshift(-1, y2, "Symbolic"); + assert(sym == TO_ZERO); // Concrete and symbolic behaviour should be the same - assert( conc == sym); + assert(conc == sym); return 0; } diff --git a/test/Programs/pcregrep.c b/test/Programs/pcregrep.c index fb99ef87..5ed8f4fa 100644 --- a/test/Programs/pcregrep.c +++ b/test/Programs/pcregrep.c @@ -211,7 +211,7 @@ struct l_struct_2E_pcre { /* Function Declarations */ double fmod(double, double); float fmodf(float, float); -unsigned int main(unsigned int llvm_cbe_argc, unsigned char **llvm_cbe_argv); +int main(int llvm_cbe_argc, char **llvm_cbe_argv); unsigned int fprintf(struct l_struct_2E__IO_FILE *, unsigned char *, ...); unsigned int __strtol_internal(unsigned char *, unsigned char **, unsigned int , unsigned int ); unsigned int printf(unsigned char *, ...); @@ -319,7 +319,7 @@ static inline int llvm_fcmp_ogt(double X, double Y) { return X > Y ; } static inline int llvm_fcmp_ole(double X, double Y) { return X <= Y ; } static inline int llvm_fcmp_oge(double X, double Y) { return X >= Y ; } -unsigned int main(unsigned int llvm_cbe_argc, unsigned char **llvm_cbe_argv) { +int main(int llvm_cbe_argc, char **llvm_cbe_argv) { unsigned int llvm_cbe_length_i_i; /* Address-exposed local */ unsigned int llvm_cbe_firstbyte_i_i; /* Address-exposed local */ unsigned int llvm_cbe_reqbyte_i_i; /* Address-exposed local */ diff --git a/test/Runtime/Uclibc/2007-10-08-optimization-calls-wrong-libc-functions.c b/test/Runtime/Uclibc/2007-10-08-optimization-calls-wrong-libc-functions.c index 71f6d07a..d82f0eb9 100644 --- a/test/Runtime/Uclibc/2007-10-08-optimization-calls-wrong-libc-functions.c +++ b/test/Runtime/Uclibc/2007-10-08-optimization-calls-wrong-libc-functions.c @@ -5,10 +5,12 @@ #include <string.h> #include <assert.h> +#include "klee/klee.h" + int main() { int a; - klee_make_symbolic(&a, sizeof a); + klee_make_symbolic(&a, sizeof a, "a"); memset(&a, 0, sizeof a); |