Skip to content

Commit 61798c6

Browse files
committed
Use klee_assume(s[N - 1] == '\0') call for the last element of string
1 parent 4ec9145 commit 61798c6

File tree

1 file changed

+1
-1
lines changed

1 file changed

+1
-1
lines changed

server/src/printers/KleeConstraintsPrinter.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -120,7 +120,7 @@ void KleeConstraintsPrinter::genConstraintsForMultiPointerOrArray(const Constrai
120120
std::vector<std::string> charSizes(indexes.begin(), indexes.end() - 1);
121121
const auto charElement = constrMultiIndex(state.curElement, charSizes);
122122
ss << TAB_N() << "if (" << indexes.back() << PrinterUtils::EQ_OPERATOR << sizes.back() - 1 << ")" << LB();
123-
ss << TAB_N() << charElement << "[" << sizes.back() - 1 << "]" << PrinterUtils::ASSIGN_OPERATOR << "'\\0'" << SCNL;
123+
ss << TAB_N() << PrinterUtils::KLEE_ASSUME << "(" << charElement << "[" << sizes.back() - 1 << "]" << PrinterUtils::EQ_OPERATOR << "'\\0'" << ")" << SCNL;
124124
ss << TAB_N() << "break" << SCNL;
125125
ss << RB();
126126
}

0 commit comments

Comments
 (0)