简介面向嵌入式软件开发与测试人员的Polyspace静态分析工具使用说明重点讲解如何通过Bug Finder与Code Prover检测C/C代码中的运行错误、规则一致性与可靠性缺陷适用于汽车电子、航空航天等安全关键领域的代码审核与质量评估。压缩包含1个PDF文档仅828KB内容从新工程建立、源码导入、分析模块选择到配置与运行检查完整覆盖工具操作流程并对Output Summary、Dashboard、Result List、Source、Result Details等结果窗口逐一说明还包含Dashboard中颜色含义红色高风险、绿色安全、橙色低风险等及其与代码风险的对应关系。文档结合fun_test.c示例函数直观展示死代码、溢出等问题的定位与原因解释适合需要快速上手Polyspace或建立静态检查规范的工程师参考。已有2868人学习作为一份轻量而系统的工具手册能帮助读者降低试用门槛、规范分析流程并提升代码安全审查效率。1. 编译通过不代表代码安全Polyspace 在查什么、为谁而查代码能编译、功能能跑和代码在极端输入下不会触发运行时错误本质上是两件事。后者需要静态验证工具兜底Polyspace 就是嵌入式静态检查这个方向上用得比较多的一款。它由 MathWorks 出品面向 C/C 代码做静态分析能覆盖四类诉求运行时错误检测、编码规则一致性MISRA/JSF、静态度量代码量、调用次数以及测试覆盖度。对汽车电子、轨交、医疗器械这类对软件可靠性有硬性要求的嵌入式场景Polyspace 的分析结果经常直接作为评审依据。这篇文章围绕一份带风险的 C 函数从建工程讲到结果定位把 Polyspace 的使用流程和踩坑点一次说清。适合嵌入式开发、代码评审和功能安全评估的工程师照着复现。2. 建工程与导代码五步把一个 C 文件接进 Polyspace 分析整个分析流程可以压缩成五步新建工程、导入源文件、选择分析模块、确认配置、运行检查。任何一份代码进来都先走这个骨架后面再谈分析深度。下面按一个单文件工程展开复杂工程只是在这个基础上加目录和配置项。2.1 Project Source Files 与 Include Folders头文件路径决定能否编译通过新建工程后最先看到的是项目配置界面核心入口是 Project Source Files 和 Project Include Folders。这一步踩坑的人不少常见错误是把工程文件所在目录当成 Include 路径填结果分析时报一堆头文件找不到。project_root/ ├── src/ │ ├── fun_test.c │ ├── can_driver.c │ └── comm/ ├── include/ │ ├── can_defs.h │ └── ecu_cfg.h └── polyspace/ └── demo.prj上面是一个典型嵌入式工程目录。Project Source Files 字段填src/下的 C 文件可以是多个文件一起参与分析Project Include Folders 填include/和src/comm/这类实际存在头文件的目录。这样配置的作用是让 Polyspace 在解析代码时能按编译器的视角找到所有依赖。逻辑说明Polyspace 分析前要先完成一次编译级解析头文件路径不完整后续所有检查都不会真正执行问题会在 Output Summary 里暴露。参数上Include Folders 允许填多条路径不需要人为把所有头文件拷贝到一个目录里那样反而破坏工程结构。我一般建议先填一个最小集合跑通后再补避免一次引入过多无关目录导致分析范围失控。还有一点容易忽略换机器后头文件路径失效是高频问题。把工程文件放在固定目录或者用相对路径组织比每次新建工程重新配一遍省事得多。2.2 Module Source Files 与 Configuration配置项不做减法源文件导入后切到 Module 部分这里决定实际分析内容和检查深度。Module Source Files 是真正要分析的代码单元Configuration 则控制检查项配置。原文示例工程里按默认配置跑实际项目里我建议至少把下面几个维度确认一遍配置项作用建议初始值编译命令与宏定义还原真实编译环境与 CI 脚本保持一致目标编译器识别基础类型宽度与边界对应交叉编译器代码标准启用 MISRA/JSF 等规则集按项目规范勾选分析方式Bug Finder 或 Code Prover先 Bug Finder后 Code Prover结果保留策略是否生成新结果文件首次分析建议保留参数说明编译器选项直接影响数据类型宽度判断。比如signed char在不同平台都是 8 位但int可能 16 位或 32 位Polyspace 依据编译器模型推断变量取值范围选错编译器会导致溢出判断偏离真实情况。配置时先取目标机的交叉编译器没有对应项就选最接近的变体并在结果解读时留意边界差异。默认配置能跑但我不建议长期不做减法。MISRA 规则全开时存量代码会报出海量风格类告警淹没真正需要关注的运行时错误。新工程先只保留与运行时安全强相关的检查项跑通后再逐步放开规则集这样 Dashboard 里的风险分布才有参考价值。2.3 运行检查与结果文件增量分析怎么省时间配置完成后进入运行环节界面会要求选择检查方法并确认是否生成新的结果文件。这个开关对应结果管理策略默认生成新结果会覆盖上一次分析适合常规迭代而当你需要对比两次修改之间的风险变化时关闭覆盖保留独立的结果记录更合理。运行开始后Output Summary 窗口会滚动输出分析进度。第一次跑工程时把注意力放在两类信息上编译阶段的错误提示和分析结束标志。编译错误会以红色警告出现文件找不到则常见黄色警告。这些信息比最终报告更优先处理因为编译没过后面所有结果都是无效的。我一般会在运行期间顺手做一件事记录分析开始时间和结束时间。这样能直观看到代码规模与耗时关系后续 Code Prover 跑全量分析前可以拿这个基线估算等待时间避免在项目交付节点上被动等待。3. Bug Finder 与 Code Prover静态扫描和深层验证到底怎么选Polyspace 的两个核心组件容易混淆。简单区分Bug Finder 是静态检测扫代码错误和规则一致性Code Prover 是运行错误检查做组件深层验证。两者的分析逻辑、耗时和结果可信度都不一样选错会直接影响项目节奏。3.1 Bug Finder适合日常集成的快速扫描Bug Finder 的工作方式更接近传统静态分析扫描速度快适合在开发迭代中高频执行。它能找出的问题包括明显的编码错误、规则违背、死代码、可疑的算术运算等。对大多数嵌入式项目来说把 Bug Finder 挂在持续集成流程里每次提交代码自动跑一遍是成本最低的防线。结合附件的fun_test.c函数Bug Finder 能直接标出执行不到的分支——y x 5之后if ( y 0 )永远不成立同时能识别出res z 5这类可能溢出的赋值。这些结论不依赖运行输入因为在signed char范围内z的最大可能取值已经足够触发溢出。Bug Finder 和编译器告警的区别值得说一句。编译器警告聚焦语法级和明显类型问题Bug Finder 则按数据流推演变量可能取值范围再对照目标类型边界给出风险判定。前者是编译的副产物后者是独立的验证活动两者定位不同不能互相替代。3.2 Code Prover用形式化验证换深度结论Code Prover 解决的问题更陡它穷举函数入口的所有可能输入状态在抽象解释的框架下推演每条执行路径证明或证伪运行时错误是否存在。结果不是「可能有问题」而是「经过验证在给定输入范围内安全」或「存在一条可到达的错误路径」。这是 Bug Finder 做不到的。Code Prover 的结果用颜色分级和 Bug Finder 的红色/粉色体系不完全相同务必区分颜色含义处理动作绿色绝对安全代码无需处理红色存在错误的高风险代码必须定位修复橙色可能存在错误的低风险代码分析外部输入和返回值范围灰色不会执行的死代码确认逻辑或删除冗余分支这个颜色体系直接体现在 Dashboard 和 Source 窗口。橙色条目是项目里争议最多的地方它通常来自外部函数返回值范围不确定。比如extFunc(y)的返回值Code Prover 不知道这个外部函数实际输出范围只能按signed char全范围推演于是z的取值被放大到-128~127后续加法全部被标记为可能溢出。这不是误报而是证明过程中信息不足。3.3 选型逻辑先 Finder 后 Prover别一上来就全量验证我见过两种极端一种只跑 Bug Finder交付评审拿不出深层验证证据另一种全项目直接 Code Prover一跑就是几个小时迭代完全卡死。正确的组合是分阶段上强度。日常开发阶段跑 Bug Finder每次提交都过一遍处理明显的规则问题和编码错误到版本冻结或安全关键组件评审前对该组件单独跑 Code Prover对红色项逐条确认。这样既保证高频检查的时效又能在关键节点拿出形式化验证级别的结论。需要补充的是Polyspace 在 Linux 环境下的命令行接口也常见于服务器批量分析做法一般是把建好的工程文件放到编译服务器通过命令行触发分析再把结果文件导回桌面端查看。这个工作流特别适合持续集成也是很多团队在嵌入式 Linux 项目里的实际用法。4. 结果窗口联动解读从 Dashboard 饼图到 Source 代码标记分析跑完只是开始真正花时间的是结果解读。Polyspace 的结果展示拆成五个窗口它们之间是联动关系不是独立面板。读懂这套联动定位问题的速度能差出几倍。4.1 Output Summary 与 Dashboard先看全局再钻细节Output Summary 是分析过程的流水账也是排错的第一现场。它记录分析进度、过程信息、遇到的问题以及是否正常结束。编译阶段有错误时这里会出现红色警告文件查找失败则是黄色警告。我拿到一份分析结果习惯先翻 Output Summary 确认没有编译级问题再去看 Dashboard顺序不能反。Dashboard 是分析结果的总览包含三块核心信息风险错误数量占比的饼状图、分析覆盖度柱状图、错误类型及数量图。饼状图中红色表示高风险错误粉色表示低风险点击色块会联动 Result List 窗口列出对应条目。覆盖度柱状图直观显示有多少代码被分析覆盖到这个比例在评审时容易被追问——覆盖度低说明分析结论的可靠性打折。Output Summary 关键信息整理自常见分析过程 [Info] Parsing source files ... ok [Info] Compiling fun_test.c ... ok [Warning] Cannot find include file: can_defs.h [Error] Syntax error in comm/parse_util.c line 42 [Info] Analysis complete.上面是输出摘要中常见的几类信息形态。出现 Warning 和 Error 时先解决文件级问题再重新分析不要拿着残缺结果继续解读。否则 Dashboard 里的统计会漏掉被中断的代码段饼图比例失真。4.2 Result List 与 Source 窗口从风险列表定位到代码行Result List 窗口按风险类型聚合展示包含风险项名称、位置、数量。示例工程跑 Bug Finder 后这个窗口会列出 1 处执行不到的死代码、2 处可能溢出的位置。点击任意风险项Source 窗口会跳转到对应代码行。Source 窗口的标记规则很直观风险代码行前有红圆圈标识位置代码本身变红表示风险产生原因产生风险的过程代码下有小圆点鼠标悬停会弹出原因提示。这里的关键动作是看「过程原因」而不是只看「结果位置」。溢出发生在res z 5但原因可能在更早的extFunc(y)返回值范围顺着小圆点逐个看才能找到该约束输入的地方。4.3 Result Details完整错误路径是怎么生成的Result Details 窗口展示的是分析过程细节解释错误产生的前因后果。它和 Source 窗口的弹窗提示互补弹窗给局部原因Result Details 给完整路径。这个窗口的价值在于它把 Polyspace 的推演链展示出来从函数入口开始变量的取值变化、分支走向、在哪一步触发了越界。评审时我习惯直接引用 Result Details 的路径描述比口头解释「这里可能溢出」有说服力得多。Code Prover 模式下Result Details 还会标注颜色判定的依据——绿色基于已验证范围橙色基于未约束输入红色基于可到达的错误状态。5. Polyspace 避坑指南头文件告警、超时与误报的五个现场这里把实际使用中容易翻车的场景集中列出来按「现象 → 原因 → 解决」的方式说明。每一条都来自真实项目里的教训照着排查能省下不少时间。5.1 分析了半天结果全是无效数据现象Output Summary 顶部一堆红色警告分析过程很快结束Dashboard 里覆盖度极低或根本没有结果。原因代码编译没过。最常见的是 Project Include Folders 没配全依赖的头文件解析失败后续分析全部中断。解决先看红色警告指向的文件路径把缺失的 include 目录补齐确认宏定义是否完整——工程里常见#ifdef包裹的代码段宏没定义整段会被跳过。修正后重新分析确认 Output Summary 不再出现编译错误再继续。5.2 换了台机器黄色警告提醒文件找不到现象同一个工程文件拷贝到另一台电脑运行分析时大量黄色警告部分源代码没有被识别。原因工程中记录了绝对路径换机器后原路径不存在。这个在多人协作里很常见有人把自己的工作目录写死到配置里提交后其他人一打开就报错。解决工程文件尽量放到团队统一约定的相对路径下重新导入源文件时用相对路径组织每次迁移后先检查配置里的路径前缀是否与当前环境一致再启动分析。5.3 Code Prover 标记橙色代码明明「不可能」溢出现象一个函数入参已被上层限制在 0~100Code Prover 仍把函数内buffer[index]标记为橙色提示可能越界。原因Polyspace 在分析单函数时不感知调用方的约束。没有显式前置条件时入参按类型全范围推演index可能取到负值于是访问被判定为潜在风险。解决在函数入口补充形式化契约说明入参范围Polyspace 支持通过配置或代码注释方式声明前置条件。约束后橙色会转为绿色或缩小到实际边界。这条几乎是 Code Prover 结果里最常被问到的「误报」。5.4 Code Prover 跑了一个小时还没结束现象全量工程切到 Code Prover 后分析时间从几分钟跳到几小时服务器内存也吃紧。原因Code Prover 做穷举式路径推演状态空间随分支数量和全局变量数量指数增长。不是工具卡死是分析深度带来的正常代价。解决用 Module 把工程拆细只对安全关键模块跑 Code Prover普通模块停留在 Bug Finder。分析前先看文档确认当前版本支持的代码规模与资源需求不要拿着几万行的老工程直接全量跑。5.5 两次分析结果不一致上次的红色项这次消失了现象同一份代码隔了一天重新分析Dashboard 的风险数量变化部分红色项不再出现。原因最常见的是配置变了——有人动了编译选项或代码标准其次是分析模式变了Bug Finder 和 Code Prover 的判定粒度不同。还有一种隐蔽情况外部函数实现被替换直接影响变量取值范围推演。解决分析前固定 Configuration 快照把编译命令、编译器、规则集、分析模块记录到工程备注里需要对比时保留上一份结果文件用增量分析模式跑。没有固定配置的分析结果不具备可比性。6. 用 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; if( y 0 ) { y 0; } z extFunc( y ); if( z 123) { res z 5; } else { res z 6; res res/2; } return res; }按前面第 2 章流程建工程只导入这一个文件配置默认项分析方式选 Bug Finder。结果预期是 1 处死代码、2 处可能溢出这正好对应 Dashboard 里的统计数字。死代码位置在if ( y 0 )x 1加 5 后y恒为 6非负分支永不进入。这个判定不依赖运行输入而是通过常量传播和范围推演得出的结论。两处溢出分别在res z 5和res z 6。z来自外部函数extFunc(y)返回值类型是signed char范围-128~127。在z 123为真的分支z最大可取 123res 128超出signed char上界 127触发溢出。在 else 分支z最小取 124z 6至少 130必然溢出。接着切到 Code Prover 重新分析同一个函数Source 窗口会按四个颜色标记y x 5赋值的局部逻辑是绿色if ( y 0 )分支呈灰色对应不可执行代码res z 5和res z 6因外部返回值未约束而呈橙色或红色。点击橙色项打开 Result Details能看到完整推演链——从extFunc的未约束返回值开始到z的取值范围生成再到加法运算的边界比较。这个路径描述就是我向评审解释风险依据时直接引用的内容。从那以后我每次给外部供应商提交代码、或者在版本封装前都会强制把 Bug Finder 跑一遍关键模块再补一次 Code Prover并把 Dashboard 截图和 Result Details 关键路径归档到工程目录里。这套习惯让我在交付评审时少吵很多架也让自己写的代码不再凭感觉说「应该没问题」。这个流程和示例函数文件放进资源包里了照着走一遍就能上手希望帮到你。本文还有配套的精品资源点击获取
