Polyspace-Code-Prover: User Program Error: User should provide a main routine, use -main or -main-generator.

When running Polyspace-Code-Prover, the log file results with:

"User Program Error: User should provide a main routine, use -main or -main-generator."

The project has a "main" function. Not sure what this response means then...

Answer 1

[Anirban]

Hi,

Could you confirm a couple of things:

• The file that has the main function was indeed added to the Polyspace project (if you know which file has the main)? I understand you used polyspace-configure to generate a Polyspace project (or options file) from a Visual Studio project/solution. I just want to confirm that the file containing the main got added in this process.
• Your Visual Studio project has the regular main function that is just called main and not one of the Visual extensions of main like wWinMain? In which case, you have to use the option Main entry point.

[jeremy longstreet]

The solution file(SLN file) for VS is what I placed into the polyspace-config. In that, there are multiple projects that produce Executable files. Most of them do NOT have the problem of missing a 'main' when running PolyspaceCodeProver on them. All of them have the 'main' method in their projects.

This is what I entered at the command line for polyspace-config via a batch file: (the link to the sln file is given here)

polyspace-configure.exe -module -output-options-path C:\xxx\PolyspaceProjects\ "C:\Program Files (x86)\Microsoft Visual Studio\2017\Professional\Common7\IDE\devenv.exe" C:\xxx\Source\TRUNK\Systems\DPM\DPM.sln

PolyspaceBugFinder on each Executable project(about 20 of them(psops) from polyspace-config. And so 20x polyspace-bug-finders are run:

polyspace-bug-finder -options-file c:\xxx\PolyspaceProjects\VS_Project_Y_exe.psopts -options-file "C:\xxx\PolyspaceProjects\BugFinderOptions.psops" -results-dir BugFinderResults_Y_exe

PolyspaceCodeProver on each Executable project(about 20 of them(psops) from polyspace-config. And so 20x polyspace-code-provers are run:

polyspace-code-prover -options-file c:\xxx\PolyspaceProjects\VS_Project_Y_exe.psopts -options-file "C:\xxx\PolyspaceProjects\BugFinderOptions.psops" -results-dir CodeProverResults_Y_exe

The BugFinderOptions.psops contains only: (for simplicity), this is used for both BugFinder and CodeProver.

-checkers all

[Anirban]

Hi,

First, the resolution. You can add the option -main-generator in your options file BugFinderOptions.psops and the error will not happen. The option applies to Code Prover only but it should simply be ignored in the Bug Finder analysis, so you can continue to reuse the same options file.

Now, more about why this might be happening. It is related to your use of -module in the polyspace-configure run. It is probable that one of the Visual Studio projects in the solution leads to a shared library and not an executable. In this case, the project itself would not contain a main function.

If you check your Visual Studio solution (for instance, in VS2019, right-click a project in the Solution Explorer and select Properties), for a library, you will see something like this:

You see that the Configuration Type for zlib is Dynamic Library (.dll). Now, if I used polyspace-configure with -module on the above solution, a separate options file is created solely for zlib. Since zlib is a library that is not meant to execute on its own, it will not have a main function.

It is possible that you have a situation like this. Without exactly going through your solution, it is difficult to say more (you can always contact MathWorks Technical Support to have them diagnose the issue further).

But the workaround is simple: just use -main-generator in the options file. For cases like these where the analysis runs on files, none of which have a main, a main will be generated for you. See more about this option in -main-generator.

[jeremy longstreet]

Looks like the complete option line to add:

-main-generator -main-generator-calls all

Thank you.

[Anirban]

Yes, sorry. Looks like the -main-generator will force you to add the other option.

It might be better to add -main-generator-calls unused so that only functions that are not called anywhere in the project get called by the generated main. This is in fact the default in the Polyspace user interface.

[jeremy longstreet]

I spoke too soon on the other:

"Command line error: No functions available that are out of class scope to call with -main-generator-calls option."

This comes about for both cases:

-main-generator-calls (unused or all)

[Anirban]

Sorry again. I forgot this was C++.

Can you try -class-analyzer all -class-analyzer-calls unused?

The -main-generator-calls is all that is needed in C. But in C++, it looks only at functions defined outside a class scope. See more about the options in -class-analyzer and -class-analyzer-calls.

[jeremy longstreet]

Ran Polyspace-code-prover on a couple projects that had returned the error prior... now it no longer puts out that error message. Thank you.