about summary refs log tree commit diff homepage
AgeCommit message (Collapse)Author
2014-12-03Merge pull request #182 from hpalikareva/fix-test-prefer-cexCristian Cadar
Fixed test /Feature/PreferCex.c: Z3 instantiates different value for unc...
2014-12-03Fixed test /Feature/PreferCex.c: Z3 instantiates different value for ↵Hristina Palikareva
unconstrained buf[3]
2014-12-02Unbreak compilation (in metaSMT configuration) by preventing the #defineHristina Palikareva
unordered_map and unordered_set from leaking out into other compilation units. This should be removed entirely when C++11 support lands.
2014-12-02Fix typoDan Liew
2014-12-02Add a comment explaining why the query expr is being negated.Dan Liew
2014-12-02The printing of constraints and the QueryExpr have been merged into aDan Liew
single method with two different implementations. There is one version of this method for human readability (printHumanReadableQuery()) and a version for machine consumption (printMachineReadableQuery()). The reason for having two versions is because different behaviour is needed in different scenarios * In machine readable mode the entire query is printed inside a single ``(assert ...)``. This is done to allow ``(let ...)`` to abbreviate as much as possible. * In human readable mode each constraint and query expression is printed inside its own ``(assert ...)`` unless the abbreviation mode is ABBR_LET in which case all constraints and query expr are printed inside a single ``(assert ...)`` much like in the machine readable mode Whilst I was here I also fixed a bug handling identation when printing ``(let ...)`` expressions in printAssert()
2014-12-02Implement :named and let abbreviation modes in ExprSMTLIBPrinterRaimondas Sasnauskas
* Set the default abbreviation mode to let (ExprSMTLIBPrinter::ABBR_LET) * Remove the now defunct ExprSMTLIBLetPrinter * Improve performance of ExprSMTLIBPrinter::scan() by keeping track of visited Expr to avoid visiting them again * Rename ExprSMTLIBPrinter::printQuery() to ExprSMTLIBPrinter::printQueryExpr()
2014-11-13Fix broken webpage link in README.mdDan Liew
2014-11-13Merge pull request #177 from jirislaby/destdirDan Liew
tools: prepend DESTDIR when installing
2014-11-13tools: prepend DESTDIR when installingJiri Slaby
Some tools prepend DESTDIR properly, some not. ktest-tool and klee-stats do not, so 'make install' chokes with an error: llvm[2]: Installing Release+Asserts /usr/bin/ktest-tool /usr/bin/install: cannot create regular file '/usr/bin/ktest-tool': Permission denied Signed-off-by: Jiri Slaby <jirislaby@gmail.com>
2014-11-02Merge pull request #174 from delcypher/allow_stp_installed_in_rootDan Liew
Allow stp installed in root
2014-11-01Upstream libstp is no longer dependent on Boost so remove theDan Liew
configure/Makefile code that adds Boost as a depdendency because We don't need to support old versions of STP that needed Boost.
2014-11-01configure: allow stp being installed in /Jiri Slaby
I have stp in standard paths: /usr/include and /usr/lib64. Allow that by correct STP_CFLAGS + STP_LDFLAGS instead of STP_ROOT. Those are empty when --with-stp is not passed. configure is regenerated by autoconf too. Signed-off-by: Jiri Slaby <jslaby@suse.cz>
2014-10-31Merge pull request #173 from delcypher/switch_to_autoconf_2.69Cristian Cadar
Switch to using autoconf 2.69 this version is more commonly available
2014-10-31Merge pull request #167 from ↵Dan Liew
willemp/willem/fix_64bit_printing_bug_in_testingUtils Fix 64bit printing bug in testing utils
2014-10-31Switch to using autoconf 2.69 this version is more commonly availableDan Liew
on Linux systems (2.60 is quite old) which will make updating the configure script easier for most users.
2014-10-16Fixed declaration of print_int that Travis complained aboutWillem
2014-10-16Fix the bug in printing 64bit numbers, set the test to expect passing. ↵Willem
Changed _testingUtils to use stdint.h
2014-10-15Fixed test/Concrete/ConstantExpr.llWillem
The difference between a 64bit pointer truncated to 32 bits and the original 64bit pointer would never be 0 if any of the high 32bits in the pointer were test. If lli and klee had a different value for the top 32bits of the address this test would be marked as failing. Due to the 64bit printing buf in _testingUtils this was not exposed before. The fix clears the top 32bits of the difference.
2014-10-15Added tests to _testingUtils.c (currently failing due to a bug in printing ↵Willem
64bit numbers) Fixing this bug will expose a failing test case for Concrete/ConstantExpr.ll
2014-10-09Add a hack for Travis so that llvm-gcc can build native executables.Dan Liew
This could be useful if KLEE tests want to use the bitcode compiler as a native compiler.
2014-10-09Merge pull request #166 from willemp/willem/klee_opts_to_concrete_testsCristian Cadar
Fixes support for passing arguments to klee in the ConcreteTests.
2014-10-08Fixes support for passing arguments to klee in the ConcreteTests.Willem
This is for use with llvm-lit --param=klee_opts=... Fixes lit.cfg to not have an extranous space behind the klee command. Augments ConcreteTest to accept and pass arguments to klee. Augments all the ConcreteTest cases to wrap %klee in quotes. Without wrapping %klee the extra arguments will be seens as arguments to ConcreteTest.py resulting in an unknown argument error.
2014-09-25Patch by Sean Bartell: "F_Binary was actually moved in LLVM 3.4 (r186447), ↵Cristian Cadar
not 3.0."
2014-09-19Removed code related to underConstrained, as it is unused (issue pointed out ↵Cristian Cadar
by @hpalikareva).
2014-09-17Fix segfault under LLVM3.5 . I forgot to release ownership of theDan Liew
MemoryBuffer from the std::unique_ptr when getLazyBitcodeModule() succesfully takes ownership.
2014-09-17Fix more LLVM3.5 compilation issues.Dan Liew
2014-09-17Compilation fix for LLVM3.5 caused by the removal of sys::fs::F_Binary.Dan Liew
The commit that caused this is r202052.
2014-09-17Another LLVM3.5 compilation fix.Dan Liew
2014-09-16[LLVM3.5] Update Kleaver for MemoryBuffer::getFileOrSTDIN changes.Daniel Dunbar
2014-09-16Fix #include under LLVM3.5. OwningPtr doesn't exist anymore.Dan Liew
2014-09-16Fix LLVM3.5 compilation a little more. ``Support/system_error.h``Dan Liew
was removed by r210803
2014-09-16Fix compilation error due to r199218. Maybe we should just remove thisDan Liew
assertion entirely?
2014-09-15Merge pull request #160 from MartinNowack/fix_dirconsistencyDaniel Dunbar
Generate fake files for test cases
2014-09-15Generate fake files for test casesMartin Nowack
2014-09-15Merge pull request #157 from MartinNowack/fix_posix_printoutCristian Cadar
Fix a possible deadlock.
2014-09-15Merge pull request #158 from delcypher/remove_response_filesCristian Cadar
Remove --read-args command line option because this feature has been
2014-09-15[Travis] Show commands as they execute inDan Liew
``install-llvm-and-runtime-compiler.sh``
2014-09-15Merge pull request #134 from delcypher/coloured_error_messagesDan Liew
Taught klee_warning(), klee_error() etc... to emit coloured text output.
2014-09-15Taught klee_warning(), klee_error() etc... to emit coloured text output.Dan Liew
Also use bold green text when KLEE finishes. This is done by taking advantage of llvm::raw_ostream's nice API for controlling the console text colour.
2014-09-15Remove --read-args command line option because this feature has beenDan Liew
available in LLVM's command line parser for a while (response files).
2014-09-15Removed inlineChecks() function which was just dead code.Dan Liew
2014-09-14[Travis] Stop building with both Clang and GCC for now, see comment.Daniel Dunbar
2014-09-15Merge pull request #154 from delcypher/travis_script_fixesDan Liew
Travis clean ups
2014-09-14[LLVM3.5] Ensure Twine definition is available from Executor.h.Daniel Dunbar
2014-09-14Fix LLVM3.5 compilation. This is due to r202168Dan Liew
2014-09-14[LLVM3.5] Drop use of PassNameParser, which we don't even use anymore.Daniel Dunbar
2014-09-14Fix LLVM3.5 compilation due to switching to std::error_codeDan Liew
2014-09-15Capture STP build output to file and only show its contents if thereDan Liew
is a build failure. This is so the output shown in the TravisCI web interface is kept small.
2014-09-14[LLVM3.5] Update for more random headers moving around.Daniel Dunbar
generated by cgit-pink 1.4.1 (git 2.36.1) at 2025-02-23 12:13:17 +0000