| Age | Commit message (Collapse) | Author |
|---|
|
to clean the runtime build.
Unfortuantely there is no way to have the `clean` target trigger the
`clean_runtime` target unfortunately.
|
|
`ExternalProject_Add_Step()` so that when using Ninja the output of the
bitcode build system is shown immediately.
|
|
This fixes a bug in the bitcode build system where the build would
fail if the build directory was a symbolic link (i.e. create a symbolic
link for the root of the build tree and try to do the build in that
directory).
The problem was that `DIR_SUFFIX` implicitly assumed that there was
only one way to refer to the build tree which is an incorrect assumption
in the presence of symbolic links. This has been fixed by using the
`$(realpath)` GNU make built in to resolve all symbolic links.
An additional sanity check has been added to check that `SRC_DIR`
exists.
|
|
It looks like older LLVM versions that were built from SVN/git didn't
have a patch version number (i.e. `3.4svn` rather than `3.4.0svn`).
|
|
the `cmake` directory breaks KLEE's CMake build.
Just copy across the STP library for now. This really sucks.
The script needs to do a better job of installing MetaSMT and
its dependencies.
For reference here's the error.
```
CMake Error at /usr/lib/cmake/STP/STPTargets.cmake:67 (message):
The imported target "stp_simple" references the file
"/usr/bin/stp_simple"
but this file does not exist. Possible reasons include:
* The file was deleted, renamed, or moved to another location.
* An install or uninstall procedure did not complete successfully.
* The installation package was faulty and contained
"/usr/lib/cmake/STP/STPTargets.cmake"
but not all the files it references.
Call Stack (most recent call first):
/usr/lib/cmake/STP/STPConfig.cmake:15 (include)
/home/travis/build/klee/build/metaSMT/build/metaSMTConfig.cmake:6 (find_package)
cmake/find_metasmt.cmake:10 (find_package)
CMakeLists.txt:360 (include)
```
|
|
runtime: POSIX, make it compile with glibc 2.25
|
|
Travis-CI target for macOS
|
|
|
|
|
|
delcypher/unbreak_build_assignment_validating_solver
[CMake] Unbreak build due to not adding AssignmentValidatingSolver.cpp
|
|
to list of source files.
The cause of the breakage was me being to eager and merging #468
before forcing tests to re-run. That PR was written before the CMake
build system existed.
|
|
assignments against the corresponding `Query` object and check the
assignment evaluates correctly.
This can be switched on using `-debug-assignment-validating-solver`
on the command line.
|
|
It looks like `deps/stp-git-basic/lib` contains a directory named
`cmake` so use `-r` instead in the hack in the `metaSMT.sh`.
We didn't catch this before because the script previously just
carried on executing if a command failed.
|
|
set. Also exit if any of the commands in `.travis/metaSMT.sh` fail.
|
|
|
|
|
|
finding a bug with the `-exit-on-error` option enabled.
|
|
test: POSIX, stop FD_Fail to fail
|
|
fixed version of metaSMT with this flag being properly set)
|
|
|
|
METASMT_VERSION
|
|
runtime: change __get_sym_file to return NULL when path is NULL
|
|
clang warns about check-after-use in POSIX runtime:
runtime/POSIX/fd.c:573:17: warning: nonnull parameter 'path' will evaluate to 'true' on first r [-Wpointer-bool-conversion]
(path ? __concretize_string(path) : NULL),
^~~~ ~
path is dereferenced in __get_sym_file before this check. So add a check
to __get_sym_file and handle NULL appropriatelly by returning NULL too.
Signed-off-by: Jiri Slaby <jirislaby@gmail.com>
|
|
In our build environments, /etc/fstab is an empty file. Use /etc/mtab,
which should be non-empty anywhere, hopefully.
For the reference, the test fails as follows:
FAIL: KLEE :: Runtime/POSIX/FD_Fail.c (188 of 212)
************ TEST 'KLEE :: Runtime/POSIX/FD_Fail.c' FAILED ************
Script:
--
clang-3.8 -Iinclude test/Runtime/POSIX/FD_Fail.c -emit-llvm -O0 -c -o build/test/Runtime/POSIX/Output/FD_Fail.c.tmp1.bc
rm -rf build/test/Runtime/POSIX/Output/FD_Fail.c.tmp.klee-out
build/bin/klee --output-dir=build/test/Runtime/POSIX/Output/FD_Fail.c.tmp.klee-out --libc=uclibc --posix-runtime build/test/Runtime/POSIX/Output/FD_Fail.c.tmp1.bc --sym-files 0 0 --max-fail 1 > build/test/Runtime/POSIX/Output/FD_Fail.c.tmp.log
grep -q "fread(): ok" build/test/Runtime/POSIX/Output/FD_Fail.c.tmp.log
grep -q "fread(): fail" build/test/Runtime/POSIX/Output/FD_Fail.c.tmp.log
grep -q "fclose(): ok" build/test/Runtime/POSIX/Output/FD_Fail.c.tmp.log
grep -q "fclose(): fail" build/test/Runtime/POSIX/Output/FD_Fail.c.tmp.log
--
Exit Code: 1
Signed-off-by: Jiri Slaby <jirislaby@gmail.com>
|
|
There was a typo and 'not' utility was tried to be built with
FileCheck's libraries. But those can be undefined. Fix this by using the
correct variable.
Signed-off-by: Jiri Slaby <jirislaby@gmail.com>
|
|
Rewritten tests by replacing 'XFAIL: darwin' with 'REQUIRES: not-darwin'
|
|
'not-*' features that exist if target operating system does not match a list of know operating systems.
|
|
With glibc 2.25, we see:
runtime/POSIX/stubs.c:243:14: error: conflicting types for 'gnu_dev_major'
unsigned int gnu_dev_major(unsigned long long int __dev) __attribute__((weak));
^
/usr/include/sys/sysmacros.h:79:27: note: previous definition is here
__SYSMACROS_DEFINE_MAJOR (__SYSMACROS_IMPL_TEMPL)
^
Glibc 2.25 switched from ULL to dev_t for gnu_dev_major, gnu_dev_minor,
and gnu_dev_makedev. Handle by using an appropriate type according to
the glibc version.
Signed-off-by: Jiri Slaby <jirislaby@gmail.com>
|
|
test: ConstantExpr, kill bogus test
|
|
test: POSIX/DirSeek, cleanup
|
|
There is a test that thinks this should hold:
((&gInt >> 8) << 8) != ((&gInt << 8) >> 8)
For example, if the address is 0x00123400, this means:
0x00123400 != 0x00123400
which is obviously not true. Kill the bogus assumption as it causes
occasional failures in the tests. This is done by ORing the address with
1 so that we can have:
0x00123400 != 0x00123401
Convert also the respective truncated 32bit pointers to 64bit.
Signed-off-by: Jiri Slaby <jirislaby@gmail.com>
|
|
Core: explicitly create CallSite from Instruction
|
|
* remove unused stat variable
* use %ld for long int
Signed-off-by: Jiri Slaby <jirislaby@gmail.com>
|
|
Added new option --warnings-only-to-file which causes warnings to be written to warnings.txt only.
|
|
Core: MCJIT functions need unique names
|
|
Module: simplify is_object checks
|
|
Moved printFileLine() to be part of KInstruction
|
|
|
|
Fix internal fork without new pathOS.id
|
|
Using klee_message instead of llvm:errs
|
|
|
|
|
|
Newer LLVMs do not allow implicit conversion from Instruction to
CallSite. We see this error:
Internal/Support/ModuleUtil.h:36:19: note: candidate function not viable: no known conversion from 'llvm::Instruction *' to 'llvm::CallSite' for 1st argument
llvm::Function *getDirectCallTarget(llvm::CallSite);
^
So explicitly create a CallSite from Instruction.
Signed-off-by: Jiri Slaby <jirislaby@gmail.com>
|
|
|
|
to warnings.txt only. Disabled by default.
|
|
convert iterators using static_cast
|
|
We will use newer MCJIT with newer LLVM versions. But it needs unique
names of functions or a wrong function can be called. So prepend
"dispatcher_" to function names (even for older LLVMs).
Signed-off-by: Jiri Slaby <jirislaby@gmail.com>
|
|
Newer versions of LLVM do not allow to implicitly cast iterators to
pointers where they point. So convert all such uses to explicit
static_cast, the same as LLVM code does.
Otherwise we see errors like:
lib/Core/Executor.cpp:548:15: error: no viable conversion from 'Module::iterator' (aka 'ilist_iterator<llvm::Function>') to 'llvm::Function *'
Function *f = i;
^ ~
Signed-off-by: Jiri Slaby <jirislaby@gmail.com>
|
|
object::Binary has isObject method, which can be used to check whether
it is an object::ObjectFile. Use that, since dyn_casting of
object::Binary is not allowed in newer LLVMs:
lib/Module/ModuleUtil.cpp:304:78: error: cannot convert ‘llvm::object::ObjectFile’ to ‘llvm::object::ObjectFile*’ in initialization
else if (object::ObjectFile *o = dyn_cast<object::ObjectFile>(child.get()))
^
Signed-off-by: Jiri Slaby <jirislaby@gmail.com>
|
|
Teach KLEE to respect the requested memory alignment of allocated memory
|
