| Age | Commit message (Collapse) | Author |
|---|
|
|
|
[CMake] Remove `ENABLE_TESTS` CMake cache option.
|
|
The intention of this option was to provide a switch that can be
used to globally enable/disable tests.
This option ended up causing a lot of confusion as can be seen
on the discussion on writing documention for the new build system.
https://github.com/klee/klee.github.io/pull/53
So it was decided to remove this option. This fixes #568 .
|
|
[CMake] Rename "integrationtests" to "systemtests", removed some undocumented targets and other build changes
|
|
disallow using reserved target names.
|
|
Surprisingly the old code still worked even when the target didn't
exist.
|
|
targets from Autoconf/Makefile build system. Having these around
just confuses things.
|
|
* lit tests are run by the `systemtests` target
* The `check` target runs the `systemtests` and `unittests` target
This make its target names consistent with the CMake build system.
|
|
This was a proposal from #500.
@andreamattavelli pointed out that the lit tests are really
system tests rather than integration tests so this commit fixes
the inappropriate naming that I chose.
|
|
Fixes and testing for libkleeRuntest
|
|
Previously error messages would be emitted but execution would continue
which might not be desirable.
Now a wrapper function (for fprintf) `report_internal_error()` is used
which will cause the program to exit. The older behaviour of continuing
to execute after an error can be achieved by setting a new environment
variable `KLEE_RUN_TEST_ERRORS_NON_FATAL`.
This commit also adds a test for each error case.
|
|
If KLEE generates ktest files with `--posix-runtime` then if replaying
using libkleeRuntest then replay would be incorrect because the
`model_version` object would be unintentionally used during replay.
For now just skip over that object and try the next one.
Also emit a warning if the object names don't match.
|
|
test is marked XFAIL because there is a bug in the implementation
of `libkleeRuntest`.
Quite a few changes had to be made to the lit configuration in
order to support these tests.
To run the tests I had to fix #480 for the autoconf/Makefile build
system otherwise the `libkleeRuntest` library would not be found
by the system linker at runtime.
|
|
Brings llvm-ar into line with llvm-as and lli, removing the assumption that
llvm-ar is installed system wide
|
|
1. It expects only 2 arguments, so if linking succeeds, nothing will happen (thanks to []),
otherwise the message "checking for new_bitvector() in -lmetaSMT" will appear.
The latter is that what we currently observe, which means linking actually failed.
2. The reason for linking failure is the use of "-lmetaSMT" in LDFLAGS.
AC_LINK_IFELSE does approximately the following: ${CXX} ... -lmetaSMT ${EXECUTABLE_NAME} ${LIBS},
which causes "libmetaSMT cannot be found" (at least on Ubuntu Xenial, where ${LIBS} = -lz).
After consulting https://www.gnu.org/software/autoconf/manual/autoconf-2.66/html_node/Running-the-Linker.html,
adding "-lmetaSMT" to ${LIBS} seems to be the correct solution.
|
|
|
|
|
|
macOS fixes
|
|
|
|
built with `-fvisibility-inlines-hidden`.
This was observed when using a bottled version of LLVM 3.4 on macOS
that appears to have been built with this option.
|
|
Fixes and clean ups in the TravisCI scripts
|
|
When trying to KLEE with a version of LLVM (specifically, 3.5) built from
Github (https://github.com/llvm-mirror/llvm/tree/release_35) the regex in
find_llvm.cmake failed to match the LLVM version string because it was suffixed
with "svn" - i.e. "3.5.2svn".
Added the optional "svn" suffix to the CMake regex to fix this.
|
|
to the root of the build tree after doing the hack the generate
the lit configuration files.
This will make it easier in the future to run more test configurations
(e.g. by passing options to lit to change KLEE's behaviour).
|
|
fast rather than continuing to run the tests (due to `set -e` at the
beginning of the script).
Although this gives less information in the event of a broken build
it means our builds might finish faster if they are broken and it
also simplifies the script significantly.
|
|
even though configure/build failed. This due to using the `&&` operator
which means failure of commands to execute in this compound statement
will not trigger the script to exit as requested by `set -e`.
|
|
Typo fix when compiling with LLVM 3.5 and above
|
|
Replaced an incorrect comma with a semicolon in the Executor constructor.
|
|
[CMake] Fix bug with enabling and then disabling TCMalloc support
|
|
and then re-configured with `ENABLE_TCMALLOC` set to OFF then
`klee/Config/config.h` was not correctly re-generated.
|
|
[CMake] Fix bugs in the Makefile bitcode build system
|
|
TravisCI config clean up
|
|
would not recompile if the `Makefile.cmake.bitcode.rules` file changed.
|
|
would not recompile if the LLVM C compiler flags changed. This could
happen if the user did something like
```
make -f Makefile.cmake.bitcode LLVMCC.ExtraFlags=-Wall
```
|
|
The main change here try to
* Avoid testing so many metaSMT configurtions
* Avoid testing so many build with STP's master branch
* Avoid testing so many builds that tests klee-uclibc's
`klee_0_9_29` branch.
* Avoid testing so many LLVM 2.9 builds given that it will
be deprecated soon.
* Remove coverage build. The server for receving this data
is dead.
This reduces 24 configurations to test down to just 14.
|
|
variables.
|
|
|
|
With the old buildsystem we could pass CFLAGS when building runtime
libs. Support passing some additional flags to cmake-based system too.
We need this to build 32 and 64bit runtime libs separately (but not
whole klee).
Signed-off-by: Jiri Slaby <jslaby@suse.cz>
|
|
Remove support for reporting the approximate git tag.
|
|
|
|
Moving to KLEE 1.3.0
|
|
This was confusing because it would emit something like
`v1.0.0-290-g08d4716` because the 1.1.0 and 1.2.0 releases
didn't have a tag on the master branch so `git describe --tags`
would just find the `v1.0.0` tag and report based on that tag.
|
|
|
|
|
|
Fixing current version of STP in Dockerfile (see #505) to 2.1.2
|
|
|
|
|
|
Fix Expr::compare
|
|
* Making `Expr::compre(const Expr&, ExprEquivSet)` private and moving
its implementation into `Expr.cpp`.
* Document `Expr::compare(const Expr&)`.
This partially addresses #515 .
|
|
and make it a pure virtual method. Also make it protected rather than
public because it is an implementation detail of `Expr::compare()`.
This means that sub classes must implement it so this commit also
provides implementations. The comparision behaves as before except
for `ConcatExpr` where its `width` attribute is now used (previously
it wasn't).
This commit also documents the semantics of `Expr::compareContents(const Expr&)`
which was clearly needed because it has been incorrectly implemented
in the past and has gone unnoticed for several years.
This partially addresses #515 .
|
|
`compareContents()`.
This bug would not have affected correctness but it would have
affected performance because if `Expr::compare()` was called on
two structually equal `NotExpr` then its children would be
checked for structually equality twice - once in
NotExpr::compareContents()` and once in `Expr::compare()`.
This partially addresses #515 .
|
