简介《Polyspace工具使用说明》面向嵌入式软件开发者、测试验证人员与代码审核者围绕C/C代码静态分析场景帮助读者理解如何发现编码错误、规则不一致、可靠性风险及测试覆盖度问题。压缩包内为1个PDF文件约828KB篇幅集中适合在开发与评审过程中随时查阅。内容系统梳理Polyspace的工程建立、分析配置与结果查看流程并对比Bug Finder和Code Prover在静态检测、运行错误检查及深层验证中的不同侧重点。结果解读部分涵盖输出摘要、Dashboard、Result List、Source和Result Details等窗口可帮助读者理解风险分布、覆盖度统计、问题定位以及红绿橙灰分级含义对MISRA/JSF规则检查、死代码与潜在溢出等典型问题也有涉及。已有2879人学习适合需要快速熟悉该工具、完善嵌入式代码检查思路的读者参考。1. 从一次误报说起Polyspace 到底在检查什么代码评审会上有人拍胸脯说这段signed char加法不可能出问题结果 Polyspace 在res z 5上标了一个红点。嵌入式软件做静态分析最怕的不是工具挑刺而是人拍胸脯。Polyspace 面向 C/C 代码两个引擎分工明确Bug Finder 做缺陷与规则一致性检查MISRA、JSF、静态度量、测试覆盖度Code Prover 做运行时错误证明把变量取值范围一路推到底。它适合谁写底层驱动、控制逻辑、通信协议栈需要拿证据说话而不是靠 review 感觉的人。下面按工程建立、结果解读、避坑、批量验证的顺序把这条链走通一遍。2. 建立工程把 fun_test.c 塞进分析器的完整路径2.1 分析前先确认三个前提很多人打开界面就点新建工程导文件、点运行然后在 Output Summary 里看到一片红色告警回头怪工具不准。真正决定分析质量的是三件事源文件清单是否完整、头文件搜索路径是否配齐、编译宏与目标平台是否和实际构建一致。前两个决定代码能不能过前端解析第三个决定类型宽度和符号性判断对不对。拿一个最小例子说话一个源文件、一个外部函数声明、十几行逻辑恰好能覆盖死代码和溢出两类典型问题。分析对象长这样/* fun_test.c —— 用于演示的最小分析单元 */ extern signed char extFunc(signed char y); /* 外部实现分析时拿不到函数体 */ signed char firstfun(void) { signed char x 1; signed char y; signed char z; signed char res; y x 5; /* x 已知为 1y 恒为 6下面判断恒不成立 */ if (y 0) { y 0; /* 死代码候选 */ } z extFunc(y); /* 返回值范围未知完全取决于外部实现 */ if (z 123) { res z 5; /* z 取 123 时 res 128越过 signed char 上限 127 */ } else { res z 6; res res / 2; } return res; }这段代码的价值在于它同时埋了两个雷。第一个是if (y 0)x被初始化成 1y x 5之后恒等于 6这个分支永远进不去属于典型的不可达代码。第二个是res z 5signed char在常见目标上是 8 位有符号范围 -128 到 127当z取 123 时结果 128 越界而有符号溢出在 C 标准里是未定义行为不是回绕一下还能用。提示char的符号性由编译器决定ARM 上常见默认无符号x86 上常见默认有符号。Polyspace 里如果这一项配错溢出结论会整体偏移这是后面避坑章节要展开的点。2.2 从新建工程到导入源文件界面操作链路不长但每一步都有容易漏的细节。新建工程后进入配置树重点看两个节点Project Source Files放待分析的.c文件Project Include Folders放头文件目录。本例没有独立头文件extern声明直接写在源文件里所以包含路径留空即可真实项目里通常会有一串-I目录逐个加进去顺序尽量和 Makefile 保持一致避免同名头文件被错误命中。接着是Module节点它决定分析什么。Module Source Files指定本次参与分析的文件子集Configuration指定检查项配置Result指定结果落盘位置。一个工程里可以挂多个 Module做增量分析时只跑改动的那一块比每次全量快得多。最后点运行按钮界面会问是否生成新的结果文件选是就覆盖选否就在原有结果上追加多人协作时建议每次新建否则结果目录里的历史数据会把 Dashboard 的统计口径搅乱。2.3 Configuration 别只吃默认值原始说明里写的是按默认配置分析作为第一次上手没问题但默认配置只是能跑通不等于覆盖到位。需要动的通常是三块编译器与目标平台决定类型宽度、字节序、对齐、检查项集合Bug Finder 的缺陷族与规则集、以及 Code Prover 的精度与超时。前两项配错的后果是结论不可信第三项配错的后果是分析跑不完。我的习惯是先把编译器和目标平台对齐现有构建脚本再在默认检查集基础上只加不减跑一轮看基线然后按项目实际关心的规则族做裁剪。裁的时候留个心眼把裁掉的项记录在配置文件里而不是口头约定否则换个人接手就再也说不清当初为什么不查这一条。2.4 运行前先读 Output SummaryOutput Summary 是整条链路上信息密度最高的窗口它记录分析进度、过程日志、以及前端解析阶段的问题。红色通常意味着编译级失败比如找不到文件、语法不通过、宏展开异常黄色多半是警告比如某个头文件被跳过、某个函数只有声明没有定义。这些信息在 Dashboard 里是看不到的Dashboard 只统计分析出来的问题不统计分析本身出的问题。一个实用的顺序是先清空红色再逐条确认黄色是否可以接受最后才去看风险列表。红色没清完就去看结果等于拿一份残缺的代码去下结论。3. Bug Finder 实战死代码与溢出是怎么被揪出来的3.1 Dashboard 三张图各自的读法分析结束后 Dashboard 一般会给出三类视图风险数量占比的饼图、分析覆盖度的柱状图、错误类型与数量的分布图。饼图用颜色区分风险等级红偏高风险、粉偏低风险点进去会联动 Result List 定位到具体条目覆盖度柱状图反映有多少代码真正被分析到覆盖度低往往说明大量函数只有声明没有实现或者被条件编译挡在外面类型分布图回答这批问题里哪一类最多是决定先修哪一批的依据。我一般先看覆盖度再看风险数。覆盖度只有六成的工程风险数为零也不值得高兴那只能说明剩下四成没被看见。覆盖度上去了风险数才有横向对比的意义。3.2 死代码判定res res / 2为什么执行不到示例代码里y 0那个分支Bug Finder 会标成不可达代码。判定逻辑并不神秘x是局部变量且在同一条路径上被赋值为常量 1y x 5于是被推成常量 66 0恒假分支体自然进不去。这类问题人眼也看得出来但真实工程里常量往往隔着三层函数调用和两个宏人眼就失效了。再看else分支里的res res / 2。它本身不是死代码但如果上游某个条件已经把这条路径封死或者extFunc的返回值范围被约束在某个区间导致else永远不成立它就会被标灰。所以看到执行不到的提示第一反应不应该是删代码而是问这个结论依赖哪些前置条件条件错了结论就错了。3.3 溢出检查8 位边界上的那一格res z 5被标红的推导过程是这样的z来自extFunc(y)的返回值声明类型是signed char在没有额外约束的情况下取值范围是 -128 到 127进入分支的条件是z 123两者取交集得到z ∈ [-128, 123]再算z 5上界变成 128超出signed char的 127。整个推演只用了类型范围和分支条件不需要真的把程序跑起来。这类溢出在测试阶段极难暴露因为要构造出恰好z 123的输入还得让外部函数真的返回这个值。静态分析的价值就在这里它不需要用例只需要类型和路径。检查项触发位置依赖条件处置方式不可达代码if (y 0)分支体x的常量传播、y的赋值链删除分支或修正条件有符号溢出res z 5signed char位宽、z的取值范围提升中间变量类型或加饱和判断外部函数范围未知z extFunc(y)缺少函数体与契约说明补 stub 或声明取值范围3.4 Result Details 里的因果链怎么读Result List 只告诉你哪里有问题Result Details 才告诉你为什么会得出这个结论。它会按步骤列出推演过程先确定x的值再算y再判断分支可行性最后算res的区间。读这条链的时候重点看两处一是它假设了哪些前置条件二是这些假设在你看来是否成立。如果某一步假设明显不对比如它认为某个全局变量可以被任意中断改写而你实际上有互斥保护那这条告警就是配置问题而不是代码问题正确做法是补上约束而不是改代码。反过来如果推演链每一步都站得住那就老老实实改代码。4. Code Prover 的颜色语义绿橙红灰对应哪类可靠性结论4.1 抽象解释与证明的边界Code Prover 和 Bug Finder 的底层思路不同。Bug Finder 找的是存在某条路径会出问题属于缺陷发现Code Prover 试图证明所有路径都不会出问题属于性质验证。它靠抽象解释把变量的所有可能取值压缩成区间或集合在每个程序点上推进直到不动点收敛。既然是抽象就一定有精度损失所以它给出的是三种结论证明安全、证明有问题、证明不了。这个三分法直接对应界面上的颜色。理解这一点才不会把橙色当成轻微错误来处理。4.2 绿橙红灰四色的处置优先级绿色表示在所有被建模的路径上都没有检出运行时错误是已证明安全红色表示存在确定的错误路径比如除零、越界、溢出必须改橙色表示可能存在错误取决于尚未确定的输入或外部返回值需要补信息才能收敛灰色表示该代码不可达属于死代码。处置优先级不是红 橙 绿而是灰 → 红 → 橙。灰色先处理因为它意味着有代码根本没参与验证覆盖度是假的红色其次是确定缺陷橙色最后攻坚因为它需要靠补 stub、加范围约束、调精度来收敛工作量最大且不一定能全部消掉。绿色区域不用管但要注意它是在当前配置和当前约束下被证明的配置一改就得重新证。4.3 给外部函数写 stubextFunc的范围从哪来示例里extFunc只有声明没有实现Code Prover 对它的返回值只能按signed char全范围处理于是橙色会沿着z一路扩散。真实项目里这类外部依赖非常多硬件寄存器读取、通信回调、第三方库。解决办法不是把它删掉而是给一个受控的 stub把契约写进去。/* extFunc_stub.c —— 仅用于分析不参与最终构建 */ #include limits.h /* 契约该函数返回 [-10, 100] 区间内的值 依据来自模块接口文档不是拍脑袋定的 */ signed char extFunc(signed char y) { signed char ret; /* 用不可判定的分支表达任意取值让分析器保留区间而不是收敛到单点 */ if (y 0) { ret 0; } else { ret 0; } __CPROVER_assume(ret -10 ret 100); return ret; }这里的关键不是代码本身而是那个区间[-10, 100]从哪来。它必须来自接口文档、上游模块的实际行为、或者实测采样不能为了让告警消失而随手写个窄区间。把区间写窄了橙色会变绿但那个绿是假的比橙色更危险。注意stub 只用于分析不要混进产品构建。工程里建议单独放一个目录构建脚本显式排除。4.4 精度与耗时的折中Code Prover 的分析时间和精度强相关。影响最大的几个因素是循环展开次数、是否做上下文敏感的过程间分析、以及每个函数的超时设置。默认配置在中等规模模块上通常能跑完代码量上去之后就容易卡住。实践中的取法是分模块跑而不是一把梭。先按编译单元切分每个 Module 单独设超时超时的函数会被标注为未完成验证这些就是下一轮要重点处理的对象。循环展开次数从保守值起步看橙色比例再逐步放宽每放宽一次都记录耗时变化形成一张自己的经验表。5. 避坑与排查五条踩过的坑5.1 前端解析失败满屏红色现象点运行后 Output Summary 立刻刷出红色告警提示文件查找失败或语法错误Dashboard 空白。原因包含路径没配全或者编译宏和实际构建不一致导致条件编译走了另一条分支把不该编进去的代码编了进来把该编的代码挡在外面。解决把工程里实际使用的编译命令原样搬到本机跑一遍确认能编过再进 Polyspace。编译命令里的-I、-D、-std逐项对应到工程配置里。这一步花十分钟能省掉后面两小时的困惑。5.2 结果一片橙色几乎没有结论现象Code Prover 跑完绝大多数代码是橙色红色寥寥绿色也寥寥。原因外部输入没有约束。凡是来自外部函数、全局变量、硬件读取的量分析器都按全范围处理区间一路发散最后啥也证明不了。解决按模块梳理输入源能写 stub 的写 stub不能写的用数据范围约束把区间框住。框的时候务必留证据区间来源写进注释否则半年后没人敢动这行配置。5.3 溢出结论和预期相反现象明明用的是有符号类型工具却不报溢出或者反过来明明做了范围保护还是被标红。原因char的符号性配置和实际目标平台不一致或者保护判断写在了赋值之后。解决先在配置里明确目标平台的char符号性再检查保护逻辑的位置。示例代码里如果先算res z 5再判断越界保护是无效的因为溢出已经发生了。5.4 分析跑了一夜没结束现象进度条卡在某个函数上不动CPU 占满内存持续上涨。原因深层递归、大循环、函数指针导致的调用图爆炸或者上下文敏感分析把路径数乘得太大。解决先定位卡住的函数把它拆成独立 Module 单独跑降低循环展开次数关掉不必要的上下文敏感选项。实在跑不完的函数标记为例外并写明理由比让它拖垮整个分析流程强。5.5 规则检查报出几百条没人看现象接上 MISRA 规则集之后Result List 里几百条告警团队直接放弃治疗。原因规则集版本和项目基线不一致或者把建议类规则和强制类规则混在一起看。解决先对齐基线版本再按强制/建议分级强制类逐条处理建议类批量评估后写入偏离说明。偏离说明不是走过场要写清为什么不改、风险如何控制否则审计时还得重来一遍。6. 用命令行跑批量分析把验证做成可复现流程界面点一遍能出结果但每周点一遍就不现实了。真正让静态分析活下来的是把它塞进构建流程用命令行跑结果落盘和历史基线对比。命令行的基本形态大致是这样# 以批处理方式运行 Bug Finder结果落到独立目录 polyspace-bug-finder \ -sources fun_test.c \ -lang c \ -compiler gcc \ -target x86_64 \ -results-dir ./ps_results \ -report-output ./ps_results/report参数里-sources指定待分析文件-lang指定语言-compiler和-target决定类型宽度与符号性-results-dir是结果落盘位置-report-output生成可归档的报告。不同版本选项名可能略有差异配置前先跑一次帮助命令确认。写成脚本之后把结果目录按日期归档下一次分析跑完做一次条目级对比新增的红色项就是本次改动引入的风险这条信息比任何评审意见都硬。验证方法上我习惯做三层第一层看覆盖度有没有掉掉了说明有代码没被分析到第二层看红色项有没有新增新增的必须当天定位第三层看橙色项的收敛趋势收敛慢说明约束没补到位。三层都过了这次改动才算通过静态验证。有个教训印象很深早期我把结果目录固定在同一个路径每次覆盖某次重构之后红色项从 3 条变成 1 条团队还挺高兴后来才发现是配置文件被改错两个文件压根没进分析范围。从那以后我每次跑分析都先把覆盖度和文件清单打印出来对一遍再去看风险数字。希望帮到你。本文还有配套的精品资源点击获取