FreeRTOS内核三层校验：CBMC、CMock、VeriFast怎么跑通
【免费下载链接】FreeRTOS'Classic' FreeRTOS distribution. Started as Git clone of FreeRTOS SourceForge SVN repo. Submodules the kernel.项目地址: https://gitcode.com/GitHub_Trending/fr/FreeRTOS
FreeRTOS的测试框架把三层校验——CBMC内存安全证明、CMock内核单元测试、VeriFast功能正确性证明——都收进了仓库，克隆下来就能在本地重新验证内核的内存安全与API行为。
三层校验各管什么，源码在哪
FreeRTOS内核由公共代码和移植层两部分组成，Test/目录把校验工作分成三层，各有独立目录和构建入口：
- CMock：内核API功能正确性的单元测试，按queue、tasks、timers、event_groups、message_buffer等模块分目录，在宿主机上编译运行
- CBMC：内存安全的自动化证明，对每个入口点做有界模型检测，CI系统会在每个拉取请求上跑这套证明
- VeriFast：queue与list两个数据结构的无界功能正确性证明，结论不受队列长度限制，覆盖任意数量和任意时序的任务与中断组合
三份源码分别位于CMock单元测试、CBMC证明基础设施、VeriFast证明。CBMC下的patches/存放剥离static与volatile限定符的预处理补丁，VeriFast下的include/proof/存放全部证明共享的谓词与引理。Test/Target/目录另有跑在真实目标板上的集成测试。
克隆仓库并拉取内核子模块
内核源码在子模块里，不取回的话Test/下的测试目录找不到被校验的对象：
git clone https://gitcode.com/GitHub_Trending/fr/FreeRTOS cd FreeRTOS && git submodule update --init --recursive在宿主机跑CMock单元测试
依赖只有GCC、Make、Ruby、unifdef、LCOV。进入Test/CMock/后按模块点名跑，例如构建并执行队列单元测试用make queue，可执行文件落在build/bin。make -C list gcov跑单个目录并产出gcov覆盖数据，make coverage则构建全部测试并输出HTML报告到build/coverage。框架本体在CMock/CMock/子目录里，记住make目标名即可，不必深入其内部。新增用例时建议加ENABLE_SANITIZER=1打开ASan。
本地跑CBMC内存安全证明
前置条件：Python ≥ 3.7、Make、32位gcc库（Debian系安装gcc-multilib）、cbmc、goto-cc、goto-instrument在PATH中。proofs/下每个叶子目录是一个入口点的证明，先生成Makefile：
cd FreeRTOS/Test/CBMC/proofs python3 prepare.py再进入目标入口点目录执行make，产出HTML与JSON报告，例如TaskCreate对应proofs/Task/TaskCreate/html/html/index.html，Errors栏显示None即为通过。
VeriFast证明与队列调用图
CI固定使用VeriFast 19.12，装好后在VeriFast目录跑全套证明回归：
VERIFAST=/path/to/verifast makequeue/与list/目录下每个文件是一个API函数的标注版证明，注解是/*@ ... @*/形式的分离逻辑契约，也可以用verifast命令行按文件单验。证明改动后语句覆盖不再匹配时，先用NO_COVERAGE=1 make绕过覆盖检查。下图是queue证明的调用图：绿色为已证明函数，蓝色为按锁不变式建模的函数，灰色为假设的桩：
首次运行的几个高频坑
- 忘记拉子模块是最常见的失败原因：证明目录里没有内核源码，make直接报错
- 64位Linux漏装gcc-multilib，CBMC构建阶段失败
- CBMC证明耗时较长，先对你改动的入口点单独证明，别上来全量跑；Windows用户走WSL
- VeriFast IDE验证create.c等4个queue证明时必须关掉Check arithmetic overflow，否则出现误报
什么时候值得跑这套测试
内核级二次开发、要给内核建立合规CI、或需要引用功能正确性证据时，值得把三层校验依次跑通。如果只是改某个模块的bug做回归，跑对应模块的CMock单元测试就够，证明层交给CI去跑。
【免费下载链接】FreeRTOS'Classic' FreeRTOS distribution. Started as Git clone of FreeRTOS SourceForge SVN repo. Submodules the kernel.项目地址: https://gitcode.com/GitHub_Trending/fr/FreeRTOS
创作声明：本文部分内容由AI辅助生成（AIGC），仅供参考
 获取 Subblock 总数（Task Ration）的用法与底层原理)
