Компилятор Polyspace® строго следует Стандарту ANSI® C99 (ISO/IEC 9899:1999). Если ваш компилятор позволяет отклонение от Стандарта, компиляция Polyspace с помощью опций по умолчанию не может эмулировать компилятор. Например, ваш компилятор может позволить определенное ключевое слово не-ANSI, которое Polyspace не распознает по умолчанию.
Чтобы эмулировать ваш компилятор тесно, вы задаете Target & Compiler options. Если вы все еще получаете ошибки компиляции от нераспознанных ключевых слов, можно удалить или заменить их только в целях верификации. Опция Preprocessor definitions (-D)
позволяет вам делать простые замены. Для комплексных замен, например, чтобы удалить группу разделенных пробелом ключевых слов, таких как функциональный атрибут, используют опцию Command/script to apply to preprocessed files (-post-preprocessing-command)
.
Можно удалить неподдерживаемые ключевые слова из кода в целях анализа. Например, выполните эти шаги, чтобы удалить far
, и ключевое слово 0x
из вашего кода (0x
предшествует абсолютному адресу).
Сохраните следующий шаблон как C:\Polyspace\myTpl.pl
.
Для ссылки см. сводные данные регулярных выражений Perl.
На панели Configuration выберите Environment Settings.
Справа от Command/script to apply to preprocessed files щелкнуть.
Используйте диалоговое окно Open File, чтобы перейти к C:\Polyspace
.
В поле File name введите myTpl.pl
.
Нажмите 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)
.
Command/script to apply to preprocessed files (-post-preprocessing-command)
| Preprocessor definitions (-D)