Ghidra + CBMC = Assembly Model Checker

I've been working on an alternate approach to this problem for a while now: https://github.com/kenballus/llvm-project/blob/abisan/llvm/tools/abisan-as/README.md

These kinds of register clobbering bugs can be caught with a little bit of static analysis in the assembler. Hopefully, future assemblers can warn about this kind of thing!

Very interesting to see it solved by CBMC, though. Makes a lot of sense.