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

Сгенерируйте main Функция

Перед верификацией задайте одну из следующих опций. В пользовательском интерфейсе десктопных решений Polyspace опции появляются под узлом Code Prover Verification.

Вручную запишите 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();

}