How do I use Polyspace Code Prover for a project with multiple "main" functions?

In my project, I have several main functions. When using Polyspace Code Prover, I receive the following error in Polyspace:

Error: main procedure multiply defined

and the analysis is stopped.

What is the reason of this message and how can I resolve this?

Answer 1

[MathWorks Support Team]

Reminder on the two modes of verification about Code Prover:

In the "Whole Application" mode, the tool analyzes the complete executable program. Therefore, it needs the full application source code and a unique entry point (main) from which all execution paths can be explored. The analysis builds the entire call graph starting from this main function, so the code provided should represent a complete application with a single entry point. 

See https://www.mathworks.com/help/codeprover/ref/verifywholeapplication.html

and https://www.mathworks.com/help/codeprover/ref/assumptions-about-main-function.html

The "Module or Library" mode is when no main is provided to the analysis, for example if the code represents a part of the whole application, or if the source code is the code of a library.  See https://www.mathworks.com/help/codeprover/ug/verifying-a-c-application-without-a-main.html

In this mode, a main will be automatically created. 

See https://www.mathworks.com/help/codeprover/ref/verifymoduleorlibrarymaingenerator.html

The generated main will then be the unique entry point in the analysis.

When multiple main functions are detected, since Polyspace Code Prover has no knowledge of the application's architecture or intended build configuration, it cannot automatically determine which main function should be used as the entry point. That's why the analysis stops.

There are several reasons why a project may contain multiple main functions. For example, the source code may support multiple build targets, each with its own entry point, or it may include test harnesses and unit test code alongside the production application.

In such situations, it is the customer's responsibility to configure the project to have only one main in the analysis.

There are several ways to do so, depending on the situation.

For example, if there are files that are not part of the target application, such as test sources, they should be excluded from the analysis.

Another suggestion is to keep the mains but then to create modules (if Polyspace is used before R2026a) or projects in the Polyspace Platform UI.

With the Polyspace Platform user interface, projects are used to organize related analyses into separate projects within a workspace: Manage Related Projects Using Workspaces

If polyspace-configure is used to create the project, projects can be generated automatically to help structure the analysis: polyspace-configure Reference

Another possibility is to keep only one main and rename the other ones.

1. Analyze each "main" function separately.

2. Rename the functions just for their use in Polyspace, while keeping their name as "main" for all other uses. Do this by inserting unique names, such as “main1" and "main2", inside a ‘#ifdef POLYSPACE’ - ‘#else’ - ‘#endif’ preprocessor. For example, you can add the wrapper below to your "main" functions:

#ifdef POLYSPACE
int psN_main(int argc, int *argv[])
#else
int main(int argc, int *argv[])
#endif 

{
   // main function implementation
   return 0;
}

        where N is a number 1-3 (according to your files). Polyspace defined the “POLYSPACE” macro when you run Code Prover analysis on your project with the recommended options, so it defines the function as "psN_main".

Then, you can run the analysis with the "-main-generator" with "-main-generator-calls all" options as shown below:

polyspace-code-prover -sources SubDir1\File1.c,SubDir2\File2.c,SubDir3\File3.c -main-generator -main-generator-calls all

        This will generate a new "main" function that calls all functions except inlined ones, and Polyspace will use this generated "main" for its analysis. For more information on these options, including how to set them using the Polyspace user interface, please refer to the documentation pages below:

• -main-generator:

                https://www.mathworks.com/help/releases/R2024a/codeprover/ref/verifymoduleorlibrarymaingenerator.html

• -main-generator-calls:

                https://www.mathworks.com/help/releases/R2024a/codeprover/ref/functionstocallmaingeneratorcalls.html