链接脚本：把构建输入放进可验证的内存布局
6343 字·13 分钟
用最小 MEMORY/SECTIONS 抽象解释输入段到输出段再到命名内存区域的布局，并用 Host Fake 验证链接脚本边界符号如何被启动初始化消费。
Startup
启动代码：把复位入口变成可运行的 C 环境
4246 字·9 分钟
用 Host Fake 观察复位入口经过启动代码、栈使用条件和 C 运行时初始化后再进入 main 的顺序，并区分主机逻辑验证与真实 Cortex-M 行为边界。
向量表：按编号找到处理程序入口
用一个不冒充硬件的 Host Fake 验证异常或中断编号如何查找向量表项并选择抽象处理程序，同时区分该模型与主机普通函数调用。