-inline)Задайте функции, которые должны быть клонированы внутренне для каждого вызова функции
Эта опция влияет на анализ Программы автоматического доказательства Кода только.
Задайте функции, которые верификация должна клонировать внутренне для каждого вызова функции.
Пользовательский интерфейс (только десктопные решения): В вашей настройке проекта опция доступна на узле Scaling.
Командная строка и файл опций: Используйте опцию -inline. Смотрите информацию о командной строке.
Используйте эту опцию экономно. Иногда, использование опции помогает работать вокруг масштабирования проблем во время верификации. Если ваша верификация занимает слишком много времени, Техническая поддержка может попросить, чтобы вы использовали эту опцию для определенных функций.
Не используйте эту опцию, чтобы изучить результаты. Например, предположите, что функция вызвана дважды в вашем коде. Цвет проверки на каждой операции в теле функции является объединенным результатом обоих вызовов. Если вы хотите различать цвета в двух вызовах, используйте опцию Sensitivity context (-context-sensitivity).
Никакое значение по умолчанию
Введите имена функций или выберите из списка.
Щелкните
, чтобы добавить поле и ввести имя функции.
Щелкните
, чтобы перечислить функции в вашем коде. Выберите функции из списка.
Верификация внутренне клонирует функцию для каждого вызова. Например, если вы задаете функциональный func для встраивания и func называется дважды, программное обеспечение внутренне создает две копии func для верификации.
Однако для каждой проверки на этапе выполнения в теле функции, вы видите, что только один окрашивает ваши результаты верификации. Семантика цвета проверки отличается от нормальной спецификации.
Красные проверки:
Обычно, если функция вызвана дважды, и операция вызывает определенную ошибку только в одном из вызовов, цвет проверки является оранжевым.
Если вы используете эту опцию, цвет превращается в темно-оранжевый (показанный с оранжевым восклицательным знаком в списке результатов).
Серые проверки:
Обычно, если функция вызвана дважды и if ветвь оператора недостижима в только одном из вызовов, ветвь показывают как достижимая.
Если вы используете эту опцию, худший цвет показывают для проверки. Поэтому if ветвь кажется серой.
Ниже каждой регистрации встроенной функции вы видите информацию, характерную для каждого контекста вызова. Например, если темно-оранжевый Division by zero происходит, потому что определенный вызов функции приводит к определенному делению на нуль, можно идентифицировать вызов наряду со значениями, следующими из того вызова.
Не используйте эту опцию, чтобы изучить результаты. Используйте эту опцию, только если определенная функция вызывает масштабирующиеся проблемы.
Используя эту опцию может иногда копировать много кода и приводить к масштабирующимся проблемам. Поэтому выберите функции, чтобы встроить тщательно.
Выберите функции, чтобы встроить на основе подсказок, обеспеченных верификацией псевдонима.
Не используйте эту опцию для функций точки входа, включая main.
Используя эту опцию может увеличить число серых проверок Unreachable code.
Например, в следующем коде, если вы вводите max для Inline вы получаете две проверки Unreachable code, один для каждого вызова max.
int max(int a, int b) {
return a > b ? a : b;
}
void main() {
int i=3, j=1, k;
k=max(i,j);
i=0;
k=max(i,j);
}Если вы используете ключевое слово inline перед функциональным определением поместите определение в заголовочный файл и вызовите функцию от нескольких исходных файлов, у вас есть тот же результат как использование опции Inline.
Для Кода С++ эта опция применяется ко всем перегруженным методам класса.
Параметр: -inline |
Значение: |
| Никакое значение по умолчанию |
Пример (Программа автоматического доказательства Кода): Polyspace Code Prover - источники |
Пример (Сервер Программы автоматического доказательства Кода):
сервер программы автоматического доказательства полипробела кода - источники |