Well, you would need a way to "tell" the compiler more about your intentions and maybe even explicitly declare rules for what you consider a memory leak in certain scenarios.
To provide an example for a different case: programs written in Gallina have the weak normalization property, implying that they always terminate.
To provide an example for a different case: programs written in Gallina have the weak normalization property, implying that they always terminate.