配置
模拟编译，指定分析约束，并提供从 Code Prover 获得最佳结果所需的其他信息
要将 Polyspace® Code Prover™ 有效集成到软件开发工作流中，请设置适当的分析选项以获得最佳结果。尤其是：
通过使用编译系统创建 Polyspace 工程或选项文件，或者通过显式指定编译器选项、数据类型大小以及其他与静态分析相关的编译选项，来模拟源代码编译。
通过对输入和全局变量指定外部约束或者通过指定全局分析假设，来限制被分析的代码路径。
创建与代码库中的现有组件对应的单独分析模块（工程或选项文件）。
定义专项分析所需的其他信息，例如多任务或全局变量初始化。
您可以使用 Polyspace 平台工程、命令行标志或选项文件来配置 Code Prover。请参阅：
