Exponenta Banner

Ошибки, связанные с компилятором Green Hills

Если вы выбираете greenhills для опции Compiler (-compiler), вы столкнулись с этой проблемой.

Проблема

Во время Polyspace® анализ показывает ошибку, связанную с типами векторных данных, характерными для целевого объекта Green Hills rh850. Например, вы видите ошибку, связанную с идентификатором __ev64_u16__.

Причина

При компиляции кода с помощью компилятора Green Hills с целевой rh850, чтобы включить одну инструкцию множественных данных (SIMD) векторных инструкций, задаете два флага:

  • -rh850_simd: Вы включаете внутренние функции, которые поддерживают SIMD векторные инструкции. Функции определены в файлах заголовков компилятора. Доступны следующие типы данных:

    • __ev64_u16__

    • __ev64_s16__

    • __ev64_u32__

    • __ev64_s32__

    • __ev64_u64__

    • __ev64_s64__

    • __ev64_opaque__

    • __ev128_opaque__

  • -rh850_fpsimd: Вы включаете внутренние функции, которые поддерживают инструкции SIMD вектора с плавающей точкой. Функции определены в файлах заголовков компилятора. Доступны следующие типы данных:

    • __ev128_f32__

    • __ev256_f32__

Анализ Polyspace по умолчанию не включает поддержку SIMD. Необходимо идентифицировать флаги компилятора в Polyspace.

Решение

В анализе Polyspace используйте опцию командной строки -compiler-parameter. В пользовательском интерфейсе можно ввести опцию командной строки в Other поле под Advanced Settings на панели Configuration.

  • -rh850_simd: Для вашего анализа Polyspace, используйте

    -compiler-parameter -rh850_simd

  • -rh850_fpsimd: Для вашего анализа Polyspace, используйте

    -compiler-parameter -rh850_fpsimd

    Примечание

    • __ev128_opaque__ 16 байт выровнено в Polyspace.

    • __ev256_f32__ 32 байта выровнены в Polyspace.

Документация Polyspace Code Prover

Поддержка