about summary refs log tree commit diff homepage
AgeCommit message (Collapse)Author
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
2010-08-05Store CallInst and InvokeInst operands in a fixed order: function, arg0, ↵Peter Collingbourne
arg1, ... git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@110352 91177308-0d34-0410-b5e6-96231b3b80d8
2010-08-05Have getDirectCallTarget use CallSitePeter Collingbourne
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@110351 91177308-0d34-0410-b5e6-96231b3b80d8
2010-08-05Use CallSite in StatsTracker::computeReachableUncoveredPeter Collingbourne
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@110350 91177308-0d34-0410-b5e6-96231b3b80d8
2010-08-05Add support for Debug+Asserts configurationPeter Collingbourne
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@110349 91177308-0d34-0410-b5e6-96231b3b80d8
2010-08-05Call klee_error instead of klee_warning when we fail to open a file,Cristian Cadar
and inform users about the common file descriptor problem. Based on patch and discussion with Cristian Zamfir. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@110329 91177308-0d34-0410-b5e6-96231b3b80d8
2010-08-05Applied patch submitted by Stefan Bucur that fixes a memory corruptionCristian Cadar
bug in the internal version of MiniSAT. See http://llvm.org/bugs/show_bug.cgi?id=7677 for more details. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@110325 91177308-0d34-0410-b5e6-96231b3b80d8
2010-08-05Small fix to test case. Without -f, the test fails when 'make test'Cristian Cadar
is run a second time without running 'make clean' in-between. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@110321 91177308-0d34-0410-b5e6-96231b3b80d8
2010-07-31Update getting started page to recommend 2.7 instead of 2.6.Daniel Dunbar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@109941 91177308-0d34-0410-b5e6-96231b3b80d8
2010-07-15Update to match new 2.8 CallInst getOperand API.Daniel Dunbar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@108406 91177308-0d34-0410-b5e6-96231b3b80d8
2010-07-15Reduce variable shadowing.Daniel Dunbar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@108405 91177308-0d34-0410-b5e6-96231b3b80d8
2010-07-15Fix a -Wbool-conversion warning.Daniel Dunbar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@108404 91177308-0d34-0410-b5e6-96231b3b80d8
2010-07-15Fix some -Wmismatched-tags warnings.Daniel Dunbar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@108403 91177308-0d34-0410-b5e6-96231b3b80d8
2010-07-15Remove stray semicolons in class definitions.Daniel Dunbar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@108402 91177308-0d34-0410-b5e6-96231b3b80d8
2010-07-14Add option to use an external version of STPPeter Collingbourne
This patch adds a new configure option, --with-stp, which configures KLEE to use an external version of STP instead of the version in the source tree. It includes documentation referring users to the STP download location. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@108347 91177308-0d34-0410-b5e6-96231b3b80d8
2010-07-08Add support for InsertValue and ExtractValue instructionsPeter Collingbourne
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@107912 91177308-0d34-0410-b5e6-96231b3b80d8
2010-06-28Applied Stefan Bucur's patch fromCristian Cadar
http://llvm.org/bugs/show_bug.cgi?id=6690. The patch adds specialized versions of klee_get_value for different types, fixing the previous klee_get_value function that sometimes truncated 64bit parameters to 32bit. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@107006 91177308-0d34-0410-b5e6-96231b3b80d8
2010-06-28Fixed bug reported at:Cristian Cadar
http://llvm.org/bugs/show_bug.cgi?id=7515 Bug was caused by the different behavior of klee_range during KLEE execution vs. replay mode, for the case when start==end: during KLEE execution, klee_range returns start, while during replay it called klee_make_symbolic. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@107005 91177308-0d34-0410-b5e6-96231b3b80d8
2010-06-25Clarify that expression labels are globally scoped.Daniel Dunbar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@106817 91177308-0d34-0410-b5e6-96231b3b80d8
2010-06-24Remove llvm.dbg.value intrinsic new to LLVM 2.7Peter Collingbourne
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@106802 91177308-0d34-0410-b5e6-96231b3b80d8
2010-06-24Handle ConstantAggregateZero constantsPeter Collingbourne
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@106801 91177308-0d34-0410-b5e6-96231b3b80d8
2010-06-24Use LLVM's TargetData::getTypeSizeInBits to determine type bitwidth instead ↵Peter Collingbourne
of our own implementation git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@106800 91177308-0d34-0410-b5e6-96231b3b80d8
2010-06-24Implement klee_stack_trace functionPeter Collingbourne
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@106799 91177308-0d34-0410-b5e6-96231b3b80d8
2010-06-24Added ExecutionState::dumpStack function for inspecting the status of the stackPeter Collingbourne
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@106798 91177308-0d34-0410-b5e6-96231b3b80d8
2010-06-21Applied Stefan Bucur's patch that fixes a non-deterministic bug in theCristian Cadar
regression suite (see http://llvm.org/bugs/show_bug.cgi?id=7423) git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@106431 91177308-0d34-0410-b5e6-96231b3b80d8
2010-06-13Tweak webpage, and link to KLEE buildbot.Daniel Dunbar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@105926 91177308-0d34-0410-b5e6-96231b3b80d8
2010-05-24Removed unused use-query-log option, patch submitted by Peter Collingbourne.Cristian Cadar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@104487 91177308-0d34-0410-b5e6-96231b3b80d8
2010-05-03test commitCristian Zamfir
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@102898 91177308-0d34-0410-b5e6-96231b3b80d8
2010-05-02Added a link to a version of uclibc that compiles on x64. Thanks toCristian Cadar
Cristian Zamfir for sharing this version with everybody. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@102878 91177308-0d34-0410-b5e6-96231b3b80d8
2010-05-02Fix a Wformat warning.Daniel Dunbar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@102877 91177308-0d34-0410-b5e6-96231b3b80d8
2010-05-02Remove bogus const applied to return type.Daniel Dunbar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@102876 91177308-0d34-0410-b5e6-96231b3b80d8
2010-05-02Scatter -Wno-deprecated about to suppress warnings about ext/hash* uses, I don'tDaniel Dunbar
feel like fixing this the right way right now. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@102875 91177308-0d34-0410-b5e6-96231b3b80d8
2010-05-02Unbreak inline asm warning.Daniel Dunbar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@102874 91177308-0d34-0410-b5e6-96231b3b80d8
2010-05-02Add missing include of Config.h, which was causing LLVM version checks to beDaniel Dunbar
broken, and thus we were removing all dbg.stoppoint instructions from modules. This totally broke debug info with 2.6. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@102873 91177308-0d34-0410-b5e6-96231b3b80d8
2010-05-02Sketch support for running KLEE tests using 'lit'.Daniel Dunbar
- Not working yet. Also, ditch a bunch of unused substitution variables from the site.exp config file. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@102872 91177308-0d34-0410-b5e6-96231b3b80d8
2010-05-02Add a little hack for visualizing KLEE branching.Daniel Dunbar
- This consumes the treestream files produced with --write-paths or --write-sym-paths, and renders out the tree in a very ad-hoc funky way. Your mileage may vary! :) Example image: http://klee.llvm.org/data/treegraph_example.jpg Example movie: http://klee.llvm.org/data/treegraph_example.avi git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@102869 91177308-0d34-0410-b5e6-96231b3b80d8
2010-05-02Compile klee-libc with -D__NO_INLINE__, to prevent glibc from using inlineDaniel Dunbar
definitions of putchar and atoi. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@102868 91177308-0d34-0410-b5e6-96231b3b80d8
2010-05-02Fix some const cast warnings.Daniel Dunbar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@102867 91177308-0d34-0410-b5e6-96231b3b80d8
2010-04-29Fixed compilation of unit tests.Cristian Cadar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@102611 91177308-0d34-0410-b5e6-96231b3b80d8
2010-04-26Applied patch submitted by Peter Collingbourne: "Some parts of theCristian Cadar
KLEE source code do not conform to the C++ standard, specifically [basic.scope.local]. gcc accepts the code due to a bug [1] but some other compilers (e.g. those based on EDG, such as icc) do not. This patch fixes the code in question to conform to the standard. [1] http://gcc.gnu.org/bugzilla/show_bug.cgi?id=18770" git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@102328 91177308-0d34-0410-b5e6-96231b3b80d8
2010-04-22Added --stp-optimize-divides flag. Patch submitted by PeterCristian Cadar
Collingbourne: "This flag controls whether constant divides are optimized into add/shift/multiplies before passing to STP, and is set by default. In some circumstances the use of this optimisation can actually slow the solver down, so it is best to allow the user to disable it." git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@102069 91177308-0d34-0410-b5e6-96231b3b80d8
2010-04-22Applied patch submitted by Peter Collingbourne: "If either of theseCristian Cadar
values is 0, the overall STP timeout should be whichever of the two values is set, i.e. the maximum of the 2 values, rather than 0." git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@102058 91177308-0d34-0410-b5e6-96231b3b80d8
2010-04-19ktest-tool: Add --write-ints option, for printing 4-byte objects as integers.Daniel Dunbar
- Patch by Li Xuan Ji! git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@101774 91177308-0d34-0410-b5e6-96231b3b80d8
2010-04-05Fix some tests w/ objdir != srcdir.Daniel Dunbar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@100422 91177308-0d34-0410-b5e6-96231b3b80d8
2010-04-05Add long double support, patch by David Ramos.Daniel Dunbar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@100421 91177308-0d34-0410-b5e6-96231b3b80d8
2010-04-05Make sure to include config.h, for llvm version check.Daniel Dunbar
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@100398 91177308-0d34-0410-b5e6-96231b3b80d8