При выборе 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 в разделе Дополнительные параметры на панели Конфигурация.
-rh850_simd: Для анализа Polyspace, используйте
-compiler-parameter -rh850_simd
-rh850_fpsimd: Для анализа Polyspace, используйте
-compiler-parameter -rh850_fpsimd
Примечание
__ev128_opaque__ равно 16 байтам, выровненным в Polyspace.
__ev256_f32__ 32 байта выровнены в Polyspace.