FreeRTOS 测试框架实操手册：3 步跑通第一条队列用例

FreeRTOS 测试框架实操手册：3 步跑通第一条队列用例

【免费下载链接】FreeRTOS'Classic' FreeRTOS distribution. Started as Git clone of FreeRTOS SourceForge SVN repo. Submodules the kernel.项目地址: https://gitcode.com/GitHub_Trending/fr/FreeRTOS

凌晨三点任务死锁，串口日志停在"往队列里发消息"，你缺的往往不是代码，而是证据：内核的队列到底靠不靠谱。FreeRTOS 测试框架就在仓库的 Test 目录下，分四条线：内存安全证明、单元测试、功能正确性证明、目标板集成测试。照下面走一遍，你能亲手跑通一条真实用例并读懂它的结果。

看懂四类验证能力

Test 目录下四个子目录各管一类问题，先按手头的问题挑对应的那条线。

用 CBMC 证内存安全

对内核 API 的每个入口做有界模型检测，证明它不会越界访问、不会解引用空指针；每条证明是 FreeRTOS/Test/CBMC/ 下 proofs 里的一个叶子目录，跑完生成 HTML 和 JSON 报告，Errors 一栏显示 None 即通过。

用 CMock 隔离依赖做单元测试

在 PC 上对队列、链表、任务、定时器这些内核 API 做单元测试，FreeRTOS/Test/CMock/ 里对任务管理、移植层这类跑不动的依赖提供 td_task.c 之类的模拟实现，其余桩函数由 CMock 自动生成。

用 VeriFast 证功能正确性

证明队列和链表实现在任意数量任务与中断下都内存安全、线程安全、"表现像一个队列"，且结论不依赖队列长度；证明文件就是加了 /@ ... @/ 注释的内核源码本身，路径 FreeRTOS/Test/VeriFast/。

上目标板跑集成测试

FreeRTOS/Test/Target/ 放的是必须在真实开发板上运行的功能测试，用来补上"PC 上逻辑对"和"真机跑得对"之间那段空白。

🧪 三步跑通第一条用例

1. 取代码。内核本体在 submodule 里，漏初始化会让后面所有构建失败：

git clone https://gitcode.com/GitHub_Trending/fr/FreeRTOS cd FreeRTOS && git submodule update --init --recursive --checkout

2. 构建并运行队列单元测试，用例组织在 FreeRTOS/Test/CMock/queue/：

cd FreeRTOS/Test/CMock make queue

3. 读结果。终端逐条打印用例名和通过/失败，可执行文件落在 build/bin；想一次跑完全部模块用 make run，想看覆盖率用 make coverage，HTML 报告在 build/coverage 下。

走查一条队列用例

拿 xQueueGenericSend 为例，按四拍过一遍：

• 设计用例：先定好三种它必须处理对的情况——正常入队、队列满且不等待时返回失败、唤醒一个正在等接收的任务。设计的重点是写清内核承诺了什么，而不是急着写断言。
• 隔离依赖：真实入队会走任务状态机和移植层，PC 上没有调度器，于是用 td_task.c 当"假任务管理"，再用 CMock 生成的桩函数替换掉跑不动的部分，被测代码保持原样。
• 执行：make queue 编译即运行，用例之间互相独立；想顺带抓内存问题，在 make 时加上 ENABLE_SANITIZER=1。
• 读结果：终端按顺序打印用例名，结尾给出总数与失败数；红了就先看失败用例名和它打印的断言，那是 queue.c 里的函数与行号，直接指向该读哪段源码。

判断该用哪条线

• VeriFast 证明只覆盖队列和链表两个数据结构；想给别的模块证内存安全，走 CBMC 按入口点证明的路线，别在 VeriFast 里找。
• CMock 单元测试跑在 PC 上，只验证"逻辑对"，不验证时序；"单独跑没问题、中断一来就死锁"这类要靠 Target 下的目标板测试暴露，别指望在 PC 上复现真实硬件行为。
• 新手最常踩的坑：忘了初始化 submodule。内核源码在子模块里，make 报找不到 queue.c 就是它，不是 Makefile 的锅。

回到开头那次凌晨三点的死锁：动手改业务代码之前，先确认内核队列的行为符合约定。下一步很具体——把 make queue 跑起来，第一行 PASS 读完，内核可靠性就有了第一份证据。

【免费下载链接】FreeRTOS'Classic' FreeRTOS distribution. Started as Git clone of FreeRTOS SourceForge SVN repo. Submodules the kernel.项目地址: https://gitcode.com/GitHub_Trending/fr/FreeRTOS