Support symbolic-size allocations

[davidtr1037]

Problem:
Currently, when the allocation size is symbolic, KLEE concretizes it.
This may lead to coverage loss and missed bugs.

Solution:
To address this, we may use the bounded symbolic size model (based on this paper).
In this model, every memory object has a (concrete or symbolic) size and a concrete capacity.
If the size is symbolic, then it is limited by the capacity.
Otherwise, the size and the capacity are equal.
The capacity can be specified by the user.