Удаление или замена ключевых слов перед компиляцией

Polyspace® компилятор строго следует ANSI® C99 стандарт (ISO/IEC 9899:1999). Если ваш компилятор допускает отклонение от Стандарта, компиляция Polyspace с использованием опций по умолчанию не может эмулировать ваш компилятор. Например, ваш компилятор может разрешить использование определенного ключевого слова, отличного от ANSI, которое Polyspace не распознает по умолчанию.

Чтобы близко эмулировать компилятор, задайте опции Target & Compiler. Если вы по-прежнему получаете ошибки компиляции из непризнанных ключевых слов, можно удалить или заменить их только в целях верификации. Опция Preprocessor definitions (-D) позволяет делать простые замены. Для сложных замен, например, чтобы удалить группу разделенных пробелом ключевых слов, таких как атрибут функции, используйте опцию Command/script to apply to preprocessed files (-post-preprocessing-command).

Удаление непризнанных ключевых слов

Вы можете удалить неподдерживаемые ключевые слова из своего кода в целях анализа. Например, выполните следующие действия, чтобы удалить far и 0x ключевое слово из вашего кода (0x предшествует абсолютному адресу).

  1. Сохраните следующий шаблон следующим C:\Polyspace\myTpl.pl.

     Содержимое myTpl.pl

    Для ссылки смотрите сводные данные регулярных выражений Perl.

     Регулярные выражения Perl

  2. На панели Configuration выберите Environment Settings.

  3. Справа от Command/script to apply to preprocessed files нажмите.

  4. Используйте диалоговое окно «Открыть файл», чтобы перейти к C:\Polyspace.

  5. В File name поле введите myTpl.pl.

  6. Нажмите Open. Видишь C:\Polyspace\myTpl.pl в поле Command/script to apply to preprocessed files.

Удаление непризнанных атрибутов функции

Можно удалить неподдерживаемые атрибуты функции из кода в целях анализа.

Если вы запускаете верификацию на этом коде, задающую универсальный компилятор, то можете увидеть ошибки компиляции из noreturn атрибут. Код компилируется с использованием GNU® компилятор.

void fatal () __attribute__ ((noreturn));
          
void fatal (/* ... */)
{
    /* ... */ /* Print error message. */ /* ... */
    exit (1);
}

Если программа не распознает атрибут и атрибут не влияет на анализ кода, можно удалить его из кода в целях верификации. Например, вы можете использовать этот скрипт Perl, чтобы удалить noreturn атрибут.

while ($line = <STDIN>) 
{

# __attribute__ ((noreturn))

  # Remove far keyword
  $line =~ s/__attribute__\ \(\(noreturn\)\)//g;
  
  # Print the current processed line to STDOUT
  print $line;
}

Задайте скрипт используя опцию Command/script to apply to preprocessed files (-post-preprocessing-command).

См. также

Опции анализа Polyspace

Похожие темы