Virtual functions execution in symbolic object

[ladisgin]

Moved from UnitTestBot/UTBotCpp#330

KLEE issue. Whenever object of class with virtual functions is made symbolic, we are generating many tests cases and waiting for forever in the end.

Consider the following test case:

#include <cassert>
#include "klee/klee.h"

struct A {
  int x = 10;
  virtual void foo() {
    x += 1;
  }
};

struct B : A {
  virtual void foo() {
    x += 2;
  }
};

int main() {
  A *a = new B();
  klee_make_symbolic(a, sizeof(B), "a");
  a->x = 100;
  a->foo();
  assert(a->x == 101); 
}

We are expect to generate 1 test, that will fail assert.

Instead we are getting weird test cases, as shown below, and non of them fails the assertion, and KLEE does not stop the execution.

KLEE: Using STP solver backend
KLEE: WARNING ONCE: Alignment of memory from call "_Znwm" is not modelled. Using alignment of 8.
KLEE: ERROR: exmple.cpp:21: memory error: out of bound pointer
KLEE: NOTE: now ignoring this error at this location
KLEE: ERROR: exmple.cpp:21: invalid function pointer
KLEE: NOTE: now ignoring this error at this location

Compiled and executed with:

clang -emit-llvm -c -g -O0 -Xclang -disable-O0-optnone example.cpp
klee example.bc