Inline (-inline)

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

Описание

Эта опция влияет только на анализ Code Prover.

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

Задать опцию

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

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

Зачем использовать эту опцию

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

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

Настройки

По умолчанию нет

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

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

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

Внутренняя верификация клонирует функцию для каждого вызова. Например, если вы задаете функцию func для встраивания и func вызывается дважды, программное обеспечение внутренне создает две копии func для верификации.

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

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

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

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

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

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

  • Если вы используете эту опцию, для проверки отображается худший цвет. Поэтому if ветвь выглядит серой.

Ниже каждой сдачи на хранение встроенной функции отображается информация, относящаяся к каждому контексту вызова. Например, если происходит темно-оранжевая Division by zero, поскольку определенный вызов функции приводит к определенному делению на нули, можно идентифицировать вызов вместе со значениями, вытекающими из этого вызова.

Polyspace results for inlined functions

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

Совет

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

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

  • Не используйте эту опцию для функций точки входа, включая 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[,...]]
По умолчанию нет
Пример (Code Prover): Polyspace Code Prover -sources file_name -inline func1, func2
Пример (Код Prover Server): Полипространство -code-prover-server -sources file_name -inline func1, func2