about summary refs log tree commit diff homepage
AgeCommit message (Collapse)Author
2011-09-27Changed Tutorial 1, which was causing confusion due to differences inCristian Cadar
LLVM code generation before and after LLVM 2.8. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@140602 91177308-0d34-0410-b5e6-96231b3b80d8
2011-09-02Applied patch from David Ramos that fixes a bug in minDistToUncoveredCristian Cadar
calculation: "Functions with a single instruction were erroneously treated as never returning. This propagated far, making many instructions unreachable according to this metric." git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@139045 91177308-0d34-0410-b5e6-96231b3b80d8
2011-09-02Update location of TargetSelect.h and TargetRegistry.h for LLVM 3.0+Peter Collingbourne
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@139026 91177308-0d34-0410-b5e6-96231b3b80d8
2011-08-22Added new publication from RWTH Aachen.Cristian Cadar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@138232 91177308-0d34-0410-b5e6-96231b3b80d8
2011-08-09Disable the LowerSetJmpPass on LLVM 3.0+Peter Collingbourne
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@137116 91177308-0d34-0410-b5e6-96231b3b80d8
2011-08-01Make the Executor capable of handling bitcasts of aliases, by rewriting thePeter Collingbourne
direct function call logic. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@136605 91177308-0d34-0410-b5e6-96231b3b80d8
2011-07-29Sign extend, rather than zero extend, narrow gep indicesPeter Collingbourne
For example, clang creates these for ++ and -- operations on pointers on 64-bit platforms. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@136474 91177308-0d34-0410-b5e6-96231b3b80d8
2011-07-28Added two publications from EPFL, fixed a typo. Cristian Cadar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@136350 91177308-0d34-0410-b5e6-96231b3b80d8
2011-07-26Added a link to the searchable archive created by David R.Cristian Cadar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@136104 91177308-0d34-0410-b5e6-96231b3b80d8
2011-07-24Applied patch by Leandro Sales that makes Kleaver compatible with theCristian Cadar
recent changes to array names. Modified FastCexSolver.pc to catch this issue. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@135896 91177308-0d34-0410-b5e6-96231b3b80d8
2011-07-24Added the CAV 2011 paper from Stanford.Cristian Cadar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@135895 91177308-0d34-0410-b5e6-96231b3b80d8
2011-07-24Improved installation instructions a bit, and changed theCristian Cadar
"officially supported" version of LLVM from 2.7 to 2.8. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@135894 91177308-0d34-0410-b5e6-96231b3b80d8
2011-07-21Add our EuroSys paper to the publications listPeter Collingbourne
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@135677 91177308-0d34-0410-b5e6-96231b3b80d8
2011-07-20Updates for LLVM 3.0. Based on changes by arrowdodger, thanks!Peter Collingbourne
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@135598 91177308-0d34-0410-b5e6-96231b3b80d8
2011-07-20Deprecate LLVM_VERSION_MAJOR and LLVM_VERSION_MINOR in favour ofPeter Collingbourne
version codes. This makes the preprocessor-based version tests more concise and less error prone. Also, fix the version tests in lib/Expr/Parser.cpp (immutable zext and trunc were introduced in LLVM 2.9); now 2.9 passes "make test". git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@135583 91177308-0d34-0410-b5e6-96231b3b80d8
2011-06-23When extracting path from debug info, use file name on its own if it begins ↵Peter Collingbourne
with '/' Clang has been observed to use an absolute path in the 'filename' field. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@133740 91177308-0d34-0410-b5e6-96231b3b80d8
2011-06-09Patch from Martin Nowack for LLVM 2.9Cristian Cadar
(http://llvm.org/bugs/show_bug.cgi?id=9595) git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@132787 91177308-0d34-0410-b5e6-96231b3b80d8
2011-06-09Patch from arrowdodger for fixing FreeBSD build..Cristian Cadar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@132786 91177308-0d34-0410-b5e6-96231b3b80d8
2011-05-26Added instructions from Philip Guo about trying out KLEE via CDE. Cristian Cadar
Added a menu on the Getting Started webpage. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@132142 91177308-0d34-0410-b5e6-96231b3b80d8
2011-05-25Name symbolic arrays using the 3rd argument to klee_make_symbolic,Peter Collingbourne
and make sure the name is unique. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@132054 91177308-0d34-0410-b5e6-96231b3b80d8
2011-05-18Add ConstantStruct support to Executor::evalConstantPeter Collingbourne
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@131586 91177308-0d34-0410-b5e6-96231b3b80d8
2011-05-18Maintain an equivalence set during comparison operationsPeter Collingbourne
This results in a significant speedup of certain comparisons involving large partially shared expression trees. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@131585 91177308-0d34-0410-b5e6-96231b3b80d8
2011-05-18Use local Makefile.rulesPeter Collingbourne
This patch changes the build system to use its own copy of Makefile.rules (taken from a recent svn snapshot). Also added a --with-llvm-build-mode flag and changed the default runtime library configuration to Release+Asserts. Makefile.rules was modified to support --with-llvm-build-mode and older versions of LLVM (tested 2.7 and 2.8). git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@131584 91177308-0d34-0410-b5e6-96231b3b80d8
2011-05-18Support for arbitrary sized types in ConstantExpr::fromMemoryPeter Collingbourne
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@131583 91177308-0d34-0410-b5e6-96231b3b80d8
2011-04-23Fixed bug reported by Li Xuan Ji and Ayrat Khalimov.Cristian Cadar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@130070 91177308-0d34-0410-b5e6-96231b3b80d8
2011-04-23Transformed the assert() checking for overlapping objects into a callCristian Cadar
to klee_error() to make sure the check is done even when assertions are disabled. This makes the AsmAddresses test pass with assertions disabled. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@130067 91177308-0d34-0410-b5e6-96231b3b80d8
2011-04-23Patch by arrowdodger ↵Cristian Cadar
(http://keeda.stanford.edu/pipermail/klee-dev/2011-April/000617.html) for compiling KLEE with the latest LLVM changes. Tested against LLVM 2.7 and 2.8. The AsmAddresses test fails in 2.8 unless assertions are explicitely enabled (--enable-assertions). git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@130065 91177308-0d34-0410-b5e6-96231b3b80d8
2011-04-22Add a note about the git mirrorPeter Collingbourne
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@129989 91177308-0d34-0410-b5e6-96231b3b80d8
2011-03-30Fixed bug in WeightedRandomSearcher (CoveringNew). Patch by DavidCristian Cadar
Ramos: "I found a nasty little bug that I'm guess dates back to removing all that foreach() syntactic sugar. It made stats::minDistToUncovered = 0 at all program points, rendering WeightedRandomSearcher (CoveringNew) pretty worthless." git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@128536 91177308-0d34-0410-b5e6-96231b3b80d8
2011-03-30Fixed some typos.Cristian Cadar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@128533 91177308-0d34-0410-b5e6-96231b3b80d8
2011-03-30Bug fix in STPBuilder. Patch submitted by David Ramos, thanks!Cristian Cadar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@128532 91177308-0d34-0410-b5e6-96231b3b80d8
2011-03-28Start sketching a list of open projects.Daniel Dunbar
Currently this is focused on things which are well understood, it is intended to be a place to start hacking on KLEE, not a list of research projects in symbolic execution. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@128407 91177308-0d34-0410-b5e6-96231b3b80d8
2010-12-11Added two more papers.Cristian Cadar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@121615 91177308-0d34-0410-b5e6-96231b3b80d8
2010-12-10Added a new KLEE-related paper, and fixed some typos.Cristian Cadar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@121480 91177308-0d34-0410-b5e6-96231b3b80d8
2010-12-09Added a webpage on KLEE-related publications.Cristian Cadar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@121429 91177308-0d34-0410-b5e6-96231b3b80d8
2010-12-09Moved maze example to the Tutorials page.Cristian Cadar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@121394 91177308-0d34-0410-b5e6-96231b3b80d8
2010-11-14On LLVM 2.9+, use TargetLowering::ExpandInlineAsm to expand asm codePeter Collingbourne
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@119046 91177308-0d34-0410-b5e6-96231b3b80d8
2010-10-28Add a link to a neat KLEE usage example.Daniel Dunbar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@117574 91177308-0d34-0410-b5e6-96231b3b80d8
2010-10-25Compile all C files in gnu89 mode. Needed to build runtime libraryPeter Collingbourne
using clang (gnu89 is the gcc default). git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@117319 91177308-0d34-0410-b5e6-96231b3b80d8
2010-10-22Use %llvmgxx to compile a .cpp filePeter Collingbourne
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@117118 91177308-0d34-0410-b5e6-96231b3b80d8
2010-10-22Disable loop index split pass for LLVM 2.9+Peter Collingbourne
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@117117 91177308-0d34-0410-b5e6-96231b3b80d8
2010-10-04Regenerate.Daniel Dunbar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@115542 91177308-0d34-0410-b5e6-96231b3b80d8
2010-10-04Fix the Release+Asserts build-type-overwrite logic,Dylan Noblesmith
and document it. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@115513 91177308-0d34-0410-b5e6-96231b3b80d8
2010-10-01Fix a build warning, patch by nobled!Daniel Dunbar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@115315 91177308-0d34-0410-b5e6-96231b3b80d8
2010-09-30Regenerate.Daniel Dunbar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@115197 91177308-0d34-0410-b5e6-96231b3b80d8
2010-09-30Tweak configure to deal with another LLVM "Release -> Release+Asserts" rename onDaniel Dunbar
TOT. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@115196 91177308-0d34-0410-b5e6-96231b3b80d8
2010-09-30Add missing include to make sure version macros are present.Daniel Dunbar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@115146 91177308-0d34-0410-b5e6-96231b3b80d8
2010-09-30Spell versioning macros correctly.Daniel Dunbar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@115140 91177308-0d34-0410-b5e6-96231b3b80d8
2010-09-30Update for spurious LLVM API changes.Daniel Dunbar
- God forbid we manage to keep an API stable for a single release cycle. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@115139 91177308-0d34-0410-b5e6-96231b3b80d8
2010-09-30Update for LLVM API changes, patch by nobled, in PR8232.Daniel Dunbar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@115138 91177308-0d34-0410-b5e6-96231b3b80d8