Polyspace用于C/ c++代码验证

3天中的第一天

---

Polyspace工作流程概述

摘要目的:熟悉Polyspace Bug Finder和Polyspace Code Prover，并完成一个介绍性示例。

• 代码验证工作流程
• 运行Bug查找器分析
• 运行代码验证程序验证
• 分析和修复软件问题

Polyspace Bug查找分析

摘要目的:分析可能不符合ANSI C标准的代码，并考虑运行时环境，并使用Polyspace Bug Finder纠正缺陷和编码规则违反。

• 创建Polyspace项目
• 公共运行时环境构件
• 处理处理器特定的代码
• 设置目标硬件信息
• 分析Polyspace Bug Finder中的缺陷
• 分析MISRA C规则违反情况
• 度量代码度量
• 模板工程

分析Polyspace代码验证结果

摘要目的:精通解释Polyspace Code Prover结果。

• 摘要解释概述
• 分析调用树
• 在源代码中导航
• 解释Polyspace Code Prover结果
• 查看源代码中全局变量的使用情况

代码验证检查

摘要目的:使用Polyspace Code Prover中提供的诊断来查找运行时错误。

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

3天中的第二天

---

管理Polyspace代码验证程序验证和结果

摘要目的:处理包含大量未验证检查的验证结果。

• 代码验证程序验证工作流程
• 控制程序执行顺序
• 优先级橙色运行时错误检查

为Polyspace代码验证器验证增加精度

摘要目的:了解Polyspace Code Prover如何在验证过程中处理缺失的代码，以及如何影响这种行为以产生更有意义的验证。

• 鲁棒性验证和上下文验证
• 自动存根
• 数据范围规范
• 手动存根

与Polyspace Access的集成分析

摘要目的:了解如何使用Polyspace Access™管理代码复杂度不断增加的验证结果，以及如何解释和比较集成分析与稳健分析。

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

应用程序分析

摘要目的:检查在验证完整应用程序时有用的程序和选项。

• 应用软件关注点
• 分析并发数据访问问题
• 替换组件或硬件功能
• 处理Polyspace中的第三方代码
• 创建文档

3天中的第3天(可选，只提供私人培训)

---

实践指导(可选)

摘要目的:花时间复习你所学到的知识，并将Polyspace直接应用到你自己的项目中。潜在主题包括:

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

附录F:与Polyspace Desktop的集成分析

摘要目的:学习如何管理代码复杂度不断增加的验证，以及如何解释和比较集成分析与健壮分析。

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