Generic target options

Задайте размер типов данных и эндианнес путем создания собственного целевого процессора

Описание

Если целевой процессор не поддерживается непосредственно Polyspace^®, можно создать свою собственную цель. Вы задаете целевую mcpu представление типового «Micro Controller/Processor Unit», а затем явное определение размеров основных типов данных, эндианнеса и других характеристик.

Настройки

В пользовательском интерфейсе десктопных продуктов Polyspace, диалоговое окно Generic target options открывается, когда вы устанавливаете Target processor type на mcpu. Опция Target processor type доступна в узле Target & Compiler на панели Configuration.

Используйте диалоговое окно, чтобы задать имя нового mcpu целевой объект, например My_target. Этот новый целевой объект добавляется в список опций Target processor type.

Характеристики по умолчанию нового целевого объекта: перечислены как [size] типа

char [8]
короткие [16]
int [16]
длинные [32]
длинные [32]
с плавающей точкой [32]
double [32]
длинный двойной [32]
указатель [16]
выравнивание [32]
char подписан
эндианнесса маленькая-эндовая

Зависимость

Пользовательский целевой объект может быть создан только при Target processor type (-target) установлено в mcpu.

Пользовательский целевой объект недоступен при Compiler (-compiler) задается значение одного из визуальных * опции.

Опции командной строки

При использовании командной строки используйте -target mcpu наряду с этими опциями целевой спецификации.

Опция	Описание	Доступно с	Пример
`-little-endian`	Little-endian architures is Less Signative byte First (LSF). Для примера: i386. Указывает, что менее значительный байт короткого целого числа (например, 0x00FF) сохранен в первом байте (0xFF) и наиболее значительном байте (0x00) во втором байте.	`mcpu`	`polyspace-code-prover -lang c -target mcpu -little-endian`
`-big-endian`	Большие-эндовые архитектуры являются наиболее значимым байтом First (MSF). Для примера: SPARC, м68к. Указывает, что самый значительный байт короткого целого числа (например, 0x00FF) сохранен в первом байте (0x00) и менее значительный байт (0xFF) во втором байте.	`mcpu`	`polyspace-code-prover -target mcpu -big-endian`
`-default-sign-of-char [signed \| unsigned]`	Задайте знак по умолчанию `char`. `signed`: Задает, что `char` является подписанным, переопределяющим значение по умолчанию целевого объекта. `unsigned`: Задает, что `char` беззнаковое, переопределяющее значение по умолчанию целевого объекта.	Все цели	`polyspace-code-prover -default-sign-of-char unsigned -target mcpu`
`-char-is-16bits`	`char` задается как 16 биты, и все объекты имеют минимальное выравнивание 16 бит Несовместимо с `-short-is-8bits` и `-align 8`	`mcpu`	`polyspace-code-prover -target mcpu -char-is-16bits`
`-short-is-8bits`	Определите `short` как 8 бит, независимо от знака	`mcpu`	`polyspace-code-prover -target mcpu -short-is-8bits`
`-int-is-32bits`	Определите `int` как 32 бита, независимо от знака. Выравнивание также устанавливается на 32 бита.	`mcpu`, `hc08`, `hc12`, `mpc5xx`	`polyspace-code-prover -target mcpu -int-is-32bits`
`-long-is-32bits`	Определите `long` как 32 бита, независимо от знака. Выравнивание также устанавливается на 32 бита. Если ваш проект задает `int` до 64 бит, вы не можете использовать эту опцию.	Все цели	`polyspace-code-prover -target mcpu -long-is-32bits`
`-long-long-is-64bits`	Определите `long long` 64 бита, независимо от знака. Выравнивание также устанавливается на 64 бита.	`mcpu`	`polyspace-code-prover -target mcpu -long-long-is-64bits`
`-double-is-64bits`	Определите `double` и `long double` 64 бита, независимо от знака.	`mcpu`, `sharc21x61`, `hc08`, `hc12`, `mpc5xx`	`polyspace-code-prover -target mcpu -double-is-64bits`
`-pointer-is-24bits`	Определите указатель как 24 бита, независимо от знака.	`c18`	`polyspace-code-prover -target c18-pointer-is-24bits`
`-pointer-is-32bits`	Определите указатель как 32 бита, независимо от знака.	`mcpu`	`polyspace-code-prover -target mcpu -pointer-is-32bits`
`-align [32\|16\|8]`	Задает наибольшее выравнивание объектов struct или массива по 32, 16 или 8-разрядным контурам. Следовательно, массив или структурное хранилище строго определяется размером отдельных объектов данных без представителя и конца.	`mcpu`, `hc08`, `hc12`, `mpc5xx`. Кроме `mcpu`, все цели поддерживают только 16 или 32 бита.	`polyspace-code-prover -target mcpu -align 16`

См. также:

Можно также использовать опцию -custom-target для определения размеров в байтах основных типов данных, сигнальности простых char, выравнивание структур и базовых типов стандартных typedef-s, например size_t, wchar_t и ptrdiff_t.

Примеры

Наборы инструментальных средств GCC

Если вы используете любую из этих цепочек инструментов GCC для разработки ПО, можно настроить анализ Polyspace так, чтобы ваш код компилировался с Polyspace:

ARM Ltd's GNU Arm Embedded Toolchain
EDV-система HighTec
Linaro^® Набор перекрестных инструментальных средств GNU
НАСТАВНИК^® Встроенный Sourcery™ CodeBench
QNX^® Платформа разработки программного обеспечения
CrossWorks от Rowley Associates
STMicroelectronics^® TrueSTUDIO^® для STM32
Составитель кода Instruments™ Техаса Studio™
Wind River^® Компилятор GNU

Использование polyspace-configure чтобы проследить систему сборки и извлечь информацию о строении компилятора. Команда создает проект Polyspace. Чтобы сгенерировать файл опций, который вы затем передаете в Polyspace в командной строке, запустите polyspace-configure с -output-options-file.

Кроме того, если вы предпочитаете устанавливать детали своего компилятора строения вручную:

Выберите gnu#.x компилятор, который соответствует версии компилятора для Compiler (-compiler).
Задайте цель при помощи опций командной строки. Пример целей, которые можно задать, см. в разделе Цели для компиляторов на основе GCC.
Задайте определения макросов компилятора с помощью Preprocessor definitions (-D).

Цели для компиляторов на основе GCC

Если вы выбираете один из gnu#.x компиляторы для Compiler (-compiler)можно задать один из поддерживаемых типов целевых процессоров. См. Target processor type (-target). Если тип целевого процессора не указан непосредственно как поддерживаемый, можно создать целевой процессор с помощью этой опции.

Например, можно создать следующие цели:

Tricore: Используйте следующие опции:

-target mcpu
-int-is-32bits 
-long-long-is-64bits 
-double-is-64bits 
-pointer-is-32bits 
-enum-type-definition auto-signed-first 
-wchar-t-type-is signed-int

PowerPC: Используйте следующие опции:

-target mcpu 
-int-is-32bits 
-long-long-is-64bits 
-double-is-64bits 
-pointer-is-32bits 
-wchar-t-type-is signed-int

ARM: Используйте следующие опции:

-target mcpu
-int-is-32bits
-long-long-is-64bits
-double-is-64bits
-pointer-is-32bits
-enum-type-definition auto-signed-first
-wchar-t-type-is unsigned-int

MSP430: Используйте следующие опции:

-target mcpu
-long-long-is-64bits
-double-is-64bits
-wchar-t-type-is signed-long
-align 16

Эмуляция микрочипов MPLAB XC16 и XC32 компиляторов

Если вы создаете свой исходный код с помощью Microchip MPLAB XC16 или XC32 компиляторов, можно настроить анализ Polyspace так, чтобы ваш код компилировался с Polyspace. Введите эти опции в командной строке или укажите их в панели Configuration интерфейса рабочего стола Polyspace.

Компилятор	Целевые процессоры	Опции
Файлы MPLAB XC16	PIC24 dsPIC	-compiler gnu4.6 -to compile -D__XC__ -D__XC16__ -target=mcpu -wchar-t-type-is unsigned-int -align 16 -long-long-is-64bits
Файлы MPLAB XC32	PIC32	-compiler gnu4.8 -custom-target true,8,2,4,-1,4,8,4,4,8,4,8,1,big,unsigned_long,long,int -D__PIC32M -D__PIC32MX -D__PIC32MX__ -D__XC32 -D__XC32__ -D__XC -D__XC__ -D__mips=32 -D__mips__ -D_mips

Компилятор

Целевые процессоры

Опции

Файлы MPLAB XC16

PIC24

dsPIC

-compiler gnu4.6 
-to compile 
-D__XC__ 
-D__XC16__ 
-target=mcpu 
-wchar-t-type-is unsigned-int 
-align 16 
-long-long-is-64bits

Файлы MPLAB XC32

PIC32

-compiler gnu4.8 
-custom-target true,8,2,4,-1,4,8,4,4,8,4,8,1,big,unsigned_long,long,int 
-D__PIC32M 
-D__PIC32MX 
-D__PIC32MX__ 
-D__XC32 
-D__XC32__ 
-D__XC 
-D__XC__ 
-D__mips=32 
-D__mips__ 
-D_mips

Набор макросов, заданный с опцией Preprocessor definitions (-D) - минимальный набор. Укажите дополнительные макросы по мере необходимости, чтобы код компилировался с Polyspace.

Совет

Если вы используете Polyspace в качестве расширений You Code в IDE, введите эту опцию в файл опций анализа. См. файл опций.

См. также

Target processor type (-target)

Документация