Документация

Произвести main Функция

Перед проверкой укажите один из следующих параметров. В пользовательском интерфейсе настольных продуктов Polyspace параметры отображаются в узле Проверка проверочного кода.

Запись вручную main Функция

Во время автоматического main генерация, программное обеспечение делает определенные предположения относительно последовательности вызова функции или поведения глобальных переменных. Например, автоматически генерируется значение по умолчанию main моделирует следующее поведение:

Для обеспечения более точной модели последовательности вызовов можно вручную записать main функция для целей проверки. Вы можете добавить это main в отдельном файле для проекта. В некоторых случаях обеспечение точной последовательности вызовов может уменьшить количество проверок оранжевого цвета. Например, в следующем коде Polyspace предполагает, что f и g может вызываться в любом порядке. Поэтому возникает оранжевое переполнение для случая, когда f вызывается до g. Если вы знаете, что f вызывается после g, вы можете написать main для моделирования этой последовательности.

static char x;
static int y;

void f(void)
{
    y = 300;
}

void g(void)
{
    x = y; 
}

 Пример 1: main Вызов одной функции перед другой

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

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

 Пример 2: main Вызов одной функции 10 раз раньше другой

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

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

    func2();

}