main ФункцияПрограмма на C/C + +, которая компилируется в полный исполняемый файл, содержит main функция. Анализ Code Prover обрабатывает main функция отличается от других функций.
main Функция как верхняя часть иерархии вызововCode Prover рассматривает main функционирует как начальная точка верификации. Если вы не предоставляете main функция, например, при проверке библиотеки, верификация генерирует одну. По умолчанию сгенерированный main вызывает функции, которые больше нигде не вызываются.
Затем верификация выполняется из main функция далее в функции, вызываемые из main и так далее вниз по иерархии вызовов.
Чтобы настроить время верификации или точность:
Можно изменить содержимое сгенерированной main использование опций анализа.
Смотрите Код Верификации Prover.
Вы можете писать свои собственные main функция, которая вызывает только те функции, которые вы хотите проверить.
main Аргументы функцииThe main функция может иметь одну из трех форм:
Форма без аргументов:
int main() {}Форма с двумя аргументами:
int main(int argc, char* argv[]) {}Любая другая форма, определяемая реализацией.
В соответствии со спецификациями C/C + + Standard, верификация делает определенные предположения на main аргументы функции. Если на main функция имеет аргументы с типами данных, которые совпадают со второй формой, Code Prover принимает эту форму и накладывает соответствующие ограничения на аргументы. В частности:
Если первый аргумент main функция является целым числом (или typdef в целое число), верификация принимает, что аргумент неотрицателен. Этот аргумент обозначает количество дополнительных аргументов в программу от ее внешнего окружения.
Предположение верно, даже когда main функция имеет только один этот аргумент.
Если первый аргумент является целым числом, а второй аргумент является указателем на указатель (или typedef для одного), верификация принимает, что второму аргументу выделяется буфер размера, равный первому аргументу argc. Каждый элемент буфера, argv[0], argv[1], …, argv[argc-1] также принято, что это инициализированный указатель. Этот аргумент хранит дополнительные аргументы к программе из ее внешнего окружения.