mainВерификация Polyspace® требует, чтобы ваш код имел функцию main. Можно выполнить одно из следующих действий:
Обеспечьте функцию main в своем коде.
Укажите, что Polyspace должен сгенерировать main.
mainПеред верификацией задайте одну из следующих опций. В пользовательском интерфейсе десктопных решений Polyspace опции появляются под узлом Code Prover Verification.
| Опция | Описание |
|---|---|
Verify whole application | Верификация останавливается, если программное обеспечение не обнаруживает |
Verify module or library (-main-generator) | Перед верификацией Polyspace проверяет, содержит ли ваш код функцию Если функция
|
mainВо время автоматической генерации main программное обеспечение делает определенные предположения о последовательности вызова функции или поведении глобальных переменных. Например, значение по умолчанию автоматически сгенерировало модели main следующее поведение:
Функции, что вы задаете использование опции Functions to call (-main-generator-calls), могут быть вызваны в произвольном порядке.
В начале каждого тела функции глобальные переменные могут иметь полный спектр значений, позволенных их типом.
Чтобы предоставить более точную модель последовательности вызова, можно вручную записать функцию 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;
}