1. 10 Nov, 2013 1 commit
  2. 24 Oct, 2013 4 commits
  3. 22 Oct, 2013 1 commit
  4. 21 Oct, 2013 1 commit
  5. 16 Oct, 2013 4 commits
  6. 15 Oct, 2013 2 commits
  7. 12 Oct, 2013 1 commit
  8. 08 Oct, 2013 1 commit
  9. 06 Oct, 2013 1 commit
  10. 04 Oct, 2013 1 commit
  11. 03 Sep, 2013 4 commits
    • Cristian Cadar's avatar
      Forgot to remove the actual stp directory. · 4d1dc5d4
      Cristian Cadar authored and Daniel Liew's avatar Daniel Liew committed
      git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@161056 91177308-0d34-0410-b5e6-96231b3b80d8
    • Daniel Liew's avatar
      Implemented runtime check for overshift (controllable with --check-overshift · a98690d5
      Daniel Liew authored
      command line argument).
      Overshift is where a Shl, AShr or LShr has a shift width greater
      than the bit width of the first operand. This is undefined behaviour
      in LLVM so we report this as an error.
    • Daniel Liew's avatar
      Fixed bug where divide by zero bugs would only be detected once in a program · 5e679697
      Daniel Liew authored
      even if there were many divide by zero bugs.
      The fix basically inlines all function calls to klee_div_zero_check()
      so that each call to klee_report_error() is a unique instruction
      for each instrumentation of a divide operation.
      It also seems that inlining the call "magically" fixed the debug information
      (file and line number) of the instruction so that the debug information on the
      inlined instructions matches that of the instrumented division instruction.
      Note that the command line option -emit-all-errors could be used to
      workaround the bug fixed in this commit.
    • Dan Liew's avatar
      Modified the buildmode of bitcode libraries. · e2201d62
      Dan Liew authored and Daniel Liew's avatar Daniel Liew committed
      The Default is Release+Asserts but if you are building KLEE with debug symbols (for example
      "Release+Debug+Asserts" or "Debug+Asserts") then this breaks because KLEE will
      look for the bitcode libraries in the wrong place because the
      RUNTIME_CONFIGURATION macro is not defined to be what KLEE actually builds as.
      This has been tweaked so that when we build the bitcode libraries the Makefile
      variable "DEBUG_SYMBOLS" is correctly overridden.
  12. 28 Aug, 2013 1 commit
  13. 23 Aug, 2013 7 commits
  14. 22 Aug, 2013 7 commits
  15. 16 Aug, 2013 4 commits