Inline (-inline)

Задайте функции, которые должны быть клонированы внутренне для каждого вызова функции

Описание

Эта опция влияет на анализ Программы автоматического доказательства Кода только.

Задайте функции, которые верификация должна клонировать внутренне для каждого вызова функции.

Установите опцию

Пользовательский интерфейс (только десктопные решения): В вашей настройке проекта опция доступна на узле Scaling.

Командная строка: Используйте опцию -inline. Смотрите информацию о командной строке.

Почему использование эта опция

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

Не используйте эту опцию, чтобы изучить результаты. Например, предположите, что функция вызвана дважды в вашем коде. Цвет проверки на каждой операции в теле функции является объединенным результатом обоих вызовов. Если вы хотите различать цвета в двух вызовах, используйте опцию Sensitivity context (-context-sensitivity).

Настройки

Никакое значение по умолчанию

Введите имена функций или выберите из списка.

  • Щелкните, чтобы добавить поле и ввести имя функции.

  • Щелкните, чтобы перечислить функции в вашем коде. Выберите функции из списка.

Верификация внутренне клонирует функцию для каждого вызова. Например, если вы задаете функциональный func для встраивания и func называется дважды, программное обеспечение создает две копии func для верификации. Копии называют с помощью соглашения func_pst_inlined_ver где ver номер версии. Вы видите обе копии на панели Call Hierarchy.

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

Красные проверки:

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

  • Если вы используете эту опцию, цвет превращается в темно-оранжевый (показанный с оранжевым восклицательным знаком в списке результатов).

Серые проверки:

  • Обычно, если функция вызвана дважды и 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
Значение: function1[, function2[,...]]
Никакое значение по умолчанию
Пример (Программа автоматического доказательства Кода): Polyspace Code Prover - источники file_name - встройте func1, func2
Пример (Сервер Программы автоматического доказательства Кода): сервер программы автоматического доказательства полипробела кода - источники file_name - встройте func1, func2