FreeRTOS内核三层校验CBMC、CMock、VeriFast怎么跑通【免费下载链接】FreeRTOSClassic FreeRTOS distribution. Started as Git clone of FreeRTOS SourceForge SVN repo. Submodules the kernel.项目地址: https://gitcode.com/GitHub_Trending/fr/FreeRTOSFreeRTOS的测试框架把三层校验——CBMC内存安全证明、CMock内核单元测试、VeriFast功能正确性证明——都收进了仓库克隆下来就能在本地重新验证内核的内存安全与API行为。三层校验各管什么源码在哪FreeRTOS内核由公共代码和移植层两部分组成Test/目录把校验工作分成三层各有独立目录和构建入口CMock内核API功能正确性的单元测试按queue、tasks、timers、event_groups、message_buffer等模块分目录在宿主机上编译运行CBMC内存安全的自动化证明对每个入口点做有界模型检测CI系统会在每个拉取请求上跑这套证明VeriFastqueue与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_SANITIZER1打开ASan。本地跑CBMC内存安全证明前置条件Python ≥ 3.7、Make、32位gcc库Debian系安装gcc-multilib、cbmc、goto-cc、goto-instrument在PATH中。proofs/下每个叶子目录是一个入口点的证明先生成Makefilecd FreeRTOS/Test/CBMC/proofs python3 prepare.py再进入目标入口点目录执行make产出HTML与JSON报告例如TaskCreate对应proofs/Task/TaskCreate/html/html/index.htmlErrors栏显示None即为通过。VeriFast证明与队列调用图CI固定使用VeriFast 19.12装好后在VeriFast目录跑全套证明回归VERIFAST/path/to/verifast makequeue/与list/目录下每个文件是一个API函数的标注版证明注解是/* ... */形式的分离逻辑契约也可以用verifast命令行按文件单验。证明改动后语句覆盖不再匹配时先用NO_COVERAGE1 make绕过覆盖检查。下图是queue证明的调用图绿色为已证明函数蓝色为按锁不变式建模的函数灰色为假设的桩首次运行的几个高频坑忘记拉子模块是最常见的失败原因证明目录里没有内核源码make直接报错64位Linux漏装gcc-multilibCBMC构建阶段失败CBMC证明耗时较长先对你改动的入口点单独证明别上来全量跑Windows用户走WSLVeriFast IDE验证create.c等4个queue证明时必须关掉Check arithmetic overflow否则出现误报什么时候值得跑这套测试内核级二次开发、要给内核建立合规CI、或需要引用功能正确性证据时值得把三层校验依次跑通。如果只是改某个模块的bug做回归跑对应模块的CMock单元测试就够证明层交给CI去跑。【免费下载链接】FreeRTOSClassic FreeRTOS distribution. Started as Git clone of FreeRTOS SourceForge SVN repo. Submodules the kernel.项目地址: https://gitcode.com/GitHub_Trending/fr/FreeRTOS创作声明：本文部分内容由AI辅助生成（AIGC），仅供参考 FreeRTOS内核三层校验：CBMC、CMock、VeriFast怎么跑通
FreeRTOS内核三层校验CBMC、CMock、VeriFast怎么跑通【免费下载链接】FreeRTOSClassic FreeRTOS distribution. Started as Git clone of FreeRTOS SourceForge SVN repo. Submodules the kernel.项目地址: https://gitcode.com/GitHub_Trending/fr/FreeRTOSFreeRTOS的测试框架把三层校验——CBMC内存安全证明、CMock内核单元测试、VeriFast功能正确性证明——都收进了仓库克隆下来就能在本地重新验证内核的内存安全与API行为。三层校验各管什么源码在哪FreeRTOS内核由公共代码和移植层两部分组成Test/目录把校验工作分成三层各有独立目录和构建入口CMock内核API功能正确性的单元测试按queue、tasks、timers、event_groups、message_buffer等模块分目录在宿主机上编译运行CBMC内存安全的自动化证明对每个入口点做有界模型检测CI系统会在每个拉取请求上跑这套证明VeriFastqueue与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_SANITIZER1打开ASan。本地跑CBMC内存安全证明前置条件Python ≥ 3.7、Make、32位gcc库Debian系安装gcc-multilib、cbmc、goto-cc、goto-instrument在PATH中。proofs/下每个叶子目录是一个入口点的证明先生成Makefilecd FreeRTOS/Test/CBMC/proofs python3 prepare.py再进入目标入口点目录执行make产出HTML与JSON报告例如TaskCreate对应proofs/Task/TaskCreate/html/html/index.htmlErrors栏显示None即为通过。VeriFast证明与队列调用图CI固定使用VeriFast 19.12装好后在VeriFast目录跑全套证明回归VERIFAST/path/to/verifast makequeue/与list/目录下每个文件是一个API函数的标注版证明注解是/* ... */形式的分离逻辑契约也可以用verifast命令行按文件单验。证明改动后语句覆盖不再匹配时先用NO_COVERAGE1 make绕过覆盖检查。下图是queue证明的调用图绿色为已证明函数蓝色为按锁不变式建模的函数灰色为假设的桩首次运行的几个高频坑忘记拉子模块是最常见的失败原因证明目录里没有内核源码make直接报错64位Linux漏装gcc-multilibCBMC构建阶段失败CBMC证明耗时较长先对你改动的入口点单独证明别上来全量跑Windows用户走WSLVeriFast IDE验证create.c等4个queue证明时必须关掉Check arithmetic overflow否则出现误报什么时候值得跑这套测试内核级二次开发、要给内核建立合规CI、或需要引用功能正确性证据时值得把三层校验依次跑通。如果只是改某个模块的bug做回归跑对应模块的CMock单元测试就够证明层交给CI去跑。【免费下载链接】FreeRTOSClassic FreeRTOS distribution. Started as Git clone of FreeRTOS SourceForge SVN repo. Submodules the kernel.项目地址: https://gitcode.com/GitHub_Trending/fr/FreeRTOS创作声明：本文部分内容由AI辅助生成（AIGC），仅供参考 RELATED READING
延伸阅读
更多一线实战笔记与深度复盘，助您持续精进
