Symbolic variables - size limiting

[GrosQuildu]

DeepState should allocate buffers of required length and truncate additional data (or don't it?). But running code below:

#include <deepstate/DeepState.hpp>
using namespace deepstate;

TEST(T, T) {
  char *data = (char*)DeepState_Malloc(5);
  // symbolic_int z;
  // LOG(INFO) << "z " << z << "\n";
  // ASSUME_GT(z, 0x41414141);
  for (int i = 0; i < 10; ++i)
  {
    char out[3] = {};
    snprintf(out, 3, "%02x", data[i]);
    LOG(INFO) << out;
  }
  printf("\n");
}

with:

clang++ ./test.cpp  -o test -ldeepstate
echo -ne 'AB\x00CDBBBB' > input
./test --input_test_file input

shows:

WARNING: No test specified, defaulting to first test defined (T_T)
TRACE: Initialized test input buffer with data from `x`
TRACE: Running: T_T from ./test.cpp(4)
INFO: ./test.cpp(13): 41
INFO: ./test.cpp(13): 42
INFO: ./test.cpp(13): 00
INFO: ./test.cpp(13): 43
INFO: ./test.cpp(13): 44
INFO: ./test.cpp(13): 42
INFO: ./test.cpp(13): 42
INFO: ./test.cpp(13): 42
INFO: ./test.cpp(13): 42
INFO: ./test.cpp(13): 00
TRACE: 

TRACE: Passed: T_T

malloced buffer is overflowed. Hard to say if it may cause some problems, but would be nice to debug and explain it.

Uncommenting commented code fragment also returns more data than expected:

WARNING: No test specified, defaulting to first test defined (T_T)
TRACE: Initialized test input buffer with data from `x`
TRACE: Running: T_T from ./test.cpp(4)
INFO: ./test.cpp(7): z 1111638594

TRACE: ./test.cpp(8): Checked condition
INFO: ./test.cpp(13): 41
INFO: ./test.cpp(13): 42
INFO: ./test.cpp(13): 00
INFO: ./test.cpp(13): 43
INFO: ./test.cpp(13): 44
INFO: ./test.cpp(13): 42
INFO: ./test.cpp(13): 42
INFO: ./test.cpp(13): 42
INFO: ./test.cpp(13): 42
INFO: ./test.cpp(13): 00
TRACE: 

TRACE: Passed: T_T

echo -ne 'AB\x00CDBBBBXXXXXXXXXXXXX' > x
./test --input_test_file x

WARNING: No test specified, defaulting to first test defined (T_T)
TRACE: Initialized test input buffer with data from `x`
TRACE: Running: T_T from ./test.cpp(4)
INFO: ./test.cpp(7): z 1111638594

TRACE: ./test.cpp(8): Checked condition
INFO: ./test.cpp(13): 41
INFO: ./test.cpp(13): 42
INFO: ./test.cpp(13): 00
INFO: ./test.cpp(13): 43
INFO: ./test.cpp(13): 44
INFO: ./test.cpp(13): 42
INFO: ./test.cpp(13): 42
INFO: ./test.cpp(13): 42
INFO: ./test.cpp(13): 42
INFO: ./test.cpp(13): 58
INFO: ./test.cpp(13): 58
INFO: ./test.cpp(13): 58
INFO: ./test.cpp(13): 58
INFO: ./test.cpp(13): 58
INFO: ./test.cpp(13): 58
TRACE: 

TRACE: Passed: T_T