-inline)Задайте функции, которые должны быть клонированы внутренне для каждого вызова функции
Эта опция влияет на анализ Программы автоматического доказательства Кода только.
Задайте функции, которые верификация должна клонировать внутренне для каждого вызова функции.
Пользовательский интерфейс (только десктопные решения): В вашей настройке проекта опция доступна на узле Scaling.
Командная строка: Используйте опцию -inline. Смотрите информацию о Командной строке.
Используйте эту опцию экономно. Иногда, использование опции помогает работать вокруг масштабирования проблем во время верификации. Если ваша верификация занимает слишком много времени, Техническая поддержка может попросить, чтобы вы использовали эту опцию для определенных функций.
Не используйте эту опцию, чтобы понять результаты. Например, предположите, что функция вызвана дважды в вашем коде. Цвет проверки на каждой операции в теле функции является объединенным результатом обоих вызовов. Если вы хотите различать цвета в двух вызовах, используйте опцию Sensitivity context (-context-sensitivity).
Никакое значение по умолчанию
Введите имена функций или выберите из списка.
Щелкните
, чтобы добавить поле и ввести имя функции.
Щелкните
, чтобы перечислить функции в вашем коде. Выберите функции из списка.
Верификация внутренне клонирует функцию для каждого вызова. Например, если вы задаете функциональный func для встраивания, и func называется дважды, программное обеспечение создает две копии func для верификации. Копии называют с помощью соглашения func_pst_inlined_verver
Однако для каждой проверки на этапе выполнения в теле функции, вы видите, что только один окрашивает ваши результаты верификации. Семантика цвета проверки отличается от нормальной спецификации.
Красные проверки:
Обычно, если функция вызвана дважды, и операция вызывает определенную ошибку только в одном из вызовов, цвет проверки является оранжевым.
Если вы используете эту опцию, худший цвет показывают для проверки. Поэтому проверка является красной.
Серые проверки:
Обычно, если функция вызвана дважды, и ответвление оператора if недостижимо в только одном из вызовов, ответвление показывают как достижимое.
Если вы используете эту опцию, худший цвет показывают для проверки. Поэтому ответвление if кажется серым.
Не используйте эту опцию, чтобы понять результаты. Используйте эту опцию, только если определенная функция вызывает масштабирующиеся проблемы.
Используйте эту опцию, чтобы идентифицировать причину ошибки Non-terminating call.
Ситуация: Иногда, красная проверка Non-terminating call может появиться на вызове функции, хотя красная проверка не появляется в теле функции. Тело функции представляет все вызовы функции. Поэтому, если некоторые вызовы функции не вызывают ошибку, оранжевая проверка появляется в теле функции.
Действие: Если вы используете эту опцию для каждого вызова функции, существует соответствующее тело функции. Поэтому можно проследить красную проверку на вызове функции к красной регистрации тела функции.
Используя эту опцию может иногда копировать много кода и приводить к масштабирующимся проблемам. Поэтому выберите функции, чтобы встроить тщательно.
Выберите функции, чтобы встроить на основе подсказок, обеспеченных верификацией псевдонима.
Не используйте эту опцию для функций точки входа, включая 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 |
Значение: |
| Никакое значение по умолчанию |
Пример (программа автоматического доказательства кода): |
Пример (сервер программы автоматического доказательства кода):
|