Repository navigation
KLEE returns error on correct test case [C standard test] #328
Description
Description
KLEE returns error on correct test case. For that reason correct test is assigned to error test suite.
To Reproduce
Steps to reproduce the behavior:
- Generate code for the following function:
size_t variable_length(size_t len) {
if (len > 100 || len == 0) {
return 0;
}
size_t a[len];
for (size_t i = 0; i < len; ++i) {
a[i] = i + 1;
}
if (a[len / 2] == 3) {
return 1;
}
return 2;
}- See error tests:
#pragma region error
TEST(error, variable_length_test_4)
{
variable_length(2UL);
}
#pragma endregion- See klee output logs in
build/utbot_build/klee_out/src/snippet_dot_c/klee_out_variable_length/test000001.model.err:
Error: concretized symbolic size
File: TestProject/src/snippet.c
Line: 10
assembly.ll line: 1676
State: 4
Stack:
#000001676 in variable_length () at TestProject/src/snippet.c:10
#100002027 in __klee_posix_wrapped_main (=1, =8792603382528, =8792603361320) at TestProject/src/snippet_klee.c:21
#200001564 in klee_entry__src_snippet_variable_length (=3, =8792603361288, =8792603361320) at runtime/POSIX/klee_init_env.c:249
Info:
size expr: (Mul w64 8
(ReadLSB w64 0 len))
concretization : 32
unbound example: 16
Expected behavior
This test supposed to be in regression suite.
Actual behavior
This test is in the error suite.
Environment
UTBot version 2022.7.0
Metadata
Metadata
Assignees
Type
Projects
- Status
Activity
misonijnik commentedon Jul 20, 2022
KLEE does not support the execution of code in which there is an allocation of a symbolic size object. Instead, it tries to concretize the object's size and continues execution for that case only. In other cases the execution of the states ends with the error: "concretized symbolic size".
We have a plan to support allocation of symbolic size objects, the example above will be a great test for this feature.
ladisgin commentedon Mar 9, 2023
Fixed in #508