From 314646f64425475fe60f95ac0fb22f53876eb76e Mon Sep 17 00:00:00 2001 From: Vladislav Kalugin Date: Fri, 27 Oct 2023 18:11:09 +0300 Subject: [PATCH] use ref --- include/klee/Expr/AlphaBuilder.h | 2 +- lib/Expr/AlphaBuilder.cpp | 5 +++-- test/Feature/MockStrategies.c | 2 +- 3 files changed, 5 insertions(+), 4 deletions(-) diff --git a/include/klee/Expr/AlphaBuilder.h b/include/klee/Expr/AlphaBuilder.h index 9095c489e2a..08d083a10ef 100644 --- a/include/klee/Expr/AlphaBuilder.h +++ b/include/klee/Expr/AlphaBuilder.h @@ -33,7 +33,7 @@ class AlphaBuilder final : public ExprVisitor { public: AlphaBuilder(ArrayCache &_arrayCache); - constraints_ty visitConstraints(constraints_ty cs); + constraints_ty visitConstraints(const constraints_ty& cs); ref build(ref v); const Array *buildArray(const Array *arr) { return visitArray(arr); } }; diff --git a/lib/Expr/AlphaBuilder.cpp b/lib/Expr/AlphaBuilder.cpp index b3b98723c99..d81c7906db2 100644 --- a/lib/Expr/AlphaBuilder.cpp +++ b/lib/Expr/AlphaBuilder.cpp @@ -65,9 +65,9 @@ ExprVisitor::Action AlphaBuilder::visitRead(const ReadExpr &re) { AlphaBuilder::AlphaBuilder(ArrayCache &_arrayCache) : arrayCache(_arrayCache) {} -constraints_ty AlphaBuilder::visitConstraints(constraints_ty cs) { +constraints_ty AlphaBuilder::visitConstraints(const constraints_ty &cs) { constraints_ty result; - for (auto arg : cs) { + for (const auto &arg : cs) { ref v = visit(arg); reverseExprMap[v] = arg; reverseExprMap[Expr::createIsZero(v)] = Expr::createIsZero(arg); @@ -75,6 +75,7 @@ constraints_ty AlphaBuilder::visitConstraints(constraints_ty cs) { } return result; } + ref AlphaBuilder::build(ref v) { ref e = visit(v); reverseExprMap[e] = v; diff --git a/test/Feature/MockStrategies.c b/test/Feature/MockStrategies.c index c69b74b7de5..524fbba3a2d 100644 --- a/test/Feature/MockStrategies.c +++ b/test/Feature/MockStrategies.c @@ -18,7 +18,7 @@ // CHECK-3: KLEE: ERROR: Deterministic mocks can be generated with Z3 solver only. // RUN: rm -rf %t.klee-out-4 -// RUN: %klee --output-dir=%t.klee-out-4 --solver-backend=z3 --external-calls=all --mock-strategy=deterministic %t.bc 2>&1 | FileCheck %s -check-prefix=CHsECK-4 +// RUN: %klee --output-dir=%t.klee-out-4 --solver-backend=z3 --external-calls=all --mock-strategy=deterministic %t.bc 2>&1 | FileCheck %s -check-prefix=CHECK-4 // CHECK-4: KLEE: done: completed paths = 2 // CHECK-4: KLEE: done: generated tests = 2