Code Prover 验证

验证整个应用程序或模块

要指定您需要验证的是包含 main 函数的完整应用程序还是不包含 main 函数的模块，请使用 Code Prover 验证选项。如果您要验证模块，该软件会为您生成一个 main 函数。要微调生成的 main 函数，请使用这些选项。

Polyspace 选项

全部展开

验证整个应用程序如果源文件不完整且未包含 main 函数，则停止验证
仅显示全局变量共享和使用情况 (-shared-variables-mode)Compute global variable sharing and usage without running full analysis
仅验证初始化代码段 (-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)Specify functions that you want the generated main to call ahead of other functions
要调用的函数 (-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)Do not analyze code other than class methods
跳过成员初始化检查 (-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)Specify variables that the generated main must initialize before the cyclic code loop
输入 (-variables-written-in-loop)Specify variables that the generated main must initialize in the cyclic code loop
初始化函数 (-functions-called-before-loop)Specify functions that the generated main must call before the cyclic code loop
单步函数 (-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

主题