[KsassPeuk]

It depends on the verification tool you use.

Eva (the abstract interpreter) has different ways to model dynamic allocation. It is thus a tradeoff to find between precision and computation time.

WP does not have dynamic allocation support. This is an ongoing work, but it will not be available in the next release. Note that there are different ways to model the behavior of dynamic allocation, generally via axiomatic definitions and/or ghosts.