From 27cfe79c1867ece6edf0c4a4bfcbdecf01020774 Mon Sep 17 00:00:00 2001 From: Frank Busse <bb0xfb@gmail.com> Date: Tue, 21 Dec 2021 13:59:30 +0000 Subject: introduce BranchTypes --- lib/Core/Executor.h | 19 ++++++++++--------- 1 file changed, 10 insertions(+), 9 deletions(-) (limited to 'lib/Core/Executor.h') diff --git a/lib/Core/Executor.h b/lib/Core/Executor.h index e9763547..7da4f63c 100644 --- a/lib/Core/Executor.h +++ b/lib/Core/Executor.h @@ -19,6 +19,7 @@ #include "UserSearcher.h" #include "klee/ADT/RNG.h" +#include "klee/Core/BranchTypes.h" #include "klee/Core/Interpreter.h" #include "klee/Core/TerminationTypes.h" #include "klee/Expr/ArrayCache.h" @@ -324,16 +325,16 @@ private: /// Create a new state where each input condition has been added as /// a constraint and return the results. The input state is included - /// as one of the results. Note that the output vector may included + /// as one of the results. Note that the output vector may include /// NULL pointers for states which were unable to be created. - void branch(ExecutionState &state, - const std::vector< ref<Expr> > &conditions, - std::vector<ExecutionState*> &result); - - // Fork current and return states in which condition holds / does - // not hold, respectively. One of the states is necessarily the - // current state, and one of the states may be null. - StatePair fork(ExecutionState ¤t, ref<Expr> condition, bool isInternal); + void branch(ExecutionState &state, const std::vector<ref<Expr>> &conditions, + std::vector<ExecutionState *> &result, BranchType reason); + + /// Fork current and return states in which condition holds / does + /// not hold, respectively. One of the states is necessarily the + /// current state, and one of the states may be null. + StatePair fork(ExecutionState ¤t, ref<Expr> condition, bool isInternal, + BranchType reason); // If the MaxStatic*Pct limits have been reached, concretize the condition and // return it. Otherwise, return the unmodified condition. -- cgit 1.4.1