about summary refs log tree commit diff homepage
AgeCommit message (Collapse)Author
2016-06-10remove bitmasking shift amount in bvRightShiftHoang M. Le
2016-06-10remove bitmasking shift amount in bvLeftShiftHoang M. Le
2016-06-10handle special cases of sdiv 1 and -1Hoang M. Le
2016-06-10rename the configure option --with-metasmt-default-solver to ↵Hoang M. Le
--with-metasmt-default-backend and improve the associated CXX flag
2016-06-10Use travis_wait to allow long running testsHoang
2016-06-10add entries for metaSMT with btor/stp/z3 in Travis CIHoang M. Le
2016-06-10use default metaSMT solver as defined in configurationHoang M. Le
2016-06-10add --with-metasmt-default-solver option to configureHoang M. Le
2016-06-10add metaSMT to travisHoang
2016-06-10update Makefile for metaSMTHoang M. Le
2016-06-10metaSMT does not require RTTIHoang M. Le
2016-06-10clean up metaSMT includesHoang M. Le
2016-06-04Merge pull request #412 from MartinNowack/fix_travisciMartinNowack
Fix Travis CI build - use alternative PPA for LLVM
2016-06-04Deactivate officiall llvm source. Use alternative ppaMartin Nowack
2016-06-04Do not install clang-3.4 if not neededMartin Nowack
2016-05-31Merge pull request #405 from ccadar/timesCristian Cadar
Fixed the stub for times() not to dereference a NULL pointer when cal…
2016-05-28Fixed an incorrect read() invocation and missing includes for FD_Fail2.cCristian Cadar
2016-05-27Merge pull request #396 from andreamattavelli/fix_kleaver_parserCristian Cadar
Fixed bug #375 in Kleaver's parser and added --clear-array-decls-after-query option to Kleaver.
2016-05-27Improved help message for POSIX environment options.Cristian Cadar
2016-05-27Merge pull request #397 from andreamattavelli/refactoring_stdinCristian Cadar
Distinct options for symbolic files and symbolic stdin
2016-05-27Fixed the stub for times() not to dereference a NULL pointer when call with ↵Cristian Cadar
a NULL argument. In respose of issue https://github.com/klee/klee/issues/399
2016-05-25Merge pull request #398 from hoangmle/masterMartinNowack
fix a compile error, add a travis matrix entry for Z3 & LLVM-2.9
2016-05-25add entry for llvm-2.9 and z3Hoang M. Le
2016-05-25add include in Z3Solver.cpp (did not compile with llvm-2.9)Hoang M. Le
2016-05-24Split creation of symbolic files and stdin in two distinct optionsAndrea Mattavelli
2016-05-24Fixed bug #375 in Kleaver's parserAndrea Mattavelli
2016-05-24Merge pull request #386 from ShayDamir/relocatable-kleeMartinNowack
Allow relocation of installed klee tree
2016-05-20Allow relocation of installed klee treeDamir Shaykhutdinov
If klee is configured with certain bindir and runtime dir, allow klee to be relocated, as long as subdirectory structure remains intact. For example, if klee is configured with bindir /usr/bin, and with runtime dir /usr/lib/klee, but is relocated to certain directory $RDIR, then running $RDIR/usr/bin/klee will search for runtime libraries in $RDIR/usr/lib/klee. Klee will use global runtime directory only when installed to global binary directory. Inspired by relocation code in gcc.
2016-05-18Merge pull request #387 from andreamattavelli/feat_instruction_loggingMartinNowack
Modified -debug-print-instructions to write directly on log file.
2016-05-18Modified -debug-print-instructions to allow to write directly on log file.Andrea Mattavelli
The option now contains 4 different options: 1) all:stderr, which logs all instructions to file in format [src, inst_id, llvm_inst]; 2) src:stderr, which logs all instructions to file in format [src, inst_id]; 3) compact:stderr, which logs all instructions to file in format [inst_id]; 4) all:file, which logs all instructions to file in format [src, inst_id, llvm_inst]; 5) src:file, which logs all instructions to file in format [src, inst_id]; 6) compact:file, which logs all instructions to file in format [inst_id]; Writing to file gives a speedup of ~50x.
2016-05-17Merge pull request #392 from MartinNowack/fix_docker_stpMartinNowack
Add newer cmake 2.8.11 from external ppa repository
2016-05-16Add cmake 2.8.11 as additional dependencyMartin Nowack
2016-04-19Merge pull request #369 from MartinNowack/fix_determ_solver_arrayMartinNowack
Generate unique STP and Z3 array names deterministically
2016-04-18Merge pull request #374 from Justme0/optimize_kinstiteratorMartinNowack
remove synthesized `rule of three` of KInstIterator
2016-04-17Merge pull request #359 from delcypher/fix_indep_solver_bugCristian Cadar
Bug fix in IndependentSolver
2016-04-14This test passes under 2.9, so it cannot be used as an XFAIL. We can enable ↵Cristian Cadar
it after the division bug is fixed.
2016-04-14Disabling --solver-optimize-divides by default, as the optimization is ↵Cristian Cadar
currently buggy, and we keep hitting this bug... See https://github.com/klee/klee/issues/334 for details.
2016-04-14Added test case with the examples from ↵Cristian Cadar
https://github.com/klee/klee/issues/334, which triggers a bug in solver-optimize-divides, and which is for now expected to fail.
2016-04-12remove synthesized `rule of three` of KInstIteratorjiangg
2016-04-12Merge pull request #364 from MartinNowack/feat_partial_loggingCristian Cadar
Partial logging of queries
2016-04-11Merge pull request #371 from andreamattavelli/masterCristian Cadar
Small refactoring to improve the consistency of info file handling
2016-04-11Small refactoring to improve the consistency of info file handlingAndrea Mattavelli
2016-04-09Generate unique STP and Z3 array names deterministicallyMartin Nowack
2016-04-08Merge pull request #370 from delcypher/fix_tautlogical_is_localCristian Cadar
Remove computation of ``isLocal`` that is always true when handling
2016-04-08Remove computation of ``isLocal`` that is always true when handlingDan Liew
AllocaInst.
2016-04-08Merge pull request #368 from delcypher/refactor_klee_out_file_to_ktestDan Liew
Refactor use of the name "outFile" to "KTest"
2016-04-08Rename KLEE command line options fromDan Liew
* ``-replay-out`` to ``-replay-ktest-file`` * ``-replay-out-dir`` to ``-replay-ktest-dir`` and also rename * help descriptions * global variables corresponding to these options. * Names used in ``KleeHandler``, ``Interpreter``, ``Executor`` and in KLEE's ``main()`` function. The old name for the options/code was very unhelpful as it wasn't obvious that "out" files are ``.ktest`` files unless you examine KLEE's source code.
2016-04-08Remove dead function declarationDan Liew
2016-03-31Updated NEWS file with 1.2.0 changesCristian Cadar
2016-03-31Moving to version 1.2.0Cristian Cadar
generated by cgit-pink 1.4.1 (git 2.36.1) at 2025-02-23 00:52:22 +0000