You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Dear all,
I found that the assertion violation in the following code is missed if you call KLEE with option --use-fast-cex-solver, but finds it if you omit the option:
#include <assert.h>
#include "klee/klee.h"
int N = 13;
int main() {
int a[N];
for (int j = 0; j < N - 1; j++) {
a[j] = klee_int("a[j]");
klee_assume(a[j] < 2139062144);
}
a[N - 1] = 100;
klee_assume(100 < a[N-2]);
int i = 2;
while (i < N) {
if (a[i] > a[i - 1]) {
klee_assume(0);
}
i = i + 1;
}
assert(a[2] <= a[3]);
return 0;
}
I compiled with clang-14 -emit-llvm -c -g -O0 -Xclang -disable-O0-optnone -I ~/klee/include/ test.c and executed klee --use-fast-cex-solver test.bc.
KLEE's output is given by:
KLEE: output directory is "/home/klee-out-5"
KLEE: Using Z3 solver backend
KLEE: Deterministic allocator: Using quarantine queue size 8
KLEE: Deterministic allocator: globals (start-address=0x7fb6ca600000 size=10 GiB)
KLEE: Deterministic allocator: constants (start-address=0x7fb44a600000 size=10 GiB)
KLEE: Deterministic allocator: heap (start-address=0x7eb44a600000 size=1024 GiB)
KLEE: Deterministic allocator: stack (start-address=0x7e944a600000 size=128 GiB)
WARNING: this target does not support the llvm.stacksave intrinsic.
KLEE: ERROR: test.c:16: invalid klee_assume call (provably false)
KLEE: NOTE: now ignoring this error at this location
Thanks for the report. As documented, --use-fast-cex-solver is an experimental feature, which as far as I know is not being used much. Have you found it useful, or are you testing KLEE?
Dear all,
I found that the assertion violation in the following code is missed if you call KLEE with option --use-fast-cex-solver, but finds it if you omit the option:
I compiled with
clang-14 -emit-llvm -c -g -O0 -Xclang -disable-O0-optnone -I ~/klee/include/ test.c
and executedklee --use-fast-cex-solver test.bc
.KLEE's output is given by:
KLEE: output directory is "/home/klee-out-5"
KLEE: Using Z3 solver backend
KLEE: Deterministic allocator: Using quarantine queue size 8
KLEE: Deterministic allocator: globals (start-address=0x7fb6ca600000 size=10 GiB)
KLEE: Deterministic allocator: constants (start-address=0x7fb44a600000 size=10 GiB)
KLEE: Deterministic allocator: heap (start-address=0x7eb44a600000 size=1024 GiB)
KLEE: Deterministic allocator: stack (start-address=0x7e944a600000 size=128 GiB)
WARNING: this target does not support the llvm.stacksave intrinsic.
KLEE: ERROR: test.c:16: invalid klee_assume call (provably false)
KLEE: NOTE: now ignoring this error at this location
KLEE: done: total instructions = 655
KLEE: done: completed paths = 1
KLEE: done: partially completed paths = 10
KLEE: done: generated tests = 2
KLEE's version is:
KLEE 3.1-pre (https://klee.github.io)
Build mode: RelWithDebInfo (Asserts: ON)
Build revision: 9edf8e8
Ubuntu LLVM version 14.0.0
Optimized build.
Default target: x86_64-pc-linux-gnu
Host CPU: alderlake
The text was updated successfully, but these errors were encountered: