=?utf-8?q?Donát?= Nagy <donat.n...@ericsson.com>
Message-ID:
In-Reply-To: <llvm.org/llvm/llvm-project/pull/109...@github.com>
================
@@ -212,6 +212,25 @@ typedef llvm::ImmutableMap<const LocationContext *,
unsigned>
REGISTER_TRAIT_WITH_PROGRAMSTATE(PendingArrayDestruction,
PendingArrayDestructionMap)
+// This trait is used to heuristically filter out results produced from
+// execution paths that took "weak" assumptions within a loop.
+REGISTER_TRAIT_WITH_PROGRAMSTATE(SeenWeakLoopAssumption, bool)
+
+ProgramStateRef clang::ento::recordWeakLoopAssumption(ProgramStateRef State) {
+ return State->set<SeenWeakLoopAssumption>(true);
+}
+
+bool clang::ento::seenWeakLoopAssumption(ProgramStateRef State) {
+ return State->get<SeenWeakLoopAssumption>();
+}
----------------
isuckatcs wrote:
Every registered trait should be removed when they are no longer needed to stop
polluting the states. Also, aren't the traits part of the exploded graph? If
they are and they are not cleaned up, they pollute the egraph too.
https://github.com/llvm/llvm-project/pull/109804
_______________________________________________
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
