汎用ターゲット オプション

独自のターゲット プロセッサを作成することによるデータ型のサイズとエンディアンの指定

説明

ターゲット プロセッサが Polyspace® で直接サポートされていない場合、独自のターゲットを作成できます。汎用の "マイクロ コントローラー/プロセッサ ユニット" を表すターゲット [mcpu] を指定して、基本データ型のサイズ、エンディアン、およびその他の特性を明示的に指定します。

設定

Polyspace デスクトップ製品のユーザー インターフェイスで、[ターゲット プロセッサ タイプ] を [mcpu] に設定すると [汎用ターゲット オプション] ダイアログ ボックスが開きます。[ターゲット プロセッサ タイプ] オプションは [構成] ペインの [ターゲットおよびコンパイラ] ノードで使用できます。

Example Generic target options dialog box.

このダイアログ ボックスを使用して、新しい [mcpu] ターゲットの名前を、たとえば My_target のように指定します。この新しいターゲットは [ターゲット プロセッサ タイプ] オプション リストに追加されます。

新しいターゲットの既定の特性: "型" [サイズ] としてリスト

  • char [8]

  • short [16]

  • int [16]

  • long [32]

  • long long [32]

  • float [32]

  • double [32]

  • long double [32]

  • pointer [16]

  • alignment [32]

  • char は符号付き

  • endianness はリトル エンディアン

コマンド ライン オプション

コマンド ラインを使用する場合は、-target mcpu をこれらのターゲット指定オプションと共に使用します。

オプション説明利用対象例
-little-endian

リトル エンディアン アーキテクチャは、LSF (下位バイト ファースト) です。例: i386。

short 型整数 (0x00FF など) の下位バイトが最初のバイト (0xFF) に格納され、最上位バイト (0x00) が 2 番目のバイトに格納されるよう指定します。

すべてのターゲットpolyspace-code-prover -lang c -target mcpu -little-endian
-big-endian

ビッグ エンディアン アーキテクチャは、MSF (最上位バイト ファースト) です。以下に例を示します。SPARC、m68k。

short 型整数 (0x00FF など) の最上位バイトが最初のバイト (0x00) に格納され、下位バイト (0xFF) が 2 番目のバイトに格納されるよう指定します。

すべてのターゲット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 とは互換性がありません。

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 [128|64|32|16|8]

スカラー オブジェクト、構造体、クラス、共用体、または配列の最大アライメントを 128、64、32、16 または 8 ビットの境界に指定します。

たとえば、配列または struct 内の基本型のアライメントが常に 8 である場合、配列または struct のストレージは、メンバーと最後のパディングを除く個々のデータ オブジェクトのサイズによって厳密に決定されます。

すべてのターゲットpolyspace-code-prover -target mcpu -align 16

参考:

オプション -custom-target を使用して、基本データ型のバイト単位のサイズ、プレーンな char の符号属性、構造体のアライメント、size_t、wchar_t、ptrdiff_t などの標準的な typedef の潜在型を指定することもできます。

例

GCC ツールチェーン

ソフトウェア開発に以下の GCC ツールチェーンのいずれかを使用する場合は、コードが Polyspace でコンパイルされるように、Polyspace 解析をセットアップすることができます。

  • ARM® Ltd. の GNU® Arm Embedded ツールチェーン

  • HighTec EDV-Systeme

  • Linaro® GNU クロスツールチェーン

  • Melexis®

  • MENTOR® Embedded Sourcery™ CodeBench

  • QNX® ソフトウェア開発プラットフォーム

  • Rowley Associates の CrossWorks

  • STMicroelectronics® TrueSTUDIO® for STM32

  • Texas Instruments® Code Composer Studio™

  • Wind River® GNU Compiler

これらのツールチェーンのいずれかを使用したビルド コマンドで [polyspace-configure] を使用して、コンパイラ構成に関する情報を抽出します。このコマンドは、既定で Polyspace プロジェクトを作成します。コマンド ラインで Polyspace に渡すオプション ファイルを生成するには、オプション -output-options-file を指定して polyspace-configure を実行します。

または、コマンド ラインでコンパイラ構成の詳細を手動で設定する場合は、次のようにします。

GCC および Clang ベースのコンパイラのターゲット

[コンパイラ] (-compiler) オプションで [gnu#.x] コンパイラまたは [clang#.x] コンパイラのいずれかを選択すると、サポートされているいずれかのターゲット プロセッサ タイプを指定できます。ターゲット プロセッサ タイプ (-target) を参照してください。ターゲット プロセッサ タイプがサポート対象として直接表示されない場合、汎用ターゲットのオプションを使用してターゲットを作成できます。

次の表に、作成できるターゲットの例を示します。

GCC ベースのコンパイラ ターゲット

ターゲットオプション
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
ARM64 
-custom-target false,8,2,4,-1,8,8,4,8,16,8,16,1,little,unsigned_long,long,unsigned_int
-D__aarch64__
MSP430 
-target mcpu
-long-long-is-64bits
-double-is-64bits
-wchar-t-type-is signed-long
-align 16
RISC-V
-custom-target false,8,2,4,-1,4,8,4,8,16,4,16,1,big,unsigned_int,int,int
-D__riscv
-D__riscv_xlen=xlen_size
-Dfloat_abi_macro

ここで、以下となります。

  • xlen_size は、ターゲットに応じて 32 または 64 になります。

  • ターゲット プラットフォームのハードウェア アーキテクチャに応じて、float_abi_macro は次のいずれかの値になります。

    • __riscv_float_abi_soft

    • __riscv_float_abi_single

    • __riscv_float_abi_double

    • __riscv_float_abi_quad

PowerPC 
-target mcpu 
-int-is-32bits 
-long-long-is-64bits 
-double-is-64bits 
-pointer-is-32bits 
-wchar-t-type-is signed-int
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

Clang ベースのコンパイラ ターゲット

ターゲットオプション
Cadence Tensilica Xtensa 
-compiler clang10.x
  -custom-target false,8,2,4,-1,4,8,4,8,8,4,8,1,little,unsigned_int,int,unsigned_short
  -D__XTENSA__
  -D__XCC__

Microchip MPLAB XC16 および XC32 コンパイラのエミュレーション

Microchip MPLAB XC16 または XC32 コンパイラを使用してソース コードをビルドする場合、Polyspace でコードがコンパイルされるように Polyspace 解析を設定できます。以下のオプションをコマンド ラインで入力するか、Polyspace デスクトップ ユーザー インターフェイスの [構成] ペインで指定します。

コンパイラターゲット プロセッサ ファミリオプション
MPLAB XC16

PIC24

dsPIC

 
-compiler gnu4.6 
-D__XC__ 
-D__XC16__ 
-target=mcpu 
-wchar-t-type-is unsigned-int 
-align 16 
-long-long-is-64bits
MPLAB XC32PIC32 
-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

オプション [プリプロセッサ定義] (-D) で指定されるマクロのセットは、最小限のセットです。Polyspace で確実にコードがコンパイルされるように、必要に応じて追加のマクロを指定してください。

ヒント

IDE で Polyspace as You Code の拡張機能を使用する場合は、このオプションを解析オプション ファイルに入力します。オプション ファイルを参照してください。

参考

トピック