Возможная ошибка во время выполнения с while loop-Polyspace

Question

Я работаю с языком 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

Мы ценим любые предложения.

Answer 1

Код в целом довольно подозрительный.

ошибки

• 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];
  }
  

Answer 2

Причина, по которой 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;

Если вы сделаете это изменение в коде, красная ошибка исчезнет.

Answer 3

Если 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 не считал все возможные значения действительными в своем анализе. Это, вероятно, также приведет к ускорению анализа.