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

[Lana243]

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]

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]

Fixed in #508