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

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

Проблема

Во время анализа Polyspace ® появляется ошибка, связанная с ключевым словом, определенным для компилятора Diab. Например, вы видите ошибку, связанную с restrict ключевое слово.

Причина

Обычно для включения ключевого слова используется флаг компилятора. Анализ Polyspace не включает эти ключевые слова по умолчанию. Необходимо информировать Polyspace о флагах компилятора.

Анализ Polyspace не включает эти ключевые слова по умолчанию, чтобы предотвратить ошибки компиляции. Другой пользователь может не включить ключевое слово и вместо этого использовать имя ключевого слова в качестве обычного идентификатора. Если Polyspace рассматривает идентификатор как ключевое слово, произойдет ошибка компиляции.

Решение

Использовать параметр командной строки -compiler-parameter в анализе Polyspace следующим образом. Этот параметр командной строки используется для информирования Polyspace о флагах компилятора. В интерфейсе пользователя настольных продуктов Polyspace можно ввести параметр командной строки в поле Other. Можно ввести опцию несколько раз.

Аргумент -compiler-parameter зависит от ключевого слова, вызывающего ошибку. После включения ключевого слова не используйте имя ключевого слова в качестве обычного идентификатора. Например, после включения ключевого слова pixel, не использовать pixel как имя переменной. Заявление int pixel = 1 вызывает ошибку компиляции.

restrict ключевое слово:
Обычно используется флаг компилятора -Xlibc-new или -Xc-new. Для анализа Polyspace используйте
```
-compiler-parameter -Xc-new
```
Следующий код не будет скомпилирован с помощью Polyspace, если не указан флаг компилятора.
```
int sscanf(const char *restrict, const char *restrict, ...);
```
Векторные расширения PowerPC AltiVec, такие как vector квалификатор типа:
Обычно используется флаг компилятора -tPPCALLAV:. Для анализа Polyspace используйте
```
-compiler-parameter -tPPCALLAV:
```
Следующий код не будет скомпилирован с помощью Polyspace, если не указан флаг компилятора.
```
vector unsigned char vbyte;
vector bool vbool;
vector pixel vpx;

int main(int argc, char** argv)
{
  return 0;
}
```
Расширенные ключевые слова, такие как pascal, inline, packed, interrupt, extended, __X, __Y, vector, pixel, bool и другие:
Обычно используется флаг компилятора -Xkeywords=. Для анализа Polyspace используйте
```
-compiler-parameter -Xkeywords=0xFFFFFFFF
```
Следующий код не будет скомпилирован с помощью Polyspace, если не указан флаг компилятора.
```
packed(4) struct s2_t {
    char b;
    int i;
} s2;

packed(4,2) struct s3_t {
    char b;
} s3;

int pascal foo = 4;

int main(int argc, char** argv) {
    foo++;
    return 0;
}
```

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