本页面提供的是上一版软件的文档。当前版本中已删除对应的英文页面。
检查 MISRA C:2004 (-misra2)
(已删除)Check for violation of MISRA C:2004 rules
不再支持使用 Code Prover 检查是否存在违反 MISRA C™:2004 规则的情形。请改用 Bug Finder 中的检查 MISRA C:2004 (-misra2)。有关详细信息,请参阅版本历史记录。
描述
设置
默认值:required-rules
- required-rules
检查必需编码规则。
- single-unit-rules
检查仅适用于单个转换单元的规则子集。这些规则在分析的编译阶段进行检查。
- system-decidable-rules
检查
single-unit-rules子集中的规则,以及适用于程序文件集合的某些规则。这些附加规则是在集成级别应用的复杂度较低的规则。由于这些规则涉及多个转换单元,因而只能在集成层面进行检查。这些规则会在分析的编译和链接阶段进行检查。- all-rules
检查必需和建议编码规则。
- SQO-subset1
仅检查 MISRA C 规则的子集。在 Polyspace Code Prover™ 中,遵守这些规则可以减少未经证明的结果数。有关详细信息,请参阅。
- SQO-subset2
检查规则的子集,包括 SQO-subset1 以及某些附加规则。在 Polyspace Code Prover 中,遵守这些规则可以进一步减少未经证明的结果数。有关详细信息,请参阅。
- from-file
指定一个 XML 文件,您可以在其中针对此编码标准配置自定义检查项选择。要创建配置文件,请点击
,然后从检查项选择窗口的右侧窗格中,选择此编码标准中要检查的规则和建议。保存该文件。 要使用或更新某个现有配置文件,请在检查项选择窗口中,在提供的字段中输入该文件的完整路径,或者点击浏览。
如果您将选项设置为 from-file,请启用
使用文件设置检查项 (-checkers-selection-file)。
依赖关系
仅在您将
源代码语言 (-lang)设置为 C 或 C-CPP 时,此选项才可用。对于具有混合 C 和 C++ 代码的工程,MISRA C:2004 检查项仅分析
.c文件。如果您将
源代码语言 (-lang)设置为 C-CPP,则可以激活 C 编码规则检查项和 C++ 编码规则检查项。如果您同时激活 C 和 C++ 编码规则检查项,为避免出现重复结果,Polyspace 不会生成在链接阶段中发现的 C 编码规则(例如 MISRA C:2012 规则 8.3)。
提示
要减少 Polyspace Code Prover 中未经证明的结果,请执行以下操作:
查找 SQO-subset1 中的编码违规。修复您的代码以解决违规并重新运行验证。
查找 SQO-subset2 中的编码违规。修复您的代码以解决违规并重新运行验证。
如果您选择
single-unit-rules或system-decidable-rules选项,并且选择仅检测编码违规,则相较于检查其他规则,分析可以更快完成。有关详细信息,请参阅。
命令行信息
参数:-misra2 |
值:required-rules | all-rules | SQO-subset1 | SQO-subset2 | single-unit-rules | system-decidable-rules | from-file |
示例 (Bug Finder):polyspace-bug-finder -sources |
示例 (Code Prover):polyspace-code-prover -sources |
示例 (Bug Finder Server):polyspace-bug-finder-server -sources |
示例 (Code Prover Server):polyspace-code-prover-server -sources |

