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

Поддержка