1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
|
//===-- BranchTypes.h -------------------------------------------*- C++ -*-===//
//
// The KLEE Symbolic Virtual Machine
//
// This file is distributed under the University of Illinois Open Source
// License. See LICENSE.TXT for details.
//
//===----------------------------------------------------------------------===//
#ifndef KLEE_BRANCHTYPES_H
#define KLEE_BRANCHTYPES_H
#include <cstdint>
/// \cond DO_NOT_DOCUMENT
#define BRANCH_TYPES \
BTYPE(NONE, 0U) \
BTYPE(ConditionalBranch, 1U) \
BTYPE(IndirectBranch, 2U) \
BTYPE(Switch, 3U) \
BTYPE(Call, 4U) \
BTYPE(MemOp, 5U) \
BTYPE(ResolvePointer, 6U) \
BTYPE(Alloc, 7U) \
BTYPE(Realloc, 8U) \
BTYPE(Free, 9U) \
BTYPE(GetVal, 10U) \
MARK(END, 10U)
/// \endcond
/** @enum BranchType
* @brief Reason an ExecutionState forked
*
* | Value | Description |
* |---------------------------------|----------------------------------------------------------------------------------------------------|
* | `BranchType::NONE` | default value (no branch) |
* | `BranchType::ConditionalBranch` | branch caused by `br` instruction with symbolic condition |
* | `BranchType::IndirectBranch` | branch caused by `indirectbr` instruction with symbolic address |
* | `BranchType::Switch` | branch caused by `switch` instruction with symbolic value |
* | `BranchType::Call` | branch caused by `call` with symbolic function pointer |
* | `BranchType::MemOp` | branch caused by memory operation with symbolic address (e.g. multiple resolutions, out-of-bounds) |
* | `BranchType::ResolvePointer` | branch caused by symbolic pointer |
* | `BranchType::Alloc` | branch caused by symbolic `alloc`ation size |
* | `BranchType::Realloc` | branch caused by symbolic `realloc`ation size |
* | `BranchType::Free` | branch caused by `free`ing symbolic pointer |
* | `BranchType::GetVal` | branch caused by user-invoked concretization while seeding |
*/
enum class BranchType : std::uint8_t {
/// \cond DO_NOT_DOCUMENT
#define BTYPE(N,I) N = (I),
#define MARK(N,I) N = (I),
BRANCH_TYPES
#undef BTYPE
#undef MARK
/// \endcond
};
#endif
|
