Exponenta Banner

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

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

Проблема

Анализ Polyspace® останавливается с ошибкой компиляции.

Причина

Вы используете определенные усовершенствованные специфичные для компилятора расширения, которые не поддерживает Polyspace. Смотрите Ограничения.

Решение

Для более легкой мобильности вашего кода избегайте использования расширений.

Если вы хотите использовать расширения и все еще анализировать ваш код, перенести неподдерживаемые расширения в директиву препроцессору. Например:

#ifdef POLYSPACE
    // Supported syntax
#else
    // Unsupported syntax
#endif
Для регулярной компиляции не задавайте макро-POLYSPACE. Для анализа Polyspace введите POLYSPACE для опции Preprocessor definitions (-D).

Если ошибка компиляции связана с кодом ассемблера, используйте опцию -asm-begin -asm-end.

Документация Polyspace Code Prover Server
Поддержка