Skip to content

Commit

Permalink
use ref
Browse files Browse the repository at this point in the history
  • Loading branch information
ladisgin committed Oct 27, 2023
1 parent 2f251c8 commit 314646f
Show file tree
Hide file tree
Showing 3 changed files with 5 additions and 4 deletions.
2 changes: 1 addition & 1 deletion include/klee/Expr/AlphaBuilder.h
Original file line number Diff line number Diff line change
Expand Up @@ -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<Expr> build(ref<Expr> v);
const Array *buildArray(const Array *arr) { return visitArray(arr); }
};
Expand Down
5 changes: 3 additions & 2 deletions lib/Expr/AlphaBuilder.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -65,16 +65,17 @@ 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<Expr> v = visit(arg);
reverseExprMap[v] = arg;
reverseExprMap[Expr::createIsZero(v)] = Expr::createIsZero(arg);
result.insert(v);
}
return result;
}

ref<Expr> AlphaBuilder::build(ref<Expr> v) {
ref<Expr> e = visit(v);
reverseExprMap[e] = v;
Expand Down
2 changes: 1 addition & 1 deletion test/Feature/MockStrategies.c
Original file line number Diff line number Diff line change
Expand Up @@ -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

Expand Down

0 comments on commit 314646f

Please sign in to comment.