Arrays of objects out of bounds

[S1eGa]

Description
Problem is happen when you try to allocate array of objects with destructor on heap using new[] operator. New allocates 8 + array_size, and writes number of elements in front 8 bytes. Then pointer moves to first element in an array. So, in KLEE there is no information about such prefix, and simple out of bound exception can be missed.

To Reproduce
Consider the following code:

#include <cassert>

int value = 0;

struct A {
  int x;
  A() {}
  A(int x) : x(x) {}
  ~A() { ++value; }
};

int main() {
  A *a = new A[4];
  a[-2] = *(new A(2));
  delete[] a;
  assert(value == 4);
}

Expected behavior
Will be generated 1 successful path, and assertion will be passed.

Actual behavior
1 error path generated and assertion failed.

Visual proofs (screenshots, logs)

KLEE: Using STP solver backend
KLEE: WARNING: undefined reference to function: __gxx_personality_v0
KLEE: WARNING ONCE: Alignment of memory from call "_Znam" is not modelled. Using alignment of 8.
KLEE: WARNING ONCE: Alignment of memory from call "_Znwm" is not modelled. Using alignment of 8.
KLEE: ERROR: exmple.cpp:16: ASSERTION FAIL: value == 4
KLEE: NOTE: now ignoring this error at this location

KLEE: done: total instructions = 212
KLEE: done: completed paths = 1
KLEE: done: generated tests = 1

Compiled and executed with:

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

Additional info
If you will increase argument in line a[-2] = *(new A(2)) up to 5 or greater, you will receive memory out of bound in destructor, that is not an error, that we expect to receive.
This number in prefix means a lot, as code in llvm IR relies on it to call destructors to specified number of objects.
Index -2 is used because sizeof A == 4.

[ladisgin]

Moved to UnitTestBot/klee#62