使用 Polyspace 进行 C/C++ 代码验证

第1天 (共3天)

Polyspace工作流程概览

目标: 了解 Polyspace Bug Finder 与 Polyspace Code Prover，并跑通一个例子程序

• 代码验证工作流
• 运行 Bug Finder 分析
• 运行 Code Prover 验证
• 分析和修复软件问题

Polyspace Bug Finder 分析

目标: 分析可能不符合 ANSI C 的代码并配置运行时环境，使用 Polyspace Bug Finder 修正缺陷和编码规则违规。

• 创建 Polyspace 工程
• 常见运行时环境构件
• 处理特定处理器代码
• 设置目标硬件信息
• 使用 Polyspace Bug Finder 分析缺陷
• 分析 MISRA C 违规
• 度量代码指标
• 模板工程

分析 Polyspace Code Prover 的结果

目标: 能熟练解读 Polyspace Code Prover 的结果。

• 抽象演绎概览
• 分析调用树
• 在源代码中导航
• 解释 Polyspace Code Prover 结果
• 查看源代码中的全局变量用法

代码验证中的检查项

目标: 使用 Polyspace Code Prover 中可用的诊断信息查找运行时错误。

• C 源代码检查概述
• Polyspace Code Prover 运行时错误检查
• 相关验证选项

第2天 (共3天)

管理 Polyspace Code Prover 验证与结果

目标: 处理含有大量未证明检查项的验证结果。

• Code Prover 验证工作流
• 控制程序执行序列
• 设置橙色运行时错误检查项优先级

增加 Polyspace Code Prover 验证精度

目标: 学习如何在用 Polyspace Code Prover 验证代码时处置缺失的代码，以及如何对此施加影响从而产生更有意义的验证结果。

• 稳健性验证与上下文验证
• 自动上桩
• 数据范围指定
• 手动打桩

使用 Polyspace Access 进行集成分析

目标: 了解如何使用 Polyspace Access™ 管理日益复杂的代码的验证结果，以及如何解释并比较集成分析与稳健性分析。

• 使用 Polyspace Access 的提交后工作流
• 上下文验证
• 检测集成缺陷和运行时错误

完整应用分析

目标: 回顾对整个应用进行完整验证时的流程和选项。

• 应用软件问题
• 分析并发数据访问问题
• 替换汇编或硬件函数
• 在 Polyspace 中处理第三方代码
• 创建文档

第3天 (共3天)

实践教学（选修）

目标: 花时间来回顾你学到的内容并在你自己的项目上直接应用 Polyspace。潜在内容包括：

• Polyspace Bug Finder 检查
• 验证 C++ 代码
• 任务与共享数据分析
• 验证生成的代码
• 开发流程回顾
• 工作流集成
• 客户端/服务器软件安装
• 项目代码的 Polyspace 配置
• 结果解读

附录 F：使用 Polyspace 桌面端进行集成分析

目标: 学习如何管理复杂性日益增加的代码验证，以及如何解释并比较集成分析与稳健性分析。

• 上下文验证
• 创建新模块
• 检测集成缺陷和运行时错误