[nanolith]

It's a clever use of assembler, but in production code, it's much better to use a bounded model checker, like CBMC, to verify memory safety across all possible execution paths.