diff options
Diffstat (limited to 'test')
| -rw-r--r-- | test/Solver/AShr_to_smtlib.kquery | 16 | ||||
| -rw-r--r-- | test/Solver/AShr_to_smtlib.kquery.good.smt2 | 7 |
2 files changed, 23 insertions, 0 deletions
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) |