about summary refs log tree commit diff homepage
path: root/test/Runtime/POSIX
AgeCommit message (Collapse)Author
2022-06-15Spelling Fixesm-davis
2022-03-11FD_Fail: use /dev/zero instead of /etc/mtabMorgan Jones
/etc/mtab doesn't exist in the Nix build sandbox since /etc doesn't exist. However, /dev/zero is more common on UNIX systems and does.
2021-10-17test/Runtime/POSIX/Futimesat: futimesat(2) requires _GNU_SOURCE on glibc ↵Lukas Zaoral
platforms
2021-10-17test/Runtime/POSIX/Futimesat: Compile with -std=c99Lukas Zaoral
.. so that `linux` is not a defined macro. Without the `-std=c99` option, linux is an implicitly defined macro so all such substrings in the given path will be replaced with `1` during stringification. Unfortunately, Fedora's rpmbuild uses `x86_64-redhat-linux-gnu` as a build directory for all CMake projects which leads to a failure due to a change to `x86_64-redhat-1-gnu`. Fixes: #1424
2021-06-19Test failure for WSL 1Pavel Yatcheniy
2020-12-23tests: add getcwd EINVAL testFrank Busse
2020-04-09[posix-runtime] Improve model to handle full-path symbolic filesTimotej Kapus
2020-04-09[posix-runtime] Add test for full path consistency for symbolic filesTimotej Kapus
2020-03-22[posix-runtime] Simple GET/SET_LK modelTimotej Kapus
2019-11-07Added test for 3-argument main.Cristian Cadar
2019-11-05[test] Fix missing includesMartin Nowack
Fix multiple missing includes
2019-08-14Moved Gen*Bout.c tests outside the test/Runtime/POSIX directory, as they ↵Cristian Cadar
don't need POSIX support to run.
2019-08-14Replace sprintf with snprintf throughout codebaseCristian Cadar
2019-08-14Create all files in the replay directory and chdir to this directory before ↵Cristian Cadar
executing the program.
2019-08-14Updated error messages in Gen*Bout.cCristian Cadar
2019-08-14Cleaned up messages emitted by klee-replay, and prefixed them all with ↵Cristian Cadar
"KLEE-REPLAY:" to distinguish them from those printed by the replayed program
2019-08-01tests: fix Gen(Random)Bout.c: cd - command not foundFrank Busse
2019-03-31Made test/Runtime/POSIX/GenBout.c run in an isolated directoryAndrew Santosa
2019-03-31Various updates to gen-random-bout.cppAndrew Santosa
* Added handling of --sym-arg * Resolved the crash when minimum and maximum number of arguments for --sym-args are equal * Replaced "range" with "n_args" produced by --sym-args * Added model_version variable (constrained to 1), to prevent klee complaining about insufficient input * Allow a single dash to prefix an option * Arrange the elements in the correct order: command-line arguments, files, stdin, stdout * Added test/Runtime/POSIX/GenRandomBout.c test, with a substitution for %gen-random-bout in test/lit.cfg
2019-03-15Renamed --seed-out to --seed-file and --seed-out-dir to --seed-dir, and ↵Cristian Cadar
placed them in the seeding category. Moved options and option categories in Executor.cpp to the klee namespace.
2019-03-07Renamed %llvmgcc and %llvmgxx to %clang and %clangxx respectively.Cristian Cadar
2018-12-19Added checks option category, moved --optimize to starting category, renamed ↵Cristian Cadar
original --run-in option to --running-dir
2018-11-02Replaced --no-externals and --allow-external-sym-calls with ↵Cristian Cadar
--external-calls, updated tests accordingly, and improved documentation on external calls
2018-10-29add %OOopt to recently added tests and ConcreteJulian Büning
2018-10-26Added gen-bout tool to generate ktest file (file.bout) using specified ↵Andrew Santosa
concrete arguments and files. * Sample use cases: * Using an interesting input as a seed, such as a crashing input. * Analyzing the path condition of a crashing input. * Also added the test: test/Runtime/POSIX/GenBout.c
2018-10-26llvm5: test, add -disable-O0-optnone to -O0Jiri Slaby
Otherwise optimizations done in klee won't have any effect. Signed-off-by: Jiri Slaby <jirislaby@gmail.com>
2018-09-29Changed code to create up to 100 properly-numbered symbolic arguments, and ↵Cristian Cadar
add a corresponding check.
2018-09-29Add checks for correct usage of the POSIX model, together with an associated ↵Cristian Cadar
test.
2018-09-20Removed unused --sym-files 0 0 argument from FD_Fail test and rewrote the ↵Cristian Cadar
test to use FileCheck instead of grep
2018-09-20Updated IoCtl test to use --sym-stdin instead of --sym-files 0 x to make ↵Cristian Cadar
stdin symbolic and removed unused arguments to main.
2018-09-20Updated DirSeek test to use --sym-stdin instead of --sym-files 0 x to make ↵Cristian Cadar
stdin symbolic.
2018-09-10Add testcase to run POSIX environment and main without argumentsMartin Nowack
2018-09-06Use FileCheck and LINE instead of grep if possibleMartin Nowack
As we do not support LLVM 2.9 anymore, we can use FileCheck LINE instead of hard coding line numbers.
2018-09-06runtime: fix memory error in canonicalize_file_nameFrank Busse
Fixes #46 and reverts #47. As stated in #46, the solution works for musl, glibc etc. However, the code in stub.c is executed by uclibc and uclibc doesn't allocate the target buffer in realpath. The memory error occured while running df for 10min with DFS.
2018-07-04Reorder linking and optimizationsMartin Nowack
Link intrinsic library before executing optimizations. This makes sure that any optimization run by KLEE on the module is executed for the intrinsic library as well. Support .ll files as input for KLEE as well.
2018-05-17Add support for concretizing symbolic objects passed to external functionsTimotej Kapus
2018-05-09Fix test case to check for correct call stringMartin Nowack
2018-05-07Fixed test case to exercise modification to utimes()Cristian Cadar
2018-05-07Fixed utimes() behavior for symbolic files when the second argument is NULLyxliang01
2018-05-05Fix handling of errno if external functions are invokedMartin Nowack
If an external function in KLEE is invoked, it might update errno. Previously, the errno specific variable in a state was only updated if it was part of the executed instructions. That opened up a timeframe that increased the likelihood of errno being overwritten by another method call. This patch fixes two issues: * the errno of the KLEE process state is updated before the external function call allowing to detect changes to it later on * after the external call, the memory object of errno is directly updated with its new value, reducing the likelihood to be overwritten by another call Additional features: * Add support for `errno()` for Darwin as well. * Simplified errno handling in POSIX layer
2017-08-10Added a basic test for klee-replayCristian Cadar
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-06test: POSIX/DirSeek, cleanupJiri Slaby
* remove unused stat variable * use %ld for long int Signed-off-by: Jiri Slaby <jirislaby@gmail.com>
2016-05-28Fixed an incorrect read() invocation and missing includes for FD_Fail2.cCristian Cadar
2016-05-24Split creation of symbolic files and stdin in two distinct optionsAndrea Mattavelli
2015-09-25Don't use /tmp for futimesat unit testAndrew Chi
This causes problems on a shared machine where multiple users are running the KLEE unit tests.
2014-09-15Generate fake files for test casesMartin Nowack
2014-09-14Enable test case againMartin Nowack
2014-09-14Use not test instead of non-existing FAIL.Martin Nowack
2014-09-14Fix testcase FD_Fail2.cMartin Nowack
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.