验证模块或库 (`-main-generator`)

如果源文件是未包含 main 的模块或库，则生成一个 main 函数

描述

此选项仅影响 Code Prover 分析。

指定当 Polyspace^® 在源文件中未找到 main 函数时必须生成该函数。

使用以下方法之一设置选项：

有关适用于模型生成的代码的类似选项，请参阅验证模型的生成代码 (-main-generator)。

如果您要验证模块或库，请使用此选项。Code Prover 分析需要 main 函数。在验证模块或库时，您的代码可能没有 main。

使用此选项时，如果不存在 main 函数，则 Code Prover 将生成该函数。如果存在 main，则分析将使用现有的 main。

开启（默认值）

当 Polyspace 在源文件中未找到 main 函数时将生成该函数。生成的 main：

初始化由要初始化的变量 (-main-generator-writes-variables) 选项指定的变量。
在调用其他函数之前，先调用由初始化函数 (-functions-called-before-main) 选项指定的函数。
按所有可能的顺序，调用由要调用的函数 (-main-generator-calls) 选项指定的函数。
（仅限 C++）调用由类 (-class-analyzer) 选项和指定类内要调用的函数 (-class-analyzer-calls) 选项指定的类方法。

如果您未指定上述函数和变量选项，则生成的 main 将执行以下操作：

初始化所有全局变量（使用关键字 const 和 static 声明的全局变量除外）。
按所有可能的顺序，调用在源文件中任何位置都未调用的所有函数。Polyspace 认为可以在两个连续的函数调用之间写入全局变量。因此，在每个被调函数中，全局变量最初都具有其类型所允许的完整范围的值。

关闭

如果源文件中不存在 main 函数，则 Polyspace 将停止

如果源文件中存在 main 函数，则验证将使用该 main 函数，无论您是启用还是禁用了此选项。
只有当您的源文件中不存在 main 函数时，此选项才有意义。
如果您使用验证整个应用程序选项（命令行中的默认选项），则您的代码必须包含 main 函数。否则，您会看到以下错误：
Error: required main procedure not found
如果您的代码未包含 main 函数，请使用此选项来生成 main 函数。
如果您指定多任务选项，则验证会忽略您的 main 生成设定。相反，验证将引入一个空的 main 函数。
有关多任务选项的详细信息，请参阅手动配置 Polyspace 多任务分析。

参数：-main-generator

默认值：关闭

示例 (Code Prover)：polyspace-code-prover -sources file_name -main-generator

示例 (Code Prover Server)：polyspace-code-prover-server -sources file_name -main-generator