diff options
author | Nguyễn Gia Phong <cnx@loang.net> | 2023-07-31 15:22:48 +0900 |
---|---|---|
committer | Nguyễn Gia Phong <cnx@loang.net> | 2024-03-05 17:26:23 +0900 |
commit | d37a4bca5dd23feabf0e4554a997a4b505b47f05 (patch) | |
tree | 8b42da50ef095914f9d40e6a7107984925910aa6 | |
parent | 61434a77783c0f72df2df4799dd700ff25e22ad9 (diff) | |
download | klee-d37a4bca5dd23feabf0e4554a997a4b505b47f05.tar.gz |
Support 1-byte metavariables
-rw-r--r-- | lib/Core/ExecutionState.cpp | 17 |
1 files changed, 11 insertions, 6 deletions
diff --git a/lib/Core/ExecutionState.cpp b/lib/Core/ExecutionState.cpp index 9a39d2dc..270a3e16 100644 --- a/lib/Core/ExecutionState.cpp +++ b/lib/Core/ExecutionState.cpp @@ -402,13 +402,18 @@ std::string extractMetaEnvVar(ref<Expr> e) { if (constant->isFalse()) // the else branch return extractMetaEnvVar(eq->right); - if (eq->right.get()->getKind() != Expr::Concat) - return ""; - const auto concat = dyn_cast<ConcatExpr>(eq->right.get()); - if (concat->getLeft().get()->getKind() != Expr::Read) - return ""; + ReadExpr* read; + if (eq->right.get()->getKind() == Expr::Read) { + read = dyn_cast<ReadExpr>(eq->right.get()); + } else { + if (eq->right.get()->getKind() != Expr::Concat) + return ""; + const auto concat = dyn_cast<ConcatExpr>(eq->right.get()); + if (concat->getLeft().get()->getKind() != Expr::Read) + return ""; + read = dyn_cast<ReadExpr>(concat->getLeft().get()); + } - const auto read = dyn_cast<ReadExpr>(concat->getLeft().get()); const auto& name = read->updates.root->name; // string::starts_with requires C++20 if (name.substr(0, 8) != "__choose") |