Возможная ошибка во время выполнения с while loop-Polyspace
Я работаю с языком Embedded C и недавно запустил MathWorks Polyspace Code Prover (динамический анализ) для всего проекта, чтобы проверить наличие критических ошибок во время выполнения. Он обнаружил одну ошибку (красное предупреждение) в цикле "В то время как я копирую некоторые данные ПЗУ в ОЗУ через регистры памяти". Код работает нормально и, как и ожидалось, но я хотел бы спросить, есть ли какое-либо решение для безопасного удаления этого предупреждения. Пожалуйста, найдите пример кода ниже:
register int32 const *source;
uint32 i=0;
uint32 *dest;
source= (int32*)&ADDR_SWR4_BEGIN;
dest = (uint32*)&ADDR_ARAM_BEGIN;
if ( source != NULL )
{
while ( i < 2048 )
{
dest[i] = (uint32)source[i];
i++;
}
}
Я предполагаю, что ADDR_SWR4_BEGIN и ADDR_ARAM_BEGIN определены в сценарии компоновщика, а polyspace не скомпилировал и не связал проект, поэтому он жалуется на возможную ошибку во время выполнения или бесконечный цикл.
ADDR_SWR4_BEGIN и ADDR_ARAM_BEGIN определены как extern в соответствующем заголовочном файле.
extern uint32_t ADDR_SWR4_BEGIN;
extern uint32_t ADDR_ARAM_BEGIN;
Предупреждение красное и точное предупреждение следующее:
Check: Non-terminating Loop Detail: The Loop is infinite or contains a run-time error Severity: Unset
Мы ценим любые предложения.
3 ответа
Код в целом довольно подозрительный.
ошибки
if ( source != NULL )
, Вы просто устанавливаете этот указатель, чтобы он указывал на адрес, поэтому он, очевидно, не будет указывать на NULL. Эта строка лишняя.- Вы не используете
volatile
при обращении к регистрам / памяти, поэтому, если этот код выполняется многократно, компилятор может делать всевозможные странные предположения. Это может быть причиной диагностического сообщения.
Плохой стиль / кодовый запах (должен быть исправлен)
- С использованием
register
Ключевое слово подозрительно. Это было когда-то в 1980-х годах, когда компиляторы были ужасны и не могли должным образом оптимизировать код. В настоящее время они могут сделать это, и гораздо лучше, чем программист, поэтому любое присутствиеregister
в новом исходном коде подозрительно. - Доступ к регистру или ячейке памяти как
int32
а затем приведение этого к типу без знака не имеет никакого смысла вообще. Если данные не подписаны, то почему вы в первую очередь используете тип со знаком. - Использование домашнего приготовления
uint32
типы вместоstdint.h
это плохой стиль.
Nit-picks (незначительные замечания)
(int32*)
актерский состав должен бытьconst
Квалифицированный.Цикл излишне безобразен, его можно заменить на цикл for:
for(uint32_t i=0; i<2048; i++) { dest[i] = source[i]; }
Причина, по которой Polyspace выдает красную ошибку, заключается в том, что source
а также dest
являются указателями на uint32. Действительно, когда ты пишешь:
source= (int32*)&ADDR_SWR4_BEGIN
вы берете адрес переменной ADDR_SWR4_BEGIN
и назначить его source
,
Следовательно, оба указателя указывают на буфер только 4 байта. Тогда невозможно использовать эти указатели как массивы из 2048 элементов. Вы также должны увидеть оранжевый флажок source[i]
давая вам информацию о том, что происходит с указателем source
,
Кажется, что ADDR_SWR4_BEGIN
а также ADDR_SWR4_BEGIN
на самом деле содержат адреса. И в этом случае код должен быть:
source = (uint32*)ADDR_SWR4_BEGIN;
dest = (uint32*)ADDR_ARAM_BEGIN;
Если вы сделаете это изменение в коде, красная ошибка исчезнет.
Если PolySpace не знает значение ADDR_ARAM_BEGIN
он будет предполагать, что это может быть NULL (или любое другое значение значения для его типа). Пока вы явно тестируете source
NULL, вы не делаете то же самое для dest
,
Поскольку оба source
а также dest
назначаются из констант линкера, и в нормальных обстоятельствах ни один из них не должен быть NULL, нет необходимости явно проверять NULL в потоке управления и assert()
было бы предпочтительнее - PolySPace распознает утверждения и применит ограничение в последующем анализе, но assert()
разрешается ни к чему, когда NDEBUG
определяется (обычно в сборках релиза), поэтому не накладывает ненужных накладных расходов:
const uint32_t* source = (const uint32_t*)&ADDR_SWR4_BEGIN ;
uint32_t* dest = (uint32_t*)&ADDR_ARAM_BEGIN;
// PolySpace constraints asserted
assert( source != NULL ) ;
assert( dest != NULL ) ;
for( int i = 0; i < 2048; i++ )
{
dest[i] = source[i] ;
}
Альтернативой является предоставление PolySpace "принудительного включения" (-include
опция) предоставить явные определения, чтобы PolySpace не считал все возможные значения действительными в своем анализе. Это, вероятно, также приведет к ускорению анализа.