Klever

At the moment there isn't a strong ground under the memory allocation model. As I understand this is primarily due to we statically define it while this a deal of particular verifiers/configurations/options like, say, the assertions model (specifications). For other models just some clear API should exist. This API should be quite reach including various functions for accurate memory allocation, for allocating memory with unknown memory sizes, for allocating "trusted" memory, etc. All users of this API should be fixed appropriately.