-target)Укажите размер типов данных и диапазон, выбрав предопределенный целевой процессор
Укажите процессор для развертывания кода.
Целевой процессор определяет размеры основных типов данных и полноту целевой машины. Код, предназначенный для незарегистрированного типа процессора, можно проанализировать с помощью одного из других типов процессоров, если они имеют общие свойства данных.
Пользовательский интерфейс (только для настольных ПК): в конфигурации проекта этот параметр находится в узле Target & Compiler. Чтобы просмотреть размеры типов, нажмите кнопку Edit справа от выпадающего списка Target processor type.
Для некоторых компиляторов в интерфейсе пользователя отображаются только процессоры, разрешенные для этого компилятора. Для этих компиляторов размеры типов данных в интерфейсе пользователя также не отображаются. Размеры типов данных см. в ссылках в таблице ниже.
файл командной строки и параметров: Использовать параметр -target. См. раздел Сведения о командной строке.
Вы указываете целевой процессор, чтобы некоторые проверки времени выполнения Polyspace ® были адаптированы к размерам типов данных и другим свойствам этого процессора.
Например, переменная может перетекать для меньших значений на 32-разрядном процессоре, таком как i386, по сравнению с 64-разрядным процессором, таким как x86_64. Если выбрать x86_64 для анализа Polyspace, но развернуть код на процессоре i386, результаты Polyspace не всегда применимы.
После выбора целевого процессора можно указать, является ли символ по умолчанию подписанным или неподписанным. Чтобы определить, какую сигнатуру указать, скомпилируйте этот код с помощью параметров компилятора, которые вы обычно используете:
#include <limits.h> int array[(char)UCHAR_MAX]; /* If char is signed, the array size is -1
-fsigned-char флаг и не может быть скомпилирован с -funsigned-char флаг.По умолчанию: i386
В этой таблице показан размер каждого типа фундаментальных данных, рассматриваемых Polyspace. Для некоторых целей можно изменить размер по умолчанию, нажав кнопку Изменить справа от выпадающего списка Тип целевого процессора. Необязательные значения для этих целей показаны в [скобках] в таблице.
| Цель | случайная работа | короткий | интервал | долго | длинная | плавание | дважды | длинный двойной [a] | ptr | Знак символа по умолчанию | индиец | Выравнивание |
|---|---|---|---|---|---|---|---|---|---|---|---|---|
i386 | 8 | 16 | 32 | 32 | 64 | 32 | 64 | 96 | 32 | подписанный | Мало | 32 |
sparc | 8 | 16 | 32 | 32 | 64 | 32 | 64 | 128 | 32 | подписанный | Большой | 64 |
m68k[b] | 8 | 16 | 32 | 32 | 64 | 32 | 64 | 96 | 32 | подписанный | Большой | 64 |
powerpc | 8 | 16 | 32 | 32 | 64 | 32 | 64 | 128 | 32 | неподписанный | Большой | 64 |
c-167 | 8 | 16 | 16 | 32 | 32 | 32 | 64 | 64 | 16 | подписанный | Мало | 64 |
tms320c3x | 32 | 32 | 32 | 32 | 64 | 32 | 32 | 64 | 32 | подписанный | Мало | 32 |
sharc21x61 | 32 | 32 | 32 | 32 | 64 | 32 | 32 [64] | 32 [64] | 32 | подписанный | Мало | 32 |
necv850 | 8 | 16 | 32 | 32 | 32 | 32 | 32 | 64 | 32 | подписанный | Мало | 32 [16, 8] |
hc08[c] | 8 | 16 | 16 [32] | 32 | 32 | 32 | 32 [64] | 32 [64] | 16 [d] | неподписанный | Большой | 32 [16] |
hc12 | 8 | 16 | 16 [32] | 32 | 32 | 32 | 32 [64] | 32 [64] | 326 | подписанный | Большой | 32 [16] |
mpc5xx | 8 | 16 | 32 | 32 | 64 | 32 | 32 [64] | 32 [64] | 32 | подписанный | Большой | 32 [16] |
c18 | 8 | 16 | 16 | 32 [24] [e] | 32 | 32 | 32 | 32 | 16 [24] | подписанный | Мало | 8 |
x86_64 | 8 | 16 | 32 | 64 [32] [f] | 64 | 32 | 64 | 128 | 64 | подписанный | Мало | 64 [32] |
mcpu... (Advanced)[г] | 8 [16] | 8 [16] | 16 [32] | 32 | 32 [64] | 32 | 32 [64] | 32 [64] | 16 [32] | подписанный | Мало | 32 [16, 8] |
| Цели для компилятора ARM ® v5 | Посмотрите ARM v5 Compiler (-compiler armcc). | |||||||||||
| Цели для компилятора ARM v6 | Посмотрите ARM v6 Compiler (-compiler armclang). | |||||||||||
| Цели для компилятора NPX CodeWarrior ® | Посмотрите NXP CodeWarrior Compiler (-compiler codewarrior). | |||||||||||
| Цели для компилятора Cosmic | Посмотрите Cosmic Compiler (-compiler cosmic). | |||||||||||
| Цели для компилятора Diab | Посмотрите Diab Compiler (-compiler diab). | |||||||||||
| Цели компилятора Green Hills ® | Посмотрите Green Hills Compiler (-compiler greenhills). | |||||||||||
| Цели компилятора IAR Embedded Workbench | Посмотрите IAR Embedded Workbench Compiler (-compiler iar-ew). | |||||||||||
| Цели для компилятора MPLAB XC8 C | Посмотрите MPLAB XC8 C Compiler (-compiler microchip) | |||||||||||
| Цели для компилятора Renesas ® | Посмотрите Renesas Compiler (-compiler renesas). | |||||||||||
| Цели для компилятора TASKING | Посмотрите TASKING Compiler (-compiler tasking). | |||||||||||
| Цель для компилятора Texas Instruments™ | Посмотрите Texas Instruments Compiler (-compiler ti). | |||||||||||
[а] Для целей, размер которых составляет
[b] Семейство M68k (68000, 68020 и т.д.) включает процессор ColdFire [c] Указанные ключевые слова, не относящиеся к ANSI C, и зависящие от реализации компилятора прагматики и средства прерывания не учитываются данной поддержкой [d] Все типы указателей (ближний или дальний указатель) физически имеют 2 байта (hc08) или 4 байта (hc12) ширины. [e] [f] Использовать опцию [г]
| ||||||||||||
Если процессор отсутствует в списке, используйте аналогичный процессор, который имеет те же характеристики, или создайте mcpu универсальный целевой процессор. Посмотрите Generic target options.
Можно также создать пользовательскую цель, явно указав размеры фундаментальных типов и т. д. с помощью опции -custom-target.
Параметр: -target |
Значение:
i386 | sparc | m68k | powerpc | c-167 | tms320c3x | sharc21x61 | necv850 | hc08 | hc12 | mpc5xx | c18 | x86_64 | mcpu |
По умолчанию: i386 |
Пример (поиск ошибок): polyspace-bug-finder -target m68k |
Пример (проверка кода):
polyspace-code-prover -target m68k |
Пример (сервер поиска ошибок): polyspace-bug-finder-server -target m68k |
Пример (сервер проверки кода):
polyspace-code-prover-server -target m68k |
Можно переопределить значения по умолчанию для некоторых целевых объектов с помощью определенных параметров командной строки. См. раздел Параметры командной строки в разделе Generic target options.