about summary refs log tree commit diff homepage
AgeCommit message (Collapse)Author
2017-03-30[Docker] Unbreak build.Dan Liew
The recent landing of macOS support in TravisCI (3a8bc6a43073b98b58c8cf0c20a930cb2c953b5d) broke the Docker build due to the `TRAVIS_OS_NAME` environment variable not being set by the Docker build. Do the simplest fix for now which is to define the variable. This isn't the cleanest fix but it will do for now.
2017-03-28Merge pull request #616 from jirislaby/glibc_225Cristian Cadar
runtime: POSIX, make it compile with glibc 2.25
2017-03-24Merge pull request #595 from andreamattavelli/travis_macosxAndrea Mattavelli
Travis-CI target for macOS
2017-03-24[Travis-CI] Added support for macOS buildAndrea Mattavelli
2017-03-24[Travis-CI] Refactored Z3 in its own scriptAndrea Mattavelli
2017-03-23Merge pull request #628 from ↵Andrea Mattavelli
delcypher/unbreak_build_assignment_validating_solver [CMake] Unbreak build due to not adding AssignmentValidatingSolver.cpp
2017-03-23[CMake] Unbreak build due to not adding AssignmentValidatingSolver.cppDan Liew
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.
2017-03-23Add `AssignmentValidatingSolver`. It's purpose is to check any computedDan Liew
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.
2017-03-23Add test case to check that on early exits stats are flushedDan Liew
2017-03-23Replace `llvm:errs()` with `klee_error()` as suggested by @andreamattavelliDan Liew
2017-03-23[WIP] Fix bug where stats would not be updated on early exit caused byDan Liew
finding a bug with the `-exit-on-error` option enabled.
2017-03-23Merge pull request #619 from jirislaby/FD_FailCristian Cadar
test: POSIX, stop FD_Fail to fail
2017-03-23remove special handling of metaSMT_CXXFLAGS (unnecessary now as we use a ↵Hoang M. Le
fixed version of metaSMT with this flag being properly set)
2017-03-23[travis] build metaSMT without C++11Hoang M. Le
2017-03-23[travis] use a proper version of metaSMT via environment variable ↵Hoang M. Le
METASMT_VERSION
2017-03-21Merge pull request #617 from jirislaby/no-warnCristian Cadar
runtime: change __get_sym_file to return NULL when path is NULL
2017-03-20runtime: POSIX, check path prior dereferenceJiri Slaby
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>
2017-03-17test: POSIX, stop FD_Fail to failJiri Slaby
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>
2017-03-17test: fix 'not' buildJiri Slaby
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>
2017-03-15Fix test case for OSX: only weak aliases are supported on darwinAndrea Mattavelli
Rewritten tests by replacing 'XFAIL: darwin' with 'REQUIRES: not-darwin'
2017-03-15[Lit] Add system information (linux/darwim) to LIT configuration. Added ↵Dan Liew
'not-*' features that exist if target operating system does not match a list of know operating systems.
2017-03-15runtime: POSIX, make it compile with glibc 2.25Jiri Slaby
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>
2017-03-07Merge pull request #608 from jirislaby/kill_testAndrea Mattavelli
test: ConstantExpr, kill bogus test
2017-03-06Merge pull request #614 from jirislaby/DirSeekCristian Cadar
test: POSIX/DirSeek, cleanup
2017-03-06test: ConstantExpr, fix bogus testJiri Slaby
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>
2017-03-06Merge pull request #611 from jirislaby/getDirectCallTargetAndrea Mattavelli
Core: explicitly create CallSite from Instruction
2017-03-06test: POSIX/DirSeek, cleanupJiri Slaby
* remove unused stat variable * use %ld for long int Signed-off-by: Jiri Slaby <jirislaby@gmail.com>
2017-03-06Merge pull request #609 from ccadar/warningsAndrea Mattavelli
Added new option --warnings-only-to-file which causes warnings to be written to warnings.txt only.
2017-03-05Merge pull request #607 from jirislaby/dispatcherAndrea Mattavelli
Core: MCJIT functions need unique names
2017-03-05Merge pull request #606 from jirislaby/ObjectFileCristian Cadar
Module: simplify is_object checks
2017-03-03Merge pull request #613 from ccadar/minor2Andrea Mattavelli
Moved printFileLine() to be part of KInstruction
2017-03-03Moved printFileLine() to be part of KInstructionCristian Cadar
2017-03-03Merge pull request #589 from gladtbx/klee_fix_pathOSAndrea Mattavelli
Fix internal fork without new pathOS.id
2017-03-03Merge pull request #612 from ccadar/minorAndrea Mattavelli
Using klee_message instead of llvm:errs
2017-03-03Using klee_message instead of llvm:errsCristian Cadar
2017-03-01fix for PathOS.idgladtbx
2017-03-01Core: explicitly create CallSite from InstructionJiri Slaby
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>
2017-03-01Updated test cases that check warning messages.Cristian Cadar
2017-03-01Added new option --warnings-only-to-file which causes warnings to be written ↵Cristian Cadar
to warnings.txt only. Disabled by default.
2017-03-01Merge pull request #604 from jirislaby/add_castsAndrea Mattavelli
convert iterators using static_cast
2017-02-28Core: MCJIT functions need unique namesJiri Slaby
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>
2017-02-28convert iterators using static_castJiri Slaby
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>
2017-02-28Module: simplify is_object checksJiri Slaby
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>
2017-02-28Merge pull request #547 from delcypher/fix_alignment_of_alloc_memoryCristian Cadar
Teach KLEE to respect the requested memory alignment of allocated memory
2017-02-27Merge pull request #600 from jirislaby/no_global_contextCristian Cadar
llvm: stop using global context
2017-02-25llvm: stop using global contextJiri Slaby
It was marked as deprecated long time ago and finally removed in LLVM 3.9. Remove all uses of getGlobalContext and create our own context. Propagate it all over the code then. [v2] use ctx, not C as name Signed-off-by: Jiri Slaby <jirislaby@gmail.com>
2017-02-24Teach KLEE to respect the requested memory alignment of globals and stackDan Liew
variables when possible. Previously an alignment 8 was always used which did not faithfully emulate what was either explicitly requested in the LLVM IR or what the default alignment was for the target.
2017-02-24Merge pull request #603 from jirislaby/no_list_copyAndrea Mattavelli
CommandLine: do not copy list in optionIsSet
2017-02-23CommandLine: do not copy list in optionIsSetJiri Slaby
Pass the list as reference. Otherwise we can get errors with newer LLVM like: lib/Basic/ConstructSolverChain.cpp:26:19: error: call to deleted constructor of 'llvm::cl::list<QueryLoggingSolverType>' if (optionIsSet(queryLoggingOptions, SOLVER_KQUERY)) { ^~~~~~~~~~~~~~~~~~~ llvm/Support/CommandLine.h:1466:3: note: 'list' has been explicitly marked deleted here list(const list &) = delete; ^ Signed-off-by: Jiri Slaby <jirislaby@gmail.com>
2017-02-22Merge pull request #599 from jirislaby/de_registerAndrea Mattavelli
klee: remove use of deprecated 'register'
generated by cgit-pink 1.4.1 (git 2.36.1) at 2024-11-24 23:46:59 +0000