Панель Orange Sources показывает неограниченные источники, такие как энергозависимые переменные и заблокированные функции, которые могут привести к нескольким оранжевым проверкам (бездоказательные результаты) в анализе Программы автоматического доказательства Кода. Если вы ограничиваете оранжевый источник, можно обратиться к нескольким оранжевым проверкам вместе. Чтобы видеть панель Orange Sources, нажмите
кнопку на панели Result Details.
Источники по существу указывают на переменные, значения которых не могут быть определены из вашего кода. Переменные могут быть входными параметрами функций, контекст вызова которых является неизвестными или возвращаемыми значениями неопределенных функций. Программа автоматического доказательства кода принимает, что эти переменные берут полный спектр значений, позволенных их типом данных. Это широкое предположение может привести к одной или нескольким оранжевым регистрациям последующего кода.
Например, в этом примере, если функциональный random_float не задан, вы видите три оранжевых проверки Overflow.
static void Close_To_Zero(void)
{
float xmin = random_float();
float xmax = random_float();
float y;
if ((xmax - xmin) < 1.0E-37f) { /* Overflow 1 */
y = 1.0f;
} else {
/* division by zero is impossible here */
y = (xmax + xmin) / (xmax - xmin); /* Overflows 2 and 3 */
}
}
random_float поэтому оранжевый источник, который вызывает самое большее три оранжевых проверки.Используя панель Orange Sources, вы можете:
Рассмотрите все оранжевые проверки, происходящие из того же источника.
В предыдущем примере, если вы выбираете функциональный random_float, список результатов показывает только три оранжевых проверки, вызванные этим источником. Смотрите, что Фильтр Использует Оранжевые Источники.
Ограничьте переменные диапазоны путем определения внешних ограничений или через дополнительный код. Ограничение области значений оранжевого источника может удалить несколько оранжевых проверок, которые прибывают из сверхприближения. Остающиеся оранжевые проверки указывают на действительные проблемы в вашем коде.
В предыдущем примере можно ограничить возвращаемое значение random_float.
Для эффективного анализа кликните по заголовку столбца Max Oranges, чтобы отсортировать оранжевые источники по количеству оранжевых проверок, которые следуют из источника. Ограничьте источники с большим количеством оранжевых проверок прежде, чем заняться другими.
То, как вы ограничиваете переменные диапазоны и работаете вокруг предположений Polyspace® по умолчанию, зависит от типа оранжевого источника:
Если определение функции не доступно для анализа Polyspace, функция заблокирована. Анализ делает несколько предположений о заблокированных функциях. Например, возвращаемое значение заблокированной функции может принять любое значение, позволенное его типом данных.
Смотрите Заблокированные Функции для предположений о заблокированных функциях и как работать вокруг них.
Если переменная объявляется с volatile спецификатор, анализ принимает, что переменная может принять любое значение, позволенное его типом данных в любой точке в коде.
Смотрите Энергозависимые Переменные, чтобы работать вокруг вокруг этого предположения.
Если переменная объявляется с extern спецификатор, но не заданный в другом месте в коде, анализ принимает, что переменная может принять любое значение в своей области значений типа данных, прежде чем это будет сначала присвоено.
Определите, где переменная задана и почему определение не доступно для анализа. Например, вы можете не использовать включать папку от анализа.
Если ваш код не содержит main функция, main функция сгенерирована для анализа. По умолчанию, сгенерированный main невостребованные функции вызовов функции с входными параметрами, которые могут принять любое значение, позволенное их типом данных.
См.:
Ограничьте Входные параметры функции ограничивать входные параметры функции.
Проверьте Приложение C Без основной Функции или Проверьте Классы C++, чтобы измениться, какие функции вызваны сгенерированным main.
Если ваш код не содержит main функция, main функция сгенерирована для анализа. По умолчанию, в каждой функции вызван сгенерированным main, глобальная переменная может принять любое значение в своей области значений типа данных, прежде чем это будет сначала присвоено.
Смотрите Инициализацию Глобальных переменных для как сгенерированный main инициализирует глобальные переменные.
Если вы явным образом ограничиваете глобальную переменную к определенной области значений в постоянном режиме, анализ принимает, что переменная может принять любое значение в этой области значений в любой точке в коде.
Смотрите Внешние Ограничения для Анализа Polyspace для получения дополнительной информации о том, как переменная получает постоянную область значений. Проверяйте, присвоили ли вы постоянную область значений по ошибке, или ваша область значений должна быть более узкой, чтобы отразить реальные значения.
Если указатель присвоен абсолютный адрес, анализ принимает, что указатель разыменовывает, приводит к области значений потенциальных ценностей, определенных типом данных указателя.
Смотрите Absolute address usage для примеров абсолютного использования адреса и соответствующих предположений Программы автоматического доказательства Кода. Чтобы удалить это предположение и отметить все использование абсолютного адреса, используйте опцию -no-assumption-on-absolute-addresses.
Иногда, больше чем один оранжевый источник может быть ответственен за оранжевую проверку. Если вы включаете оранжевый источник, но не видите ожидаемого исчезновения оранжевой проверки, рассматривают, если другой источник также ответственен за проверку.