| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
- Mostly fixed by removing unnecessary references.
|
|
|
|
|
|
|
|
For LLVM >= 3.5 explicitly force this to be enabled otherwise we can't
compile against LLVM.
- Some minor tweaks to the configure logic by me (Daniel Dunbar), to ensure C++
compiler is tested before these checks run, and to properly restore CXXFLAGS.
|
|
- KCachegrind appears to expect the first function name to be preceeded by the
name of the file it appears in. Otherwise, it will end up creating two
different records for the function, one of which has no file name and won't
have any statistics.
|
|
- This makes KCachegrind output look nicer, as otherwise it assumes
instructions without debug info were inlined and shows some message to that
effect.
- This does however we might be lying a bit about the source line that an
instruction came from.
- This also adds a test case for our istats output, yay!
|
|
- This works fine for me on OS X now, and has been reported to work on Linux as
well. Enabling across the board although presumably Travis will still only
run single-threaded.
- Fixes #147.
|
|
- I suspect no one is using this feature, and I'm not sure it is well conceived
either. Ripping it out for now in lieu of bothering to maintain it.
|
|
- If this is a problem for some reason, lets either fix the problem or move it
into Runtime tests.
|
|
Fix testcase FD_Fail2.c
|
|
|
|
Major issue was that puts was used for the succeed printf calls.
With newer gcc/clang versions, printf is always used.
The former took different code paths leading to much more possibilities
to trigger failed writes and therefore generating more test cases.
This patch avoids the generation of puts.
And checks for the 4 possible generated test cases for 2 possible errors.
|
|
|
|
prevents the hang we are seeing.
|
|
|
|
already dependent on it.
|
|
|
|
work)
|
|
FloatingPointOps.ll).
|
|
- You can now make tests disabled, or expected to fail, by writing something like:
// XFAIL: llvm-3.4
or
// REQUIRES: not-llvm-3.4
- This mechanism doesn't support version comparisons, it is mostly intended to
help with switching over to new LLVM versions and incrementally working
through the test failures.
|
|
- LLVM changed the exception handling semantics a lot, and we can't write
compatible tests across the versions. Unfortunately I am afraid this probably
also means KLEE's exception handling semantics are broken for LLVM 3.4+, but
our C++ support is spotty at best. These tests should probably be replaced
with ones in a source language that supports exceptions if and when someone
wants to make that work.
|
|
|
|
- See comment, this is a gross workaround for Darwin's very small default limit
on shared memory size. I'm not sure how big of a counterexample users can
actually expect STP to solve in practice -- if there is a practical use for
larger ones it would probably be good for us to write a fallback strategy.
|
|
not asserts.
|
|
|
|
|
|
|
|
|
|
- This allows us to build in +Asserts mode even when LLVM isn't (by disabling
the checks in that mode).
- Eventually it would be nice to just move off of LLVM's DEBUG infrastructure
entirely and just have our own copy, but this works for now.
- Fixes #150.
|
|
Add TravisCI testing.
- Needs various cleanups, but merging now so we can enable for the primary repository and continue iteration there.
|
|
Some additional cleaning in test/Makefile
|
|
|
|
|
|
|
|
|
|
unsupported floating point widths.
|
|
- The change in 6829fb9 caused us to not allocation InstructionInfo objects for
instructions without source-level debug info, however, that means that all
such instructions end up sharing the one dummy InstructionInfo object, which
really breaks statistics tracking.
- This commit basically reverts that change, and also changes the code so we
don't ever use the dummy InstructionInfo object for instructions, so that
this problem can't be hit in other ways (e.g., if someone modifies the module
after the InstructionInfoTable construction). There is a FIXME for checking
the same thing for functions.
- Fixes #144.
|
|
- This ensures any stray klee-last files won't be picked up by my check to
prevent people from adding tests that don't use --output-dir.
|
|
which the LLVM JIT can't handle.
|
|
|
|
path.
- Otherwise this test takes a long time just hammering on the allocator trying
to get to the memory limit.
|
|
- This one test was taking about half the test time, and it definitely isn't
worth that much value as a test. We probably should have some kind of long
running tests infrastructure for things where we actually want to test KLEE
on real programs.
|
|
parallel.
- It would be nice if there was an easier way to do this that didn't involve
editing all of the tests (like running each test in its own directory), but
this approach fixes #146 and doesn't involve changing 'lit' or writing a
wrapper harness. My assumption is a lot of tests start are derived from
another one, so hopefully following this convention won't be burdensome, and
I updated 'make check' so that it will produce an error if any test runs klee
without --output-dir (by checking for the existing of klee-last files).
- This also helps with #147 but I still can't fully run tests in parallel (I
start hitting STP errors).
|
|
|
|
|
|
|
|
Fixes #96.
|
