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