about summary refs log tree commit diff homepage
AgeCommit message (Collapse)Author
2016-11-03Merge pull request #491 from andreamattavelli/fix_raiseasm_macosMartinNowack
Support for Darwin platform in RaiseAsm pass
2016-11-03Adds support for Darwin platform in RaiseAsm passAndrea Mattavelli
2016-11-02Merge pull request #487 from hoangmle/masterCristian Cadar
Upgraded to boolector-2.2.0 and some cleanup and refactoring of the metaSMT support.
2016-10-27apply clang-formatHoang M. Le
2016-10-27update commentsHoang M. Le
2016-10-27upgrade to boolector-2.2.0 & remove the no longer needed aux array vectorHoang M. Le
2016-10-26move the query creation part into runAndGetCex() (to be consistent with ↵Hoang M. Le
runAndGetCexForked())
2016-10-26change signature of runAndGetCex() to match runAndGetCexForked()Hoang M. Le
2016-10-26remove outdated FIXME (metaSMT-Z3 implements assumption via push/pop)Hoang M. Le
2016-10-18Merge pull request #484 from delcypher/fix_misleading_indentationCristian Cadar
Fix `-Wmisleading-indentation` warning and also correctly set the `dirty` flag
2016-10-18Fix `-Wmisleading-indentation` warning and also correctly set theDan Liew
`dirty` flag if we remove `llvm.trap` from the module.
2016-10-14Use newer trusty-based Travis CI (#452)MartinNowack
2016-10-02Merge pull request #475 from delcypher/klee_fix_asanCristian Cadar
Don't build KLEE's runtime with any sanitizers.
2016-10-01Merge pull request #426 from hoangmle/metaSMT_remove_ITE_chain_for_shiftMartinNowack
remove mimic_stp option and the associated ITE chain construction for variable shift operations
2016-09-29When building KLEE with the sanitizers make sure the runtime is notDan Liew
built with them because KLEE can't handle this.
2016-09-29Fix bug in `AssignmentEvaluator` where NotOptimizedExpr would not (#466)Dan Liew
* Add unittest to check that the `Assignment` class can evaluate expressions containing a `NotOptimizedExpr`. * Fix the `AssignmentTest.FoldNotOptimized` unit test by teaching the `ExprEvaluator` to fold `NotOptimizedExpr` nodes.
2016-09-29Merge pull request #474 from jirislaby/timestampCristian Cadar
configure: add option to enable timestamping and disabled it by default
2016-09-29remove mimic_stp option and the associated ITE chain construction for shift ↵Hoang M. Le
operators
2016-09-29configure: run AutoRegen.shJiri Slaby
The previous change altered .ac files, regenerate the scripts. Signed-off-by: Jiri Slaby <jslaby@suse.cz>
2016-09-29configure: add option to enable timestampingJiri Slaby
It is pain for build systems to see __DATE__ or __TIME__ in sources as the build is not reproducible. So disable the timestamping by default and add an option to enable it if somebody is really after it. Signed-off-by: Jiri Slaby <jslaby@suse.cz>
2016-09-29Merge pull request #471 from domainexpert/argv-argAndrea Mattavelli
Fixed the description of -posix-runtime option
2016-09-29Fixed the description of -posix-runtime optionAndrew Santosa
In the description, --sym-argv and --sym-argvs should have instead been --sym-arg and --sym-args
2016-09-26Merge pull request #444 from andreamattavelli/refactor_warningsMartinNowack
Refactoring logging information
2016-09-26Modified logging information to steer the usage of klee_message, ↵Andrea Mattavelli
klee_warning, and klee_error
2016-09-20Merge pull request #443 from MartinNowack/feat_assembler_raisingCristian Cadar
Extended support for assembler raising
2016-09-16Avoid internalization of non-standard entry point (i.e. not the main ↵Andrea Mattavelli
function) (#455)
2016-09-15Merge pull request #372 from delcypher/stp_z3_crosscheckDan Liew
Allow cross checking of solvers
2016-09-15Rename `-debug-cross-check-core-solver` option toDan Liew
`-debug-crosscheck-core-solver` as requested by Cristian
2016-09-15Correct out of date comments for some of the klee error handlingDan Liew
functions.
2016-09-15Add ``-debug-cross-check-core-solver`` option to allow cross-checkingDan Liew
with another solver. For example the core solver can be STP and the cross checking solver can be Z3. Unfortunately a few fragile tests don't pass when actually using this option.
2016-09-15Clang-format ``ConstructSolverChain.cpp``Dan Liew
2016-09-15Check the existence of the entry point during the initialization of the ↵Andrea Mattavelli
POSIX runtime. If the check fails, exit with an error. (#457)
2016-09-02Merge pull request #463 from delcypher/fix_gtest_buildDan Liew
Try to unbreak the TravisCI and Docker builds.
2016-09-01Try to unbreak the TravisCI and Docker builds.Dan Liew
GTest has moved from googlecode to GitHub so update URL and directory name used in source archive as appropriate.
2016-08-19Merge pull request #453 from andreamattavelli/fix_save_writes_docCristian Cadar
Document -save-all-writes to klee_init_env help message
2016-08-19Added -save-all-writes to klee_init_env help messageAndrea Mattavelli
2016-08-19Merge pull request #462 from giacomoguerci/masterCristian Cadar
[Klee Web] Link libkleeRuntest library to fix coverage report
2016-08-16[Klee Web] Link libkleeRuntest library to fix coverage reportGiacomo Guerci
2016-08-10Extended support for assembler raisingMartin Nowack
Improved support for assembler handling. Providing additional triple information to raise assembler for supported architectures only. Implemented support for raising full assembly memory fence. Added initial support for memory fences in Executor.
2016-08-10Merge pull request #451 from andreamattavelli/fix_ub_ptreeMartinNowack
Fix to PTree pointer use-after-delete
2016-08-09Fix to PTree pointer use-after-delete undefined behaviorAndrea Mattavelli
2016-08-08Merge pull request #447 from hutoTUM/fix-klee_get_obj_sizeMartinNowack
Fix for klee_get_obj_size() crashing on 64-bit, resolves #446
2016-08-08Fix for klee_get_obj_size() crashing on 64-bit, resolves #446hutoTUM
2016-08-08Merge pull request #450 from andreamattavelli/fix_to_strerrorCristian Cadar
Fix to #449 by using sys::StrError(errno) to print error messages.
2016-08-08Use LLVM-based functions to print errnoAndrea Mattavelli
2016-08-06Merge pull request #448 from andreamattavelli/fix_query_compressionMartinNowack
Fix to #445
2016-08-06Fix to #445Andrea Mattavelli
2016-08-04Merge pull request #441 from jirislaby/exit-on-error-typeCristian Cadar
add --exit-on-error-type option
2016-08-04klee: add exit-on-error-type parameterJiri Slaby
It allows stopping the execution on some conditions like assertions. The use is like: klee -exit-on-error-type=Assert -exit-on-error-type=External file.llvm This is especially useful in the SV-COMP. A test to cover the new parameter was added too. Signed-off-by: Jiri Slaby <jslaby@suse.cz>
2016-08-03Merge pull request #439 from jirislaby/fprintfCristian Cadar
fprintf: convert to klee_warning
generated by cgit-pink 1.4.1 (git 2.36.1) at 2024-11-26 05:18:35 +0000