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

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

Чтобы эмулировать ваш компилятор тесно, вы задаете Целевые и Параметры компилятора. Если вы все еще получаете ошибки компиляции от нераспознанных ключевых слов, можно удалить или заменить их только в целях верификации. Опция 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. Используйте диалоговое окно Open File, чтобы перейти к 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

Похожие темы