Classifications of error on TP and FP

include/klee/Core/TerminationTypes.h

@@ -85,6 +85,8 @@ enum class StateTerminationType : std::uint8_t {
   /// \endcond
 };
 
+enum StateTerminationConfidenceCategory { CONFIDENT, PROBABLY };
+
 namespace HaltExecution {
 enum Reason {
   NotHalt = 0,

lib/Core/CodeEvent.h

@@ -152,6 +152,10 @@ struct ErrorEvent : public CodeEvent {
   /// @brief ID for this error.
   const StateTerminationType ruleID;
 
+  /// @brief Confidence of this error: may be considered
+  /// as a flag of `true positive` error for instance.
+  const StateTerminationConfidenceCategory confidence;
+
   /// @brief Message describing this error.
   const std::string message;
 
@@ -161,14 +165,17 @@ struct ErrorEvent : public CodeEvent {
   const std::optional<ref<CodeEvent>> source;
 
   ErrorEvent(const ref<CodeEvent> &source, const ref<CodeLocation> &sink,
-             StateTerminationType ruleID, const std::string &message)
-      : CodeEvent(EventKind::ERR, sink), ruleID(ruleID), message(message),
-        source(source) {}
+             StateTerminationType ruleID,
+             StateTerminationConfidenceCategory confidence,
+             const std::string &message)
+      : CodeEvent(EventKind::ERR, sink), ruleID(ruleID), confidence(confidence),
+        message(message), source(source) {}
 
   ErrorEvent(const ref<CodeLocation> &sink, StateTerminationType ruleID,
+             StateTerminationConfidenceCategory confidence,
              const std::string &message)
-      : CodeEvent(EventKind::ERR, sink), ruleID(ruleID), message(message),
-        source(std::nullopt) {}
+      : CodeEvent(EventKind::ERR, sink), ruleID(ruleID), confidence(confidence),
+        message(message), source(std::nullopt) {}
 
   std::string description() const override { return message; }
 

lib/Core/ExecutionState.cpp

@@ -160,7 +160,9 @@ ExecutionState::~ExecutionState() {
 ExecutionState::ExecutionState(const ExecutionState &state)
     : initPC(state.initPC), pc(state.pc), prevPC(state.prevPC),
       stack(state.stack), stackBalance(state.stackBalance),
-      incomingBBIndex(state.incomingBBIndex), depth(state.depth),
+      incomingBBIndex(state.incomingBBIndex),
+      lastBrConfidently(state.lastBrConfidently),
+      nullPointerMarkers(state.nullPointerMarkers), depth(state.depth),
       level(state.level), addressSpace(state.addressSpace),
       constraints(state.constraints), eventsRecorder(state.eventsRecorder),
       targetForest(state.targetForest), pathOS(state.pathOS),

lib/Core/ExecutionState.h

@@ -317,6 +317,12 @@ class ExecutionState {
 
   // Overall state of the state - Data specific
 
+  /// @brief: TODO:
+  bool lastBrConfidently = true;
+
+  /// @brief: TODO:
+  ImmutableList<ref<Expr>> nullPointerMarkers;
+
   /// @brief Exploration depth, i.e., number of times KLEE branched for this
   /// state
   std::uint32_t depth = 0;