模块化分析
将工程模块化为更小的部分并指定每个部分的分析方式
将工程划分为更小的部分以便于分析：
使用选项
-classification将您的工程中的源文件分类为不同文件集，并指定分析这些文件集的方式。使用
polyspace-configure为在联编文件中创建的每个二进制文件创建单独的 Polyspace® 工程或选项文件。识别库，并使用
使用的库 (-library)选项指定分析这些库的方式。
您可以对非自有代码进行插桩以加快分析运行速度。使用这些选项来规避规模问题。
函数
polyspace-configure | (System Command) Create Polyspace Platform project, workspace, or options file from build command or compilation database |
Polyspace 选项
内联 (-inline) | 指定必须要为对其的每次调用在内部创建克隆的函数 |
结构体内部的验证深度 (-k-limiting) | 限制对嵌套结构体的分析深度 |
设置结构体内部的验证深度 | 指定必须指定结构体内部的验证深度 (自 R2023b 起) |
-classification | Control precisely which files to include in Polyspace analysis and how to analyze them (自 R2025a 起) |
使用的库 (-library) | Specify libraries that you use in your program |
主题
分类
- Classify Project Files into File Sets for Precise Control of Polyspace Analysis
Control precisely which files to include in analysis and how to analyze them. - 使用模式匹配选择用于 Polyspace 工程的文件
使用带有 glob 模式的表达式选择要包含在 Polyspace 工程或选项文件中的文件。
模块化
- Modularize Polyspace Projects by Using Makefile Builds
Create a separate Polyspace project or options file for each binary in makefile build. - Modularize Polyspace Analysis at Command Line Based on an Initial Interdependency Analysis
Break down Polyspace analysis into smaller and relatively independent modules for faster module verification.
