Exponenta Banner

Типичные целевые опции

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

Описание

Если целевой процессор непосредственно не поддержан Polyspace®, можно создать собственную цель. Вы задаете целевой mcpu, представляющий типичный "Микро Контроллер/Процессор", и затем явным образом задаете размеры основополагающих типов данных, порядка байтов и других характеристик.

Настройки

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

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

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

  • символьный [8]

  • короткий [16]

  • int16

  • длинный [32]

  • долго длинный [32]

  • [32] плавающий

  • двойной [32]

  • долго двойной [32]

  • указатель [16]

  • char подписывается

  • порядок байтов является прямым порядком байтов

Зависимость

Пользовательская цель может только быть создана, когда Target processor type (-target) установлен в mcpu.

Пользовательская цель не доступна, когда Compiler (-compiler) установлен в одну из опций visual*.

Параметры командной строки

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

ОпцияОписаниеДоступный сПример
-little-endian

Архитектура с прямым порядком байтов является Менее значительным байтом, Первым (LSF). Например: i386.

Указывает, что менее значительный байт короткого целого (например, 0x00FF) хранится на уровне первого байта (0xFF) и старшего значащего байта (0x00) на уровне второго байта.

mcpupolyspace-code-prover -lang c -target mcpu -little-endian
-big-endian

Архитектура с обратным порядком байтов является Старшим значащим байтом, Первым (MSF). Например: SPARC, m68k.

Указывает, что старший значащий байт короткого целого (например, 0x00FF) хранится на уровне первого байта (0x00) и менее значительного байта (0xFF) на уровне второго байта.

mcpupolyspace-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

mcpupolyspace-code-prover -target mcpu -char-is-16bits
-short-is-8bitsЗадайте short как 8 битов, независимо от знакаmcpupolyspace-code-prover -target mcpu -short-is-8bits
-int-is-32bitsЗадайте int как 32 бита, независимо от знака. Выравнивание также установлено в 32 бита.mcpu, hc08, hc12, mpc5xxpolyspace-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 бита.mcpupolyspace-code-prover -target mcpu -long-long-is-64bits
-double-is-64bitsЗадайте double и long double как 64 бита, независимо от знака.mcpu, sharc21x61, hc08, hc12, mpc5xxpolyspace-code-prover -target mcpu -double-is-64bits
-pointer-is-24bitsЗадайте указатель как 24 бита, независимо от знака.c18polyspace-code-prover -target c18-pointer-is-24bits
-pointer-is-32bitsЗадайте указатель как 32 бита, независимо от знака.mcpupolyspace-code-prover -target mcpu -pointer-is-32bits
-align [32|16|8]

Задает самое большое выравнивание struct, или массив возражает против этих 32, контуров на 16 или 8 битов.

Следовательно, устройство хранения данных массива или struct строго определяется размером отдельных объектов данных без дополнения конца и участника.

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 основанные компиляторы

Если вы выбираете один из компиляторов 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

Смотрите также

Темы

Документация Polyspace Code Prover
Поддержка