Cristian Cadar
Cristian Cadar
Hi, we're trying to understand the sources of non-determinism in STP. More exactly, is it enough to use the "--seed" option to get STP to execute deterministically on a certain...
Several benchmarks have calls to string functions that are not defined in the benchmark files. For instance, the following benchmarks have calls to `strcpy` without defining it: `c/ldv-linux-3.4-simple/32_1_cilled_ok_nondet_linux-3.4-32_1-drivers--acpi--fan.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i` `c/ldv-linux-3.4-simple/32_1_cilled_ok_nondet_linux-3.4-32_1-drivers--platform--x86--topstar-laptop.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i` `c/ldv-linux-3.4-simple/43_1a_cilled_ok_nondet_linux-43_1a-drivers--acpi--container.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.i`...
Benchmark `c/ldv-regression/fo_test.i` has the following sequence of calls: `int file = l_open("unknown",00);` where `l_open` eventually returns `__VERIFIER_nondet_int()` ... `int a = l_read(file,cbuf,99);` where `l_read` calls `read(file, ...)` But `read` is...
…t this warning once per array. Add test case. ## Summary: ## Checklist: - [x] The PR addresses a single issue. If it can be divided into multiple independent PRs,...
KLEE is already packaged for FreeBSD and macOS (Homebrew). We would like to find maintainers for other popular distributions, particularly Ubuntu, but also Arch Linux, Gentoo Linux, OpenSUSE etc.
**For:** we typically expect better performance and efficiency on large apps. Some numbers would be useful though. **Against:** the default implementation is time-dependant, and I would prefer having a deterministic...
Because the default values for KLEE options change from time to time, it would be useful to save all options and current values in klee-last/info.
...and would be nice to be fixed, although it doesn't have very high priority.
We need to add such tests: https://codecov.io/gh/klee/klee/src/master/lib/Core/ExecutorUtil.cpp