Exponenta Banner

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

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

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

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

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

Verify whole applicationОстановите верификацию, если исходные файлы являются неполными и не содержат main функция
Show global variable sharing and usage only (-shared-variables-mode)Вычислите совместное использование глобальной переменной и использование, не запуская полный анализ
Verify initialization section of code only (-init-only-mode)Проверяйте один только код инициализации на ошибки времени выполнения и другие проблемы
Verify module or library (-main-generator)Сгенерируйте main функционируйте, если исходные файлы являются модулями или библиотеками, которые не содержат main
Variables to initialize (-main-generator-writes-variables)Задайте глобальные переменные, что вы хотите сгенерированный main инициализировать
Initialization functions (-functions-called-before-main)Задайте функции, что вы хотите сгенерированный main вызывать перед другими функциями
Functions to call (-main-generator-calls)Задайте функции, что вы хотите сгенерированный main вызывать после функций инициализации
Verify files independently (-unit-by-unit)Проверьте каждый исходный файл независимо от других исходных файлов
Common source files (-unit-by-unit-common-source)Задайте файлы, которые вы хотите включать с каждым исходным файлом во время файла верификацией файла
Main entry point (-main)Задайте Microsoft Visual C++ расширения main
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)Укажите что main функция должна быть сгенерирована, если она не присутствует в исходных файлах
Parameters (-variables-written-before-loop)Задайте переменные что сгенерированный main должен инициализировать перед циклическим циклом кода
Inputs (-variables-written-in-loop)Задайте переменные что сгенерированный main должен инициализировать в циклическом цикле кода
Initialization functions (-functions-called-before-loop)Задайте функции что сгенерированный main должен вызвать перед циклическим циклом кода
Step functions (-functions-called-in-loop)Задайте функции что сгенерированный main должен вызвать в циклическом цикле кода
Termination functions (-functions-called-after-loop)Задайте функции что сгенерированный main должен вызвать после циклического цикла кода

Темы

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

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

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

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

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

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

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

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

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

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

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