[klee-dev] Bug?

2012-01-18 Thread Paul Thomson
Searcher.cpp: std::setExecutionState*::const_iterator it2 = pausedStates.find(es); if (it2 != pausedStates.end()) { pausedStates.erase(it); Last line should refer to it2, not it? Thanks, Paul ___ klee-dev mailing list

[klee-dev] PATCH: Support for bitcasted aliased calls

2012-01-18 Thread Stefan Bucur
Hi, I'm submitting a patch that adds support in the KLEE executor for handling bitcasted aliased calls, which are valid LLVM constructs that might be encountered from time to time. Stefan = diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp index

Re: [klee-dev] PATCH: Bug fix for invalid offsets when getelementptr takes negative indices

2012-01-18 Thread Peter Collingbourne
On Wed, Jan 18, 2012 at 02:38:31AM +0100, Stefan Bucur wrote: Hi, Below is a patch that addresses an issue that would cause Klee to incorrectly execute a getelementptr instruction that contains negative offsets. I presume this situation has not been encountered too much before, but it

Re: [klee-dev] PATCH: Support for bitcasted aliased calls

2012-01-18 Thread Peter Collingbourne
On Wed, Jan 18, 2012 at 02:46:27AM +0100, Stefan Bucur wrote: Hi, I'm submitting a patch that adds support in the KLEE executor for handling bitcasted aliased calls, which are valid LLVM constructs that might be encountered from time to time. Hi Stefan, Likewise, I made a very similar

Re: [klee-dev] PATCH: Bug fix for invalid offsets when getelementptr takes negative indices

2012-01-18 Thread Stefan Bucur
On Wed, Jan 18, 2012 at 7:13 PM, Peter Collingbourne pe...@pcc.me.ukwrote: On Wed, Jan 18, 2012 at 02:38:31AM +0100, Stefan Bucur wrote: Hi, Below is a patch that addresses an issue that would cause Klee to incorrectly execute a getelementptr instruction that contains negative offsets.

Re: [klee-dev] memory leak patch

2012-01-18 Thread Cristian Cadar
On 11/20/2011 10:33 AM, Gang Hu wrote: The memory leak is caused by two reasons. First, the MemoryObject objects are not freed, until the MemoryManager is destroyed. Second, when KLEE allocates a non-fixed MemoryObject object, KLEE also allocates a block of memory which is the same as the