Компилятор 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)