Exponenta Banner

Верификация программы автоматического доказательства кода

Проверьте целое приложение или модуль

Чтобы задать, проверяете ли вы законченное приложение с функцией main или модулем без функции main, используйте опции верификации Программы автоматического доказательства Кода. Если вы проверяете модуль, программное обеспечение генерирует функцию main для вас. Чтобы подстроить сгенерированную функцию main, используйте эти опции.

Аналитические опции

развернуть все

Verify whole applicationОстановите верификацию, если исходные файлы являются неполными и не содержат основную функцию
Verify module or library (-main-generator)Сгенерируйте основную функцию, если исходные файлы являются модулями или библиотеками, которые не содержат основное
Variables to initialize (-main-generator-writes-variables)Задайте глобальные переменные, которые вы хотите, чтобы сгенерированное основное инициализировало
Initialization functions (-functions-called-before-main)Задайте функции, которые вы хотите, чтобы сгенерированное основное вызвало перед другими функциями
Functions to call (-main-generator-calls)Задайте функции, которые вы хотите, чтобы сгенерированное основное вызвало после функций инициализации
Verify files independently (-unit-by-unit)Проверьте каждый исходный файл независимо от других исходных файлов
Common source files (-unit-by-unit-common-source)Задайте файлы, которые вы хотите включать с каждым исходным файлом во время файла верификацией файла
Main entry point (-main)Задайте Microsoft Visual C++ расширения основного
Analyze class contents only (-class-only)Не анализируйте код кроме методов класса
Skip member initialization check (-no-constructors-init-check)Не проверяйте, инициализирует ли конструктор класса члены класса
Functions to call within the specified classes (-class-analyzer-calls)Задайте методы класса, которые вы хотите проверить
Class (-class-analyzer)Задайте классы, которые вы хотите проверить
Verify model generated code (-main-generator)Укажите, что основная функция должна быть сгенерирована, если она не присутствует в исходных файлах
Parameters (-variables-written-before-loop)Задайте переменные, которые сгенерированное основное должно инициализировать перед циклическим циклом кода
Inputs (-variables-written-in-loop)Задайте переменные, которые сгенерированное основное должно инициализировать в циклическом цикле кода
Initialization functions (-functions-called-before-loop)Задайте функции, которые сгенерированное основное должно вызвать перед циклическим циклом кода
Step functions (-functions-called-in-loop)Задайте функции, которые сгенерированное основное должно вызвать в циклическом цикле кода
Termination functions (-functions-called-after-loop)Задайте функции, которые сгенерированное основное должно вызвать после циклического цикла кода

Темы

Задайте аналитические опции Polyspace

Задайте аналитические опции Polyspace® в пользовательском интерфейсе Polyspace, других IDE-s или скриптах.

Проверьте Приложение C Без основной Функции

Изучите преимущества ручной записи функции main по сравнению с автоматической генерацией функции main.

Проверьте классы C++

Узнать, как, чтобы выполнить верификацию робастности классов так, чтобы это было безопасно для повторного использования.

Обеспечьте контекст для верификации кода С

Изучите, какой внешний контекст можно обеспечить, чтобы сузить предположения верификации по умолчанию.

Обеспечьте контекст для верификации кода С++

Изучите, какой внешний контекст можно обеспечить, чтобы сузить предположения верификации по умолчанию.

Документация Polyspace Code Prover
Поддержка