I’m fairly certain that this does not require solving the halting problem. Fundamentally, every line of code can be transformed to the underlying code constructs, and those could be checked for allocations. Doing this in an efficient manner is probably hard, but certainly not impossible