-context-sensitivity)Сохраните контекстную информацию вызова, чтобы идентифицировать вызов функции, который вызвал ошибки
Эта опция влияет на анализ Программы автоматического доказательства Кода только.
Задайте функции, для которых верификация должна сохранить контекстную информацию вызова. Если функция вызвана многократно, использование этой опции помогает вам различать различные вызовы.
Пользовательский интерфейс (только десктопные решения): В вашей настройке проекта опция доступна на узле Precision.
Командная строка: Используйте опцию -context-sensitivity. Смотрите информацию о командной строке (Polyspace Code Prover).
Предположим, что функция вызвана дважды в вашем коде. Цвет проверки на каждой операции в теле функции является объединенным результатом обоих вызовов. Если вы хотите различать цвета в двух вызовах, используйте эту опцию.
Например, если функция содержит красную или оранжевую проверку и зеленую проверку на той же операции для двух различных вызовов, программное обеспечение комбинирует контексты и отображает оранжевую проверку на операции. Если вы используете эту опцию, проверка становится темно-оранжевой, и детали результата показывают цвет проверки на каждый вызов.
Значение по умолчанию: none
none Программное обеспечение не хранит контекстную информацию вызова для функций.
auto Хранилища программного обеспечения вызывают контекстную информацию для регистраций:
Функции, которые формируют листы дерева вызова. Эти функции вызваны другими функциями, но не вызывают сами функции.
Небольшие функции. Программное обеспечение использует внутренний порог, чтобы определить, мала ли функция.
customХранилища программного обеспечения вызывают контекстную информацию для функций, которые вы задаете. Чтобы ввести имя функции, щелкнуть
.
Если вы выбираете эту опцию, вы не видите подсказки в теле функций, которые извлекают выгоду из этой опции (и разделяют контексты вызова).
Если вы выбираете эту опцию, анализ может отобразить некоторые операции кода серым (недостижимый код), даже когда можно идентифицировать продвижение путей к выполнению к операциям. В этом случае код Грея указывает на операции, которые могут быть недостижимыми только в конкретном контексте вызова.
Например, предположите, что эта функция вызвана с аргументами-1 и 1:
int isPositive (int num) {
if(num < 0)
return 0;
return 1;
}Проверка на if серо потому что, когда функция вызвана с аргументом-1, if условие всегда верно.
Проверка на коде в if ветвь сера потому что, когда функция вызвана с аргументом 1, if условие является всегда ложным.
Каждая недостижимая проверка кода указывает на код, который недостижим только в конкретном контексте вызова. Вы видите контекст вызова в деталях результата.
Параметр: -context-sensitivity |
Значение: |
Значение по умолчанию: none |
Пример (Программа автоматического доказательства Кода): Polyspace Code Prover - источники |
Пример (Сервер Программы автоматического доказательства Кода):
сервер программы автоматического доказательства полипробела кода - источники |
Чтобы позволить программному обеспечению определять, какие функции получают устройство хранения данных контекста вызова, используйте опцию -context-sensitivity-auto.