1. 15 Oct, 2013 2 commits
  2. 12 Oct, 2013 1 commit
  3. 08 Oct, 2013 1 commit
  4. 06 Oct, 2013 1 commit
  5. 04 Oct, 2013 1 commit
  6. 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
      4d1dc5d4
    • 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.
      
      Conflicts:
      
      	lib/Module/KModule.cpp
      	tools/klee/main.cpp
      a98690d5
    • 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.
      5e679697
    • 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.
      
      Conflicts:
      
      	Makefile.config.in
      e2201d62
  7. 28 Aug, 2013 1 commit
  8. 23 Aug, 2013 7 commits
  9. 22 Aug, 2013 7 commits
  10. 16 Aug, 2013 5 commits
  11. 18 Mar, 2013 1 commit
    • Dan Liew's avatar
      Modified the buildmode of bitcode libraries. · 4556faa3
      Dan Liew authored
      The Default is Release+Asserts but if you are building for example "Release+Debug+Asserts" then this break 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 as "Release+Asserts" whether or not we've
      choosen debug for the main build of KLEE does not matter.
      4556faa3
  12. 11 Mar, 2013 6 commits
  13. 09 Apr, 2012 3 commits