UnitTestBot / UTBotCpp

Tool that generates unit test by C/C++ source code, trying to reach all branches and maximize code coverage
Apache License 2.0
137 stars 26 forks source link

KLEE returns error on correct test case [C standard test] #328

Closed Lana243 closed 1 year ago

Lana243 commented 2 years ago

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:

  1. 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;
    }
  2. See error tests:
    
    #pragma region error
    TEST(error, variable_length_test_4)
    {
    variable_length(2UL);
    }

pragma endregion

4. 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_
misonijnik commented 2 years ago

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 commented 1 year ago

Fixed in #508