Verify C Application Without main Function

Verify C Application Without `main` Function

Polyspace^® verification requires that your code must have a main function. You can do one of the following:

Provide a main function in your code.
Specify that Polyspace must generate a main.

Generate `main` Function

Before verification, specify one of the following options. In the user interface of the Polyspace desktop products, the options appear under the Code Prover Verification node.

Option Description

Option	Description
`Verify whole application`	The verification stops if the software does not detect a `main`.
`Verify module or library (-main-generator)`	Before verification, Polyspace checks if your code contains a `main` function. If a `main` function exists, the software uses that `main`. Otherwise, the software generates a `main` using the options that you specify: `Variables to initialize (-main-generator-writes-variables)` `Initialization functions (-functions-called-before-main)` `Functions to call (-main-generator-calls)`

Verify whole application

The verification stops if the software does not detect a main.

Verify module or library
                                    (-main-generator)

Before verification, Polyspace checks if your code contains a main function.

If a main function exists, the software uses that main. Otherwise, the software generates a main using the options that you specify:

Manually Write `main` Function

During automatic main generation, the software makes certain assumptions about the function call sequence or behavior of global variables. For instance, the default automatically generated main models the following behavior:

The functions that you specify using the option Functions to call (-main-generator-calls) can be called in arbitrary order.
In the beginning of each function body, global variables can have the full range of values allowed by their type.

To provide a more accurate model of the call sequence, you can manually write a main function for the purposes of verification. You can add this main function in a separate file to your project. In some cases, providing an accurate call sequence can reduce the number of orange checks. For example, in the following code, Polyspace assumes that f and g can be called in any order. Therefore, it produces an orange overflow for the case when f is called before g. If you know that f is called after g, you can write a main function to model this sequence.

static char x;
static int y;

void f(void)
{
    y = 300;
}

void g(void)
{
    x = y; 
}

Example 1: main Calls One Function Before Another

Suppose you want to verify two functions func1 and func2 that have the following prototypes.

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

You have the requirement that func1 is always called before func2.

To manually define a main that models this behavior:

Write a main containing declarations of a volatile variable for each function parameter type.
Write a loop with a volatile termination condition.
The verification assumes that a volatile variable can have any value allowed by its type. Because the loop potentially terminates after any run, this condition models the fact that you call func1 and func2 an arbitrary number of times.
Inside this loop, call func2 after func1.

You can write the following main:

void main()
{
    volatile int random=0; 
    volatile void * volatile ptr;
    while(random) 
    {
        random = func1(ptr, random);
        func2(random, random); 
    }
}

Example 2: main Calls One Function 10 Times Before Another

Suppose you want to verify two functions func1 and func2 with the following prototypes:

void func1(int);
void func2(void);

You know that when both func1 and func2 are called, func1 is always called 10 times before func2.

To manually define a main that models this behavior:

Write a main containing declarations of a volatile variable for each function parameter type.
In your main function, call func1 in a loop 10 times before func2.

For instance, you can write the following main:

void main(void) {
    int i=0;
    volatile int random=0;
    
    while (++i <= 10)
        func1(random);

    func2();

}