主要内容

指定代码行为

指定代码行为(例如变量范围、库使用情况和其他信息),以减少 Polyspace® Bug Finder™ 分析中的假正和假负结果

为了减少假正和假负结果,请提供有关您代码的更多信息。例如:

使用此处列出的分析选项,向 Polyspace Bug Finder 更详细地描述您的代码,这有助于提高分析精度并加快分析速度。

Polyspace 选项

全部展开

约束设置 (-data-range-specifications)对桩函数的全局变量、函数输入和返回值进行约束
使用的库 (-library)Specify libraries that you use in your program
-code-behavior-specificationsAssociate behaviors with code elements such as functions
-classificationControl precisely which files to include in Polyspace analysis and how to analyze them (自 R2023a 起)
-asm-begin -asm-end将编译器特定的 asm 函数排除在分析之外
有效布尔类型 (-boolean-types)Specify data types that coding rule checker must treat as effectively Boolean
允许的 pragma (-allowed-pragmas)Specify pragma directives that are documented
要插桩的函数 (-functions-to-stub)在分析期间指定要插桩的函数
-termination-functions指定进程终止函数
验证时限 (-timeout)Specify a time limit on your analysis
校验模型的生成代码 (-main-generator)指定如果在源文件中不存在 main 函数,则必须生成该函数
参数 (-variables-written-before-loop)指定生成的 main 在有环代码循环之前必须初始化的变量
输入 (-variables-written-in-loop)指定生成的 main 在有环代码循环中必须初始化的变量
初始化函数 (-functions-called-before-loop)指定生成的 main 在有环代码循环之前必须调用的函数
单步函数 (-functions-called-in-loop)Specify functions that the generated main must call in the cyclic code loop
终止函数 (-functions-called-after-loop)Specify functions that the generated main must call after the cyclic code loop

主题

提供更多信息

指定外部约束