================
@@ -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>();
+}
+
+// This trait points to the last expression (logical operator) where an eager
+// assumption introduced a state split (i.e. both cases were feasible). This is
+// used by the WeakLoopAssumption heuristic to find situations where the an
+// eager assumption introduces a state split within the evaluation of a loop
+// condition.
+REGISTER_TRAIT_WITH_PROGRAMSTATE(LastEagerlyAssumeAssumptionAt, const Expr *)
----------------
NagyDonat wrote:
I tried to emphasize that I'm only marking the `EagerlyAssume` checks that _did
assume something new_ (i.e. they introduce a state split). I'll probably rename
this to `LastEagerAssumptionStateSplitAt` or something similar.
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
