 |
|
 |
|
| Files: |
1 |
|
Branches Taken: |
0.0% |
0 / 0 |
| Generated: |
2009-05-17 22:47 |
|
Branches Executed: |
0.0% |
0 / 0 |
| |
|
Line Coverage: |
100.0% |
1 / 1 |
| |
 |
|
 |
1 : //===- Executor.h - --*- C++ -*-===//
2 :
3 : #ifndef KLEE_SPECIALFUNCTIONHANDLER_H
4 : #define KLEE_SPECIALFUNCTIONHANDLER_H
5 :
6 : #include <map>
7 : #include <vector>
8 : #include <string>
9 :
10 : namespace llvm {
11 : class Function;
12 : }
13 :
14 : namespace klee {
15 : class Executor;
16 : class Expr;
17 : class ExecutionState;
18 : class KInstruction;
19 : template<typename T> class ref;
20 :
21 103: class SpecialFunctionHandler {
22 : public:
23 : typedef void (SpecialFunctionHandler::*Handler)(ExecutionState &state,
24 : KInstruction *target,
25 : std::vector<ref<Expr> > &arguments);
26 : std::map<const llvm::Function*,
27 : std::pair<Handler,bool> > handlers;
28 : class Executor &executor;
29 :
30 : public:
31 : SpecialFunctionHandler(Executor &_executor);
32 :
33 : /// Perform any modifications on the LLVM module before it is
34 : /// prepared for execution. At the moment this involves deleting
35 : /// unused function bodies and marking intrinsics with appropriate
36 : /// flags for use in optimizations.
37 : void prepare();
38 :
39 : /// Initialize the internal handler map after the module has been
40 : /// prepared for execution.
41 : void bind();
42 :
43 : bool handle(ExecutionState &state,
44 : llvm::Function *f,
45 : KInstruction *target,
46 : std::vector< ref<Expr> > &arguments);
47 :
48 : /* Convenience routines */
49 :
50 : std::string readStringAtAddress(ExecutionState &state, ref<Expr> address);
51 :
52 : /* Handlers */
53 :
54 : #define HANDLER(name) void name(ExecutionState &state, \
55 : KInstruction *target, \
56 : std::vector< ref<Expr> > &arguments)
57 : HANDLER(handleAbort);
58 : HANDLER(handleAssert);
59 : HANDLER(handleAssertFail);
60 : HANDLER(handleAssume);
61 : HANDLER(handleCalloc);
62 : HANDLER(handleCheckMemoryAccess);
63 : HANDLER(handleDefineFixedObject);
64 : HANDLER(handleDelete);
65 : HANDLER(handleDeleteArray);
66 : HANDLER(handleExit);
67 : HANDLER(handleAliasFunction);
68 : HANDLER(handleFree);
69 : HANDLER(handleGetErrno);
70 : HANDLER(handleGetObjSize);
71 : HANDLER(handleGetValue);
72 : HANDLER(handleIsSymbolic);
73 : HANDLER(handleMakeSymbolic);
74 : HANDLER(handleMalloc);
75 : HANDLER(handleMallocN);
76 : HANDLER(handleMarkGlobal);
77 : HANDLER(handleMerge);
78 : HANDLER(handleNew);
79 : HANDLER(handleNewArray);
80 : HANDLER(handlePreferCex);
81 : HANDLER(handlePrintExpr);
82 : HANDLER(handlePrintRange);
83 : HANDLER(handleRange);
84 : HANDLER(handleRealloc);
85 : HANDLER(handleReportError);
86 : HANDLER(handleRevirtObjects);
87 : HANDLER(handleSetForking);
88 : HANDLER(handleSilentExit);
89 : HANDLER(handleUnderConstrained);
90 : HANDLER(handleWarning);
91 : HANDLER(handleWarningOnce);
92 : #undef HANDLER
93 : };
94 : } // End klee namespace
95 :
96 : #endif
Generated: 2009-05-17 22:47 by zcov