-compiler
ti)Задайте компилятор Texas Instruments
Задайте ti для Compiler (-compiler) если вы скомпилируете свой код с помощью компилятора Texas Instruments. Указав компилятор, можно избежать ошибок компиляции из синтаксиса, который не является частью Standard, но происходит из языковых расширений.
Затем укажите тип целевого процессора. Если вы выбираете ti для Compiler, в пользовательском интерфейсе Polyspace® настольные продукты, вы видите только процессоры, разрешенные для компилятора Texas Instruments. Ваш выбор целевого процессора определяет размер фундаментальных типов данных, конечность целевой машины и определенные определения ключевых слов.
Если вы задаете ti компилятор, вы должны задать путь к файлам заголовка компилятора. Смотрите раздел «Предоставление заголовков стандартных библиотек для анализа Polyspace».
Целевые системы используют следующие размеры по умолчанию в битах для основных типов. Вы не видите эти размеры в пользовательском интерфейсе десктопных продуктов Polyspace.
| Цель | char | короткий | int | долго | длинный длинный | плавание | дважды | длинный двойной | ptr | Знак по умолчанию char | 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 _ рабочий столpolyspacerootC:\Program Files\Polyspace\R2019a.
Если вы используете Polyspace в качестве расширений You Code в IDE, введите эту опцию в файл опций анализа. См. файл опций.
Параметр:
-compiler ti -target |
Значение:
c28x | c6000 | arm | msp430 |
По умолчанию:
c28x |
Пример (Bug Finder):
polyspace-bug-finder -compiler ti -target msp430 |
Пример (Code Prover):
polyspace-code-prover -compiler ti -target msp430 |
Пример (Bug Finder Server):
polyspace-bug-finder-server -compiler ti -target msp430 |
Пример (Code Prover Server):
polyspace-code-prover-server -compiler ti -target msp430 |