diff options
author | Andrea Mattavelli <andreamattavelli@gmail.com> | 2017-04-09 13:33:29 +0200 |
---|---|---|
committer | Dan Liew <delcypher@gmail.com> | 2017-04-09 22:15:21 +0100 |
commit | 28872c1a0cb8a8f6b835af67719b9cd9aba66d3f (patch) | |
tree | 8875de15f92a3d09836567d44df6b4335bc21b64 /lib/Core/Memory.h | |
parent | 23a6c27d2e1e2c69a64eefc217675267868604e7 (diff) | |
download | klee-28872c1a0cb8a8f6b835af67719b9cd9aba66d3f.tar.gz |
Removed unused variable 'fake_object' in MemoryObject
Diffstat (limited to 'lib/Core/Memory.h')
-rw-r--r-- | lib/Core/Memory.h | 3 |
1 files changed, 0 insertions, 3 deletions
diff --git a/lib/Core/Memory.h b/lib/Core/Memory.h index d08bfb0c..4e5c8734 100644 --- a/lib/Core/Memory.h +++ b/lib/Core/Memory.h @@ -50,8 +50,6 @@ public: mutable bool isGlobal; bool isFixed; - /// true if created by us. - bool fake_object; bool isUserSpecified; MemoryManager *parent; @@ -96,7 +94,6 @@ public: isLocal(_isLocal), isGlobal(_isGlobal), isFixed(_isFixed), - fake_object(false), isUserSpecified(false), parent(_parent), allocSite(_allocSite) { |