ASMC：用 Ghidra 与 CBMC 打造汇编模型检查器

ASMC 将 Ghidra 的 pcode 汇编语义接入 CBMC，把编译后的 .elf 文件提升为 .gb 文件再做模型检查。其核心提升工具 asmc-lift 仅约 1kLOC C++ 胶水代码，可支持独立汇编验证、反编译验证、DWARF 调试数据验证等场景。示例中 mov $42,%rax 的后置条件 outreg.rax == 42 通过检查，写成 43 则返回反例。