验证整个应用程序

如果源文件不完整且未包含 main 函数，则停止验证

描述

此选项仅影响 Code Prover 分析。

此选项不适用于从 MATLAB^® 代码或 Simulink^® 模型生成的代码。

指定如果源文件中不存在 main 函数，则 Polyspace^® 验证必须停止。

如果您为编译器 (-compiler) 选择 Visual C++^® 设置，则可以指定必须将哪个函数视为 main。请参阅主入口函数 (-main)。

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

打开: 如果 Polyspace 在源文件中未找到 main 函数，验证将停止。
关闭（默认值）: 当源文件中不存在 main 函数时，Polyspace 会继续进行验证。如果 main 不存在，它会生成一个包含 main 函数的 __polyspace_main.c 文件。

如果您使用此选项，则您的代码必须包含一个 main 函数。否则，您会看到以下错误：

Error: required main procedure not found

如果您的代码未包含 main 函数，请使用验证模块或库 (-main-generator) 选项来生成 main 函数。

与用户界面不同的是，默认情况下，如果它在源文件中未找到 main 函数，从命令行发起的验证将停止。如果您指定 -main-generator 选项，当 Polyspace 在源文件中无法找到 main 函数时将生成该函数。