配置库验证

配置 Polyspace® Code Prover™ 分析以验证不含 main() 的库

指定选项以设置 Code Prover，将不含 main 的代码作为库进行分析。如果您要验证模块，该软件会为您生成一个 main 函数。要微调生成的 main 函数，请使用这些选项。

Polyspace 选项

全部展开

验证整个应用程序如果源文件不完整且未包含 main 函数，则停止验证
仅显示全局变量共享和使用情况 (-shared-variables-mode)在不运行完整分析的情况下，计算全局变量的共享和使用情况
仅验证初始化代码段 (-init-only-mode)Check initialization code alone for run-time errors and other issues
验证模块或库 (-main-generator)如果源文件是未包含 main 的模块或库，则生成一个 main 函数
要初始化的变量 (-main-generator-writes-variables)Specify global variables that you want the generated main to initialize
初始化函数 (-functions-called-before-main)指定您希望生成的 main 在其他函数之前调用的函数
要调用的函数 (-main-generator-calls)Specify functions that you want the generated main to call after the initialization functions
独立验证文件 (-unit-by-unit)Option to verify each source file independently of other source files
常用源文件 (-unit-by-unit-common-source)Specify files that you want to include with each source file during a file by file verification
主入口函数 (-main)指定 main 的 Microsoft Visual C++ 扩展
仅分析类内容 (-class-only)不分析类方法以外的代码
跳过成员初始化检查 (-no-constructors- init-check)Do not check if class constructor initializes class members
指定类内要调用的函数 (-class-analyzer-calls)Specify class methods that you want to verify
类 (-class-analyzer)Specify classes that you want to verify
验证模型的生成代码 (-main-generator)指定如果在源文件中不存在 main 函数，则必须生成该函数
参数 (-variables-written-before-loop)指定生成的 main 在有环代码循环之前必须初始化的变量
输入 (-variables-written-in-loop)指定生成的 main 在有环代码循环中必须初始化的变量
初始化函数 (-functions-called-before-loop)指定生成的 main 在有环代码循环之前必须调用的函数
单步函数 (-functions-called-in-loop)指定生成的 main 在有环代码循环中必须调用的函数
终止函数 (-functions-called-after-loop)指定生成的 main 在有环代码循环之后必须调用的函数
-main-generator-bounded-loopGenerate a main that calls functions in a loop with a specific number of iterations (自 R2022a 起)

主题