-compiler ti)Укажите компилятор Texas Instruments
Определить ti для Compiler (-compiler) при компиляции кода с помощью компилятора Texas Instruments. Указывая компилятор, можно избежать ошибок компиляции из синтаксиса, который не является частью стандарта, но происходит от языковых расширений.
Затем укажите тип целевого процессора. При выборе ti для компилятора в интерфейсе пользователя настольных продуктов Polyspace ® отображаются только процессоры, разрешенные для компилятора Texas Instruments. Ваш выбор целевого процессора определяет размер фундаментальных типов данных, полноту целевой машины и определённые определения ключевых слов.
При указании ti необходимо указать путь к файлам заголовка компилятора. См. раздел Предоставление стандартных заголовков библиотек для анализа полиспейсов.
Целевые объекты используют следующие размеры по умолчанию в битах для фундаментальных типов. Эти размеры не отображаются в интерфейсе пользователя настольных продуктов Polyspace.
| Цель | случайная работа | короткий | интервал | долго | длинная | плавание | дважды | длинный двойник | ptr | Знак символа по умолчанию | Endianness | Выравнивание | Определение size_t | Определение wchar_t |
|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
c28x | 16 | 16 | 16 | 32 | 64 | 32 | 32 | 64 | 32 | подписанный | Мало | 32 | неподписанный длинный | неподписанная int |
c6000 | 8 | 16 | 32 | 32 | 64 | 32 | 64 | 64 | 32 | подписанный | Мало | 64 | неподписанная int | неподписанный короткий |
arm | 8 | 16 | 32 | 32 | 64 | 32 | 64 | 64 | 32 | неподписанный | Большой | 64 | неподписанная int | неподписанный короткий |
msp430 | 8 | 16 | 16 | 32 | 64 | 32 | 64 | 64 | 16 | неподписанный | Мало | 16 | неподписанная int | неподписанная int |
Спецификация компилятора также определяет значения многих специфичных для компилятора макросов. Если требуется узнать, как Polyspace определяет определенный макрос, используйте опцию -dump-preprocessing-info.
Чтобы переопределить определение макроса, используйте параметр Preprocessor definitions (-D).
Чтобы отменить определение макроса, используйте параметр Disabled preprocessor definitions (-U).
Polyspace не поддерживает некоторые конструкции, специфичные для компилятора Texas Instruments.
Список неподдерживаемых конструкций см. в разделе codeprover_limitations.pdf в polyspaceroot\polyspace\verifier\code_prover_desktoppolyspacerootC:\Program Files\Polyspace\R2019a.
Если в качестве расширений кода в IDE используется Polyspace, введите эту опцию в файл опций анализа. См. файл параметров.
Параметр:
-compiler ti -target |
Значение:
c28x | c6000 | arm | msp430 |
По умолчанию:
c28x |
Пример (поиск ошибок):
polyspace-bug-finder -compiler ti -target msp430 |
Пример (проверка кода):
polyspace-code-prover -compiler ti -target msp430 |
Пример (сервер поиска ошибок):
polyspace-bug-finder-server -compiler ti -target msp430 |
Пример (сервер проверки кода):
polyspace-code-prover-server -compiler ti -target msp430 |