Added support for bitvector constants to the SMTLIB parser. Only

variable and array support left.



git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@74690 91177308-0d34-0410-b5e6-96231b3b80d8

1 files changed, 9 insertions, 0 deletions

diff --git a/lib/SMT/SMTParser.cpp b/lib/SMT/SMTParser.cpp
index 32e453f0..6e40978a 100644
--- a/lib/SMT/SMTParser.cpp
+++ b/lib/SMT/SMTParser.cpp
@@ -77,6 +77,15 @@ int SMTParser::StringToInt(const std::string& s) {
 }
 
 
+ExprHandle SMTParser::GetConstExpr(std::string val, uint8_t base, klee::Expr::Width w) {
+  cerr << "In GetConstExpr(): val=" << val << ", base=" << (unsigned)base << ", width=" << w << "\n";
+  assert(base == 2 || base == 10 || base == 16);
+  llvm::APInt ap(w, val.c_str(), val.length(), base);
+  
+  return klee::ConstantExpr::alloc(ap);
+}
+
+
 void SMTParser::PushVarEnv() {
   cout << "Pushing new var env\n";
   varEnvs.push(VarEnv(varEnvs.top()));