about summary refs log tree commit diff homepage
AgeCommit message (Collapse)Author
2016-06-30Dockerfile: link binaries to /usr/binDomenico Fabio Marino
Signed-off-by: Domenico Fabio Marino <dfm114@ic.ac.uk>
2016-06-28Merge pull request #417 from hoangmle/fix_constructSDIvByConstant_metaSMTMartinNowack
Fix #416
2016-06-28add assertions to check the pre-condition of bvVar*Shift that both operands ↵Hoang M. Le
have the same bv width
2016-06-27change bitwidth of expr_shpost in MetaSMTBuilder::constructSDivByConstant to ↵Hoang M. Le
64, so that the first two arguments of the call bvVarRightShift(extend_npm, expr_shpost, 64) have the same bitwidth of 64.
2016-06-24Merge pull request #394 from andreamattavelli/refactoring_runindirCristian Cadar
Added error message for -run-in directory errors
2016-06-23Merge pull request #415 from andreamattavelli/termination_infoCristian Cadar
Use klee_message for timeout information
2016-06-23Merge pull request #409 from hoangmle/fix_metaSMTCristian Cadar
Add metaSMT to Travis CI, fix metaSMTBuilder to pass all tests
2016-06-23Use klee_message for timeout informationAndrea Mattavelli
2016-06-10apply clang-formatHoang M. Le
2016-06-10remove now unused getShiftBits()Hoang M. Le
2016-06-10remove bitmasking shift amount in bvVarArithRightShiftHoang M. Le
2016-06-10remove bitmasking shift amount in bvVarRightShiftHoang M. Le
2016-06-10remove bitmasking shift amount in bvVarLeftShiftHoang M. Le
2016-06-10remove bitmasking shift amount in constructAShrByConstant and make it return ↵Hoang M. Le
0 when overshifting
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-24Added string for -run-in directory errorsAndrea 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
generated by cgit-pink 1.4.1 (git 2.36.1) at 2024-11-29 04:03:28 +0000