-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 | долго | долго долго | плавание | 'double' | долго удваивайтесь | ptr | Знак по умолчанию char | порядок байтов | Выравнивание |
|---|---|---|---|---|---|---|---|---|---|---|---|---|
i386 | 8 | 16 | 32 | 32 | 64 | 32 | 64 | 96 | 32 | со знаком | Мало | 32 |
sparc | 8 | 16 | 32 | 32 | 64 | 32 | 64 | 128 | 32 | со знаком | Большой | 64 |
m68kB | 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] |
hc08C | 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 Compiler (-compiler cosmic). | |||||||||||
| Цели для компилятора Diab | Смотрите Diab Compiler (-compiler diab). | |||||||||||
| Цели для компилятора Green Hills® | Смотрите Green Hills Compiler (-compiler greenhills). | |||||||||||
| Цели для IAR Встроенный компилятор Инструментальных средств | Смотрите IAR Embedded Workbench Compiler (-compiler iar-ew). | |||||||||||
| Цели для компилятора C MPLAB XC8 | Смотрите MPLAB XC8 C Compiler (-compiler microchip) | |||||||||||
| Цели для компилятора Renesas® | Смотрите Renesas Compiler (-compiler renesas). | |||||||||||
| Цели для того, чтобы ОПРЕДЕЛИТЬ ЗАДАЧУ для компилятора | Смотрите TASKING Compiler (-compiler tasking). | |||||||||||
| Цели для Техаса компилятор Instruments™ | Смотрите Texas Instruments Compiler (-compiler ti). | |||||||||||
[a] Для целей, где размер
[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 |
Пример (программа автоматического доказательства кода):
polyspace-code-prover -target m68k |
Пример (сервер Bug Finder): polyspace-bug-finder-server -target m68k |
Пример (сервер программы автоматического доказательства кода):
polyspace-code-prover-server -target m68k |
Можно заменить значения по умолчанию для некоторых целей при помощи определенных параметров командной строки. Смотрите раздел Command-Line Options в Generic target options.