diff options
| -rw-r--r-- | include/klee/util/ExprSMTLIBPrinter.h | 4 | ||||
| -rw-r--r-- | lib/Expr/ExprSMTLIBPrinter.cpp | 18 |
2 files changed, 11 insertions, 11 deletions
diff --git a/include/klee/util/ExprSMTLIBPrinter.h b/include/klee/util/ExprSMTLIBPrinter.h index a27d2bbc..6b0d260a 100644 --- a/include/klee/util/ExprSMTLIBPrinter.h +++ b/include/klee/util/ExprSMTLIBPrinter.h @@ -82,7 +82,7 @@ public: enum SMTLIBv2Logic { QF_ABV, ///< Logic using Theory of Arrays and Theory of Bitvectors QF_AUFBV ///< Logic using Theory of Arrays and Theory of Bitvectors and has - ///uninterpreted functions + ///< uninterpreted functions }; /// Different SMTLIBv2 options that have a boolean value that can be set @@ -99,7 +99,7 @@ public: OPTION_TRUE, ///< Set option to true OPTION_FALSE, ///< Set option to false OPTION_DEFAULT ///< Use solver's defaults (the option will not be set in - ///output) + ///< output) }; enum ConstantDisplayMode { diff --git a/lib/Expr/ExprSMTLIBPrinter.cpp b/lib/Expr/ExprSMTLIBPrinter.cpp index b5fefc92..9db6f328 100644 --- a/lib/Expr/ExprSMTLIBPrinter.cpp +++ b/lib/Expr/ExprSMTLIBPrinter.cpp @@ -241,7 +241,7 @@ void ExprSMTLIBPrinter::printFullExpression( case Expr::Eq: /* The "=" operator is special in that it can take any sort but we must - * enforce that both arguments are the same type. We do this a lazy way + * enforce that both arguments are the same sort. We do this in a lazy way * by enforcing the second argument is of the same type as the first. */ printSortArgsExpr(e, getSort(e->getKid(0))); @@ -254,8 +254,8 @@ void ExprSMTLIBPrinter::printFullExpression( case Expr::Not: /* These operators have a bitvector version and a bool version. * For these operators only (e.g. wouldn't apply to bvult) if the expected - * sort the - * expression is T then that implies the arguments are also of type T. + * sort of the expression is T then that implies the arguments are also of + * type T. */ printLogicalOrBitVectorExpr(e, expectedSort); @@ -307,7 +307,7 @@ void ExprSMTLIBPrinter::printExtractExpr(const ref<ExtractExpr> &e) { } void ExprSMTLIBPrinter::printCastExpr(const ref<CastExpr> &e) { - /* sign_extend and zero_extend behave slightly unusually in SMTLIBv2 + /* sign_extend and zero_extend behave slightly unusually in SMTLIBv2, * instead of specifying of what bit-width we would like to extend to * we specify how many bits to add to the child expression * @@ -667,8 +667,8 @@ void ExprSMTLIBPrinter::scan(const ref<Expr> &e) { if (const ReadExpr *re = dyn_cast<ReadExpr>(e)) { - // Attempt to insert array and if array wasn't present before do more things if (usedArrays.insert(re->updates.root).second) { + // Array was not recorded before // check if the array is constant if (re->updates.root->isConstantArray()) @@ -835,7 +835,7 @@ void ExprSMTLIBPrinter::printAssert(const ref<Expr> &e) { // to print nested let expressions bindings.clear(); - // Print each binding on it's level + // Print each binding on its level for (unsigned i = 0; i < orderedBindings.size(); ++i) { BindingMap levelBindings = orderedBindings[i]; for (BindingMap::const_iterator j = levelBindings.begin(); @@ -944,9 +944,9 @@ void ExprSMTLIBPrinter::printCastToSort(const ref<Expr> &e, *p << ")"; break; case SORT_BOOL: { - /* We make the assumption (might be wrong) that any bitvector whos unsigned - *decimal value is - * is zero is interpreted as "false", otherwise it is true. + /* We make the assumption (might be wrong) that any bitvector whose unsigned + * decimal value is is zero is interpreted as "false", otherwise it is + * true. * * This may not be the interpretation we actually want! */ |