-compiler
ti)Задайте компилятор Texas Instruments
Задайте ti для Compiler (-compiler) если вы компилируете свой код с помощью компилятора Texas Instruments. Путем определения компилятора можно избежать ошибок компиляции от синтаксиса, который не является частью Стандарта, но прибывает из расширений языка.
Затем задайте свой тип целевого процессора. Если вы выбираете ti для Compiler, в пользовательском интерфейсе десктопных решений Polyspace®, вы видите, что только процессоры допускали компилятор Texas Instruments. Ваш выбор целевого процессора определяет размер основополагающих типов данных, порядок байтов целевой машины и определенных определений ключевого слова.
Если вы задаете ti компилятор, необходимо задать путь к заголовочным файлам компилятора. Смотрите Обеспечивают Стандартные Заголовки Библиотеки для Анализа Polyspace.
Цели используют следующие размеры по умолчанию в битах для фундаментальных типов. Вы не видите эти размеры в пользовательском интерфейсе десктопных решений Polyspace.
| Цель | 'char' | короткий | int | долго | долго долго | плавание | 'double' | долго дважды | ptr | Знак по умолчанию char | Порядок байтов | Выравнивание | Определение 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.
Параметр:
-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 |