На Orange Sources панели показаны источники без ограничений, такие как изменчивые переменные и упрямые функции, которые могут привести к нескольким оранжевым проверкам (недоказанным результатам) в анализе Code Prover. Если вы ограничиваете оранжевый источник, можно адресовать несколько оранжевых чеков вместе. Чтобы увидеть панель Orange Sources, нажмите
кнопку на панели Result Details.
Источники по существу указывают переменные, значения которых не могут быть определены из вашего кода. Переменные могут быть входными параметрами функций, контекст вызова которых неизвестен, или возвращающими значения неопределенных функций. Code Prover принимает, что эти переменные берут полную область значений значений, разрешенных их типом данных. Это широкое предположение может привести к одной или нескольким оранжевым проверкам в последующем коде.
Например, в этом примере, если функция 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 function, a main функция генерируется для анализа. По умолчанию сгенерированный main функция вызывает незакрытые функции с входами, которые могут принимать любое значение, разрешенное их типом данных.
См.:
Ограничьте Входные Параметры Функции, чтобы ограничить входные параметры функции.
Проверьте приложение C без основной функции или проверьте классы C++, чтобы изменить, какие функции вызываются сгенерированными main.
Если ваш код не содержит main function, a main функция генерируется для анализа. По умолчанию в каждой функции, вызываемой сгенерированным mainглобальная переменная может взять любое значение в своей области значений типов данных, прежде чем она будет впервые назначена.
Смотрите допущения об инициализации глобальной переменной для того, как сгенерированный main инициализирует глобальные переменные.
Если вы явным образом ограничиваете глобальную переменную определенной областью значений в постоянном режиме, анализ принимает, что переменная может взять любое значение в этой области значений в любой точке кода.
Дополнительные сведения о том, как переменная получает постоянную область значений, см. в разделе «Внешние ограничения для анализа Polyspace». Проверьте, присвоена ли вам постоянная область значений по ошибке или ваша область значений должен быть более узким, чтобы отражать значения реального мира.
Если указателю назначен абсолютный адрес, анализ принимает, что разыменование указателя приводит к области значений потенциальных значений, определяемых типом данных указателя.
См. Absolute address usage для примеров использования абсолютного адреса и соответствующих допущений Code Prover. Чтобы удалить это предположение и пометить все виды использования абсолютного адреса, используйте опцию -no-assumption-on-absolute-addresses.
Иногда за оранжевый чек может отвечать более одного оранжевого источника. Если вы подключаете оранжевый источник, но не видите ожидаемого исчезновения оранжевого чека, рассмотрите, является ли другой источник также ответственным за чек.