Exponenta Banner

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

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

Проблема

Анализ останавливает с сообщением об ошибке, связанным с non-ANSI® C ключевое слово, например, data или приписывает, такие как __attribute__((weak)).

В зависимости от местоположения ключевого слова может варьироваться сообщение об ошибке. Например, эта линия вызывает сообщение об ошибке: expected a ";".

data int tab[10];

Причина

Типовой компилятор Polyspace® поддерживает только ANSI C ключевые слова. Если вы используете расширение языка, типовой компилятор не распознает его и обрабатывает ключевое слово как регулярный идентификатор.

Решение

Задайте свой компилятор при помощи опции Compiler (-compiler).

Если ваш компилятор непосредственно не поддерживается или не основан на поддерживаемом компиляторе, можно использовать типовой компилятор. Работать вокруг ошибок компиляции:

  • Если ключевое слово связано с моделированием памяти, удалите его из предварительно обработанного кода. Например, чтобы удалить data ключевое слово, введите data= для опции Preprocessor definitions (-D).

  • Если ключевое слово связано с атрибутом, удалите атрибуты из предварительно обработанного кода. Введите __attribute__(x)= для опции Preprocessor definitions (-D).

    Если ваш код имеет эту линию:

    void __attribute__ ((weak)) func(void);
    И вы удаляете атрибуты, анализ читает строку как:
    void func(void);

Когда вы используете эти обходные решения, ваш исходный код не изменен.

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

Поддержка