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