5 files changed, 45 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);
 
diff --git a/test/Solver/AShr_to_smtlib.kquery b/test/Solver/AShr_to_smtlib.kquery
new file mode 100644
index 00000000..774c46d9
--- /dev/null
+++ b/test/Solver/AShr_to_smtlib.kquery
@@ -0,0 +1,16 @@
+# RUN: %kleaver -print-smtlib -smtlib-abbreviation-mode=none %s > %t
+# RUN: diff -u %t %s.good.smt2
+
+# This test tries to check that the SMT-LIBv2 we generate when a AShrExpr is
+# used is correct.
+#
+# FIXME: We should really pass the generated query to an SMT solver that supports
+# SMT-LIBv2 and check it gives the correct answer ``unsat``. An older version of
+# KLEE where AShrExpr wasn't handled correctly would give ``sat`` for this query.
+#
+# We could fix this if we required STP to be in the user's PATH and made available
+# as a substitution in llvm-lit
+
+array value[1] : w32 -> w8 = symbolic
+array shift[1] : w32 -> w8 = symbolic
+(query [(Ule 8 (Read w8 0 shift))] (Eq 0 (AShr w8 (Read w8 0 value) (Read w8 0 shift))) )
diff --git a/test/Solver/AShr_to_smtlib.kquery.good.smt2 b/test/Solver/AShr_to_smtlib.kquery.good.smt2
new file mode 100644
index 00000000..e9478da6
--- /dev/null
+++ b/test/Solver/AShr_to_smtlib.kquery.good.smt2
@@ -0,0 +1,7 @@
+;SMTLIBv2 Query 0
+(set-logic QF_AUFBV )
+(declare-fun shift () (Array (_ BitVec 32) (_ BitVec 8) ) )
+(declare-fun value () (Array (_ BitVec 32) (_ BitVec 8) ) )
+(assert (and  (=  false (=  (_ bv0 8) (ite (bvuge (select  shift (_ bv0 32) ) (_ bv8 8) ) (_ bv0 8) (bvashr (select  value (_ bv0 32) ) (select  shift (_ bv0 32) ) ) ) ) ) (bvule  (_ bv8 8) (select  shift (_ bv0 32) ) ) ) )
+(check-sat)
+(exit)