about summary refs log tree commit diff homepage
AgeCommit message (Collapse)Author
2016-07-08Handle aligned varargs allignment correctlyMartin Nowack
For vararg handling, arguments of size bigger than 64 bit need to be handled 128bit aligned according to AMD calling conventions AMD64-ABI 3.5.7p5. To handle that case correctly, we do: 1) make sure that every argument is aligned correctly in an allocation for function arguments 2) the allocation itself is aligned correctly
2016-07-08Merge pull request #362 from MartinNowack/feat_determ_state_selectionMartinNowack
Deterministic state addition and removing
2016-07-08Generate forked states for switch instructions deterministicallyMartin Nowack
This patch generates the states based on the order of switch-cases. Before, switch-constraints were randomly assigned to forked states. As generated code might be different between LLVM versions, we use the case values, order them, and iterate in that order over the cases. This way we can also support deterministic execution of older LLVM versions.
2016-07-08Use vector instead of set to add/remove statesMartin Nowack
Deterministic adding/removing of states.
2016-07-08IterativeDeepeningTimeSearcher: Fix using wrong iteratorMartin Nowack
2016-07-08Refactoring: Extract method to dump remaining statesMartin Nowack
2016-07-08Merge pull request #391 from MartinNowack/feat_zipstream_compressMartinNowack
Support gzip-based compression of raw_outstreams
2016-07-08Merge pull request #410 from MartinNowack/feat_log_after_stepsMartinNowack
Add options to dump istats and stats statistics every n instructions.
2016-07-08Support gzip-based compression of raw_outstreamsMartin Nowack
Provide initial zlib-based compression support for raw_outstreams. Replacing llvm::raw_fd_outstreams with compressed_fd_outstreams automatically compresses data in gzip format before writing to file. Options added: * --compress-log to compress all query log files (e.g. *.pc, *.smt2) on the fly. Every query log file gets extended with .gz. * --debug-compress-instructions to compress logfile for instruction stream on the fly.
2016-07-08Add feature to dump statistics after n instructionsMartin Nowack
Add -stats-write-after-instructions and -istats-write-after-instructions to update each statistic after n steps. Furthermore, the metric "minimal distance to uncovered state" is now updated independently if statistics are enabled or not. This metric is needed i.e. by weighted random searchers directed towards uncovered instructions. Remove some dead code.
2016-06-30Merge pull request #424 from helicopter88/masterMartinNowack
Dockerfile: link binaries to /usr/bin
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
generated by cgit-pink 1.4.1 (git 2.36.1) at 2025-02-18 09:11:12 +0000