Commented few print statements for better readability #382
Conversation
|
Thanks @ArpitaDutta . Can you please add the condition for -debug-subsumption=4 to the code too. You can search for |
|
Sure @rasool Maghareh ***@***.***> I will do this.
…On Fri, Sep 10, 2021 at 10:06 AM Rasool Maghareh ***@***.***> wrote:
Thanks @ArpitaDutta <https://github.com/ArpitaDutta> . Can you please add
the condition for -debug-subsumption=4 to the code too. You can search for if
(debugSubsumptionLevel >= 3) and see how it works.
—
You are receiving this because you were mentioned.
Reply to this email directly, view it on GitHub
<#382 (comment)>, or
unsubscribe
<https://github.com/notifications/unsubscribe-auth/AD22LADLNUDNB6KP3MSBCOLUBFRZDANCNFSM5DYLH7OA>
.
Triage notifications on the go with GitHub Mobile for iOS
<https://apps.apple.com/app/apple-store/id1477376905?ct=notification-email&mt=8&pt=524675>
or Android
<https://play.google.com/store/apps/details?id=com.github.android&referrer=utm_campaign%3Dnotification-email%26utm_medium%3Demail%26utm_source%3Dgithub>.
|
lib/Core/Executor.cpp
Outdated
| @@ -2858,11 +2858,15 @@ void Executor::executeInstruction(ExecutionState &state, KInstruction *ki) { | |||
| Instruction *i = ki->inst; | |||
| // if this is starting a new BB then | |||
| // check for non-linear & new BB in speculation mode | |||
|
|
|||
There was a problem hiding this comment.
Please remove white space.
lib/Core/Executor.cpp
Outdated
| if (INTERPOLATION_ENABLED && SpecTypeToUse != NO_SPEC && | ||
| txTree->isSpeculationNode() && | ||
| (i == &state.txTreeNode->getBasicBlock()->front())) { | ||
| // check non-linear | ||
| uintptr_t pp = state.txTreeNode->getProgramPoint(); | ||
| //i->dump(); |
There was a problem hiding this comment.
Please remove these three lines. They are commented code.
lib/Core/TxPrintUtil.cpp
Outdated
| @@ -537,15 +537,15 @@ TxPrettyExpressionBuilder::constructQuery(ConstraintManager &constraints, | |||
| std::string msg; | |||
| std::string tabs = makeTabs(1); | |||
| llvm::raw_string_ostream stream(msg); | |||
| stream << "antecedent:\n"; | |||
| /*stream << "antecedent:\n"; | |||
There was a problem hiding this comment.
These lines should not be commented. As discussed in our last meeting these lines should be guarded by: if (debugSubsumptionLevel >= 4) .
lib/Core/TxTree.cpp
Outdated
| @@ -1598,9 +1598,10 @@ bool TxSubsumptionTableEntry::subsumed( | |||
| } | |||
|
|
|||
| if (debugSubsumptionLevel >= 2) { | |||
| klee_message("Querying for subsumption check:\n%s", | |||
| /* klee_message("Querying for subsumption check:\n%s", | |||
There was a problem hiding this comment.
These lines should not be commented. As discussed in our last meeting these lines should be guarded by: if (debugSubsumptionLevel >= 4).
lib/Core/TxTree.cpp
Outdated
| @@ -1634,9 +1635,10 @@ bool TxSubsumptionTableEntry::subsumed( | |||
|
|
|||
| } else { | |||
| if (debugSubsumptionLevel >= 2) { | |||
| klee_message("Querying for subsumption check:\n%s", | |||
| /*klee_message("Querying for subsumption check:\n%s", | |||
There was a problem hiding this comment.
These lines should not be commented. As discussed in our last meeting these lines should be guarded by: if (debugSubsumptionLevel >= 4).
lib/Core/TxValues.cpp
Outdated
| @@ -633,11 +633,11 @@ void TxInterpolantValue::print(llvm::raw_ostream &stream, | |||
| std::string nextTabs = appendTab(prefix); | |||
| bool offsetDisplayed = false; | |||
|
|
|||
| stream << prefix << "function/value: "; | |||
| /*stream << prefix << "function/value: "; | |||
There was a problem hiding this comment.
These lines should not be commented. As discussed in our last meeting these lines should be guarded by: if (debugSubsumptionLevel >= 4) .
lib/Core/TxValues.cpp
Outdated
| @@ -694,7 +694,7 @@ void TxInterpolantValue::print(llvm::raw_ostream &stream, | |||
| expr->print(stream); | |||
| } | |||
|
|
|||
| if (!coreReasons.empty()) { | |||
| /* if (!coreReasons.empty()) { | |||
There was a problem hiding this comment.
These lines should not be commented. As discussed in our last meeting these lines should be guarded by: if (debugSubsumptionLevel >= 4) .
lib/Core/TxValues.cpp
Outdated
| @@ -795,7 +795,7 @@ void TxStateAddress::print(llvm::raw_ostream &stream, | |||
| std::string tabsNext = appendTab(prefix); | |||
|
|
|||
| variable->print(stream, prefix); | |||
| stream << "\n"; | |||
| /*stream << "\n"; | |||
There was a problem hiding this comment.
These lines should not be commented. As discussed in our last meeting these lines should be guarded by: if (debugSubsumptionLevel >= 4) .
lib/Core/TxValues.cpp
Outdated
| @@ -923,19 +923,19 @@ void TxStateValue::printMinimal(llvm::raw_ostream &stream, | |||
| const std::string &prefix) const { | |||
| std::string tabsNext = appendTab(prefix); | |||
|
|
|||
| stream << prefix << "function/value: "; | |||
| /*stream << prefix << "function/value: "; | |||
There was a problem hiding this comment.
These lines should not be commented. As discussed in our last meeting these lines should be guarded by: if (debugSubsumptionLevel >= 4) .
lib/Core/TxValues.cpp
Outdated
| stream << prefix << "expression: "; | ||
| if (!valueExpr.isNull()) | ||
| valueExpr->print(stream); | ||
| else | ||
| stream << "NULL"; | ||
| stream << "\n"; | ||
| stream << prefix | ||
| << "pointer to location object: " << reinterpret_cast<uintptr_t>(this); | ||
| /*stream << prefix |
There was a problem hiding this comment.
These lines should not be commented. As discussed in our last meeting these lines should be guarded by: if (debugSubsumptionLevel >= 4) .
|
The code works properly on local tests. |
Removed few print statements for better readability.