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