Укажите размер типов данных и диапазон, создав собственный целевой процессор
Если целевой процессор напрямую не поддерживается Polyspace ®, можно создать собственный целевой процессор. Вы указываете цельmcpu представление общего «микроконтроллера/процессорного блока», а затем явное указание размеров фундаментальных типов данных, эндианнессы и других характеристик.
В интерфейсе пользователя настольных продуктов Polyspace открывается диалоговое окно Общие параметры целевого процессора (Generic target options), если для параметра Тип целевого процессора (Target processor type) задано значение mcpu. Параметр Тип целевого процессора доступен в узле Target & Compiler на панели Конфигурация.
Используйте диалоговое окно для указания имени нового mcpu цель, например My_target. Этот новый целевой объект добавляется в список опций Тип целевого процессора.
Характеристики по умолчанию для нового целевого объекта: перечислены как тип
[size]
случайная работа
[8]
короткий
[16]
интервал
[16]
долго
[32]
длинная
[32]
плавание
[32]
дважды
[32]
длинный двойник
[32]
указатель
[16]
выравнивание
[32]
символ подписан
endianness является little-endian
Пользовательский целевой объект может быть создан только в том случае, если Target processor type (-target) имеет значение mcpu.
Пользовательский конечный объект недоступен, когда Compiler (-compiler) имеет значение одного из visual варианты.*
При использовании командной строки используйте -target mcpu вместе с этими параметрами целевой спецификации.
| Выбор | Описание | Доступно с | Пример |
|---|---|---|---|
-little-endian | Архитектурами Little-endian являются Byte First (LSF). Например: i386. Указывает, что менее значимый байт короткого целого числа (например, 0x00FF) хранится в первом байте (0xFF), а наиболее значимый байт (0x00) - во втором байте. | mcpu | polyspace-code-prover -lang c -target mcpu -little-endian |
-big-endian | Архитектуры Big-endian - это наиболее значимые байты (MSF). Например: SPARC, m68k. Указывает, что наиболее значимый байт короткого целого числа (например, 0x00FF) хранится в первом байте (0x00), а менее значимый байт (0xFF) - во втором байте. | mcpu | polyspace-code-prover -target mcpu -big-endian |
-default-sign-of-char [signed | unsigned] | Укажите знак по умолчанию для
| Все цели | polyspace-code-prover -default-sign-of-char unsigned -target mcpu |
-char-is-16bits |
Несовместим с | 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 | Определить Если набор проектов | Все цели | 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] | Задает наибольшее выравнивание объектов структуры или массива по 32, 16 или 8 битовым границам. Следовательно, массив или хранилище структуры строго определяется размером отдельных объектов данных без заполнения элемента и конца. |
Кроме | polyspace-code-prover -target mcpu -align 16 |
См. также:
Также можно использовать опцию -custom-target для указания размеров в байтах основных типов данных, сигнатура простой char, согласование конструкций и нижележащих типов стандарта typedef-s, такие как size_t, wchar_t и ptrdiff_t.
При использовании любой из этих цепочек инструментов GCC для разработки программного обеспечения можно настроить анализ Polyspace так, чтобы код компилировался с Polyspace:
Встроенный инструментарий GNU Arm компании ARM Ltd
HighTec EDV-Systeme
Перекрестная цепочка инструментов Linaro ® GNU
MENTOR ® Embedded Sourcery™ CodeBench
Платформа для разработки программного обеспечения QNX ®
Кроссворки Rowley Associates
STMicroelectronics ® StartSTUDIO ® для STM32
Техасский Instruments™ композитор кода Studio™
Компилятор Wind River ® GNU
Использовать polyspace-configure для отслеживания системы сборки и извлечения информации о конфигурации компилятора. Команда создает проект Polyspace. Чтобы создать файл параметров, который затем будет передан в Polyspace в командной строке, выполните команду polyspace-configure с -output-options-file.
Кроме того, если вы предпочитаете задать сведения о конфигурации компилятора вручную:
Выберите gnu#.x компилятор, соответствующий вашей версии компилятора для Compiler (-compiler).
Укажите целевой объект с помощью параметров командной строки. Пример целевых объектов, которые можно указать, см. в разделе Целевые объекты для компиляторов на основе GCC.
Укажите определения макросов компилятора с помощью Preprocessor definitions (-D).
При выборе одного из gnu#.x компиляторы для Compiler (-compiler), можно указать один из поддерживаемых типов целевого процессора. Посмотрите Target processor type (-target). Если целевой тип процессора не указан непосредственно как поддерживаемый, можно создать целевой тип с помощью этой опции.
Например, можно создать следующие цели:
Трикор: Используйте следующие опции:
-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
Если исходный код создается с помощью компиляторов Microchip MPLAB XC16 или XC32, можно настроить анализ Polyspace так, чтобы код компилировался с Polyspace. Введите эти параметры в командной строке или укажите их на панели «Конфигурация» интерфейса пользователя рабочего стола Polyspace.
| Компилятор | Целевые семейства процессоров | Варианты |
|---|---|---|
| XC16 MPLAB | 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 |
| XC32 MPLAB | 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.
Если в качестве расширений кода в IDE используется Polyspace, введите эту опцию в файл опций анализа. См. файл параметров.