Polyspace C/C++代码验证培训课程培训中心

第一部分

Polyspace工作流程概览

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

· Polyspace与软件开发流程

· 简单验证样例

· 分析代码中的缺陷与运行时错误

Polyspace Bug Finder分析

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

· 常见运行环境构件

· 处理处理器特定代码

· 定义执行的上下文

· 设置目标硬件信息

· 分析和管理Bug Finder发现的缺陷

· 检测编码规则冲突

· 度量代码统计指标

分析Polyspace Code Prover的结果

目标： 能熟练解释Polyspace Code Prover的结果。

· 抽象解释概览

· 调用层次分析

· 源代码导航

· 执行路径

· 变量范围

· 全局变量

代码验证中的检查项

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

· C代码检查项一览

· 源代码中的检查项定位

· 检查项描述

· 相关验证选项

第二部分

管理Polyspace Code Prover验证与结果

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

· 判断验证开销

· 进行快速评审

· 进行选择性的橙色代码评审

· 设置验证精度

· 区分橙色检查项优先级

· 评审橙色检查项

增加Polyspace Code Prover验证精度

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

· 鲁棒性验证与上下文验证

· 函数打桩

· 数据范围指定

· 手动打桩

集成分析

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

· 管理代码模块

· 用Bug Finder与Code Prover分析集成缺陷与编码违规

· 导入注释

完整应用分析

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

· 创建应用级验证工程

· 改善应用的验证结果

· 发现并发访问问题

· 对比健壮性验证和上下文验证

· 创建文档

第三部分

实践教学（选修）

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

· Bug Finder 检测

· 验证 C++ 代码

· 任务和共享数据分析

· 验证生成的代码

· 开发过程回顾

· 工作流程整合

· 客户端/服务器软件安装

· 项目代码的 Polyspace 配置

· 结果解释