Verifying a C Application Without a "Main"

Main Generator Overview

When your application is a function library (API) or a single module, you must provide a main that calls each function because of the execution model used by Polyspace verification. You can either manually provide a main, or have Polyspace software generate one for you automatically.

When you run a verification on Polyspace Client for C/C++ software, the main is always generated. When you run a verification on Polyspace Server for C/C++ software, you can choose to automatically generate a main by selecting the Generate a main (-main-generator) option.

Polyspace Client for C/C++ Main Generator

The Polyspace Client for C/C++ product automatically checks your code for a main.

• If a main exists in the set of files, the verification uses that main.

• If a main does not exist, the tool generates a main using the options you specify.

Polyspace Server for C/C++ Main Generator

If you do not select the -main-generator option, a Polyspace Server for C/C++ verification stops if it does not detect a main. This behavior can help isolate files missing from the verification.

When you select the -main-generator option, the Polyspace Server for C/C++ product checks your code for a main.

• If a main exists in the set of files, the verification uses that main.

• If a main does not exist, the tool generates a main using the options you specify.

Back to Top

Automatically Generating a Main

When you run a client verification, or a server verification using the Generate a main (-main-generator) option, the software automatically generates a main.

The generated main has the following behavior.

1. It initializes any variables identified by the option -variables written-before-loop.

2. It calls any functions specified by the option -functions-called-before-loop. This could be considered an initialization function.

3. It initializes any variables identified by the option -variables written-in-loop.

4. It calls any functions specified by the option -functions-called-in-loop.

5. It calls any functions specified by the option -functions-called-after-loop. This could be a terminate function for a cyclic program.

For more information on the main generator, see Main Generator Behavior for Polyspace Software.

Main for Generated Code

The following example shows how to use the main generator options to generate a main for a cyclic program, such as code generated from a Simulink model.

init parameters		\\ -variables-written-before-loop
init_fct()				\\ -functions-called-before-loop
	while(1){			\\ start main loop
	init inputs			\\ -variables-written-in-loop
	step_fct()			\\ -functions-called-in-loop
}
terminate_fct()		\\ -functions-called-after-loop

Back to Top

Manually Generating a Main

Manually generating a main is often preferable to an automatically generated main, because it allows you to provide a more accurate model of the calling sequence to be generated.

There are three steps involved in manually defining the main.

1. Identify the API functions and extract their declaration.

2. Create a main containing declarations of a volatile variable for each type that is mentioned in the function prototypes.

3. Create a loop with a volatile end condition.

4. Inside this loop, create a switch block with a volatile condition.

5. For each API function, create a case branch that calls the function using the volatile variable parameters you created.

Consider the following example. Suppose that the API functions are:

int func1(void *ptr, int x);
void func2(int x, int y);

You should create the following main:7

void main()
{
volatile int random; /* We need an integer variable as a function
parameter */
volatile void * volatile ptr; /* We need a void pointer as a function
parameter */
while (random) {
	switch (random) {
	case 1:
		random = func1(ptr, random); break; /* One API function call */
	default:
		func2(random, random); /* Another API function call */
	}
}

Back to Top

Specifying Call Sequence

Polyspace software verifies every function in any order. This means that in some particular situations, a function "f" might be called before a function "g". In the default usage, Polyspace verification assumes that "f" and "g" can be called in any order. If some actions set by "f" must be executed before "g" is called, writing a main which will call "f" and "g" in the exact order will bring a higher selectivity.

Colored Source Code Example

With the default launching mode of Polyspace verification, no problem will be highlighted on the following example. With a bit of setup, more bugs can be found.

static char x;
static int y;

void f(void)
{
y = 300;
}

void g(void)
{
x = y; // red or green OVFL?
}

With knowledge of the relative call sequence between g and f: if g is called first, the assignment is green, otherwise its red. Thanks to the exact call order, an attempt to place 300 in a char fails, displaying a red.

Example of Call Sequence

void main(void)
{
f()
g()
}

Simply create a main that calls in the desired order the list of functions from the module.

Back to Top

Specifying Functions Not Called by Generated Main

You can specify source files in your project that the main generator will ignore. Functions defined in these source files are not called by the automatically generated main.

Use this option for files containing function bodies, so that the verification looks for the function body only when the function is called by a primary source file and no body is found.

Note   This option applies only to automatically generated mains. Therefore, you must also select the option Generate a main (-main-generator) for this option to take effect.

To specify a source file as not called by the main generator:

1. In the Project Browser Source tree, select the source files you want the main generator to ignore.

2. Right click any selected file, and select Define As > Not Called by Main Generator.

   

   The files ignored by the main generator appear is italics in the Source tree of the project.

   

Note   To specify that a file previously marked Not Called by Main Generator should be called, right-click the file in the project Source tree, then select Regular Source File.

Back to Top

Main Generator Assumptions

When using the automatic main generator to verify a specific function, the objective is to find problems with the function. To do this, the generated main makes assumptions about parameters so that you can focus on run-time errors (red, gray and orange) that are related to the function.

The main generator makes assumptions about the arguments of called functions to reduce the number of orange checks in the results. Therefore, when you see an orange check in your results, it is likely to be due to the function, not the main.

However, green checks are computed with the same assumptions. Therefore, you should be cautious of green checks involving the main, especially when conducting unit-by-unit verification.

Back to Top

Setting Up a Target

Polyspace C++ Class Analyzer