-target)Задайте размер типов данных и конечность путем выбора предопределенного целевого процессора
Укажите процессор, на котором вы развертываете свой код.
Целевой процессор определяет размеры основных типов данных и конечность целевой машины. Можно анализировать код, предназначенный для несвязанного типа процессора, используя один из других типов процессора, если они имеют общие свойства данных.
Пользовательский интерфейс (только для настольных продуктов): В строении проекта опция находится на узле Target & Compiler. Чтобы увидеть размеры типов, нажмите кнопку Edit справа от раскрывающегося списка Target processor type.
Для некоторых компиляторов в пользовательском интерфейсе отображаются только процессоры, разрешенные для этого компилятора. Для этих компиляторов вы также не можете увидеть размеры типов данных в пользовательском интерфейсе. Размеры типов данных см. в приведенной ниже таблице ссылок.
Командная строка и файл опций: Используйте опцию -target. См. «Информация о командной строке».
Вы задаете целевой процессор, чтобы часть Polyspace® проверки во время выполнения адаптируются к размерам типов данных и другим свойствам этого процессора.
Например, переменная может переполняться для меньших значений на 32-разрядном процессоре, таком как i386, по сравнению с 64-разрядным процессором, таким как x86_64. Если вы выбираете x86_64 для анализа Polyspace, но развертываете код на процессоре i386, результаты Polyspace не всегда применяются.
После выбора целевого процессора можно указать, подписан ли знак char по умолчанию или не подписан. Чтобы определить, какую сигнальность задать, скомпилируйте этот код с помощью настроек компилятора, которые вы обычно используете:
#include <limits.h> int array[(char)UCHAR_MAX]; /* If char is signed, the array size is -1
-fsigned-char флаг и не удается скомпилироваться со -funsigned-char флаг.По умолчанию: i386
Эта таблица показывает размер каждого основного типа данных, который рассматривает Polyspace. Для некоторых целей можно изменить размер по умолчанию, нажав кнопку Edit справа от выпадающего списка Target processor type. Необязательные значения для этих целевых объектов показаны в [скобках] в таблице.
| Цель | char | короткий | int | долго | длинный длинный | плавание | дважды | длинный двойной[a] | ptr | Знак по умолчанию char | индиец | Выравнивание |
|---|---|---|---|---|---|---|---|---|---|---|---|---|
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)[g] | 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 Compiler (-compiler diab). | |||||||||||
| Цели для зеленых холмов® компилятор | См. 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). | |||||||||||
| Цели для компилятора Instruments™ Texas | См. Texas Instruments Compiler (-compiler ti). | |||||||||||
[a] Для целей, где размер
[b] Семейство M68k (68000, 68020 и так далее) включает процессор «ColdFire» [c] Не-ANSI C заданные ключевые слова и зависимые от реализации компилятора прагмы и средства прерывания не учитываются этой поддержкой [d] Все виды указателей (ближний или дальний указатель) имеют 2 байта (hc08) или 4 байта (hc12) ширины физически. [e] The [f] Используйте опцию [g]
| ||||||||||||
Если ваш процессор не указан в списке, используйте аналогичный процессор, который имеет те же характеристики, или создайте mcpu типовой целевой процессор. См. Generic target options.
Можно также создать пользовательский целевой объект, явно указав размеры основных типов и так далее с помощью опции -custom-target.
Параметр: -target |
Значение:
i386 | sparc | m68k | powerpc | c-167 | tms320c3x | sharc21x61 | necv850 | hc08 | hc12 | mpc5xx | c18 | x86_64 | mcpu |
По умолчанию: i386 |
Пример (Bug Finder): polyspace-bug-finder -target m68k |
Пример (Code Prover):
polyspace-code-prover -target m68k |
Пример (Bug Finder Server): polyspace-bug-finder-server -target m68k |
Пример (Code Prover Server):
polyspace-code-prover-server -target m68k |
Можно переопределить значения по умолчанию для некоторых целей с помощью определенных опций командной строки. Смотрите раздел Command-Line Опций в Generic target options.