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
предшествует абсолютному адресу).
Сохраните следующий шаблон следующим C:\Polyspace\myTpl.pl
.
Для ссылки смотрите сводные данные регулярных выражений Perl.
На панели Configuration выберите Environment Settings.
Справа от Command/script to apply to preprocessed files нажмите.
Используйте диалоговое окно «Открыть файл», чтобы перейти к 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)