ターゲットプロセッサタイプ (`-target`)

事前定義されたターゲットプロセッサの選択によるデータ型のサイズとエンディアンの指定

説明

コードを展開するプロセッサを指定します。

ターゲットプロセッサにより、ターゲットマシンの基本データ型のサイズとエンディアンが決定されます。リストに無いプロセッサタイプ向けのコードは、そのデータプロパティが共通であれば、他のプロセッサタイプを使用して解析できます。

オプションの設定

以下のいずれかの方法を使用してオプションを設定します。

Polyspace^® ユーザーインターフェイス (デスクトップ製品のみ) — プロジェクト構成で [ターゲットおよびコンパイラ] ノードを選択してから、このオプションの値を選択します。
型のサイズを確認するには、[ターゲットプロセッサタイプ] ドロップダウンリストの右にある [編集] ボタンをクリックします。一部のコンパイラについては、そのコンパイラで許容されるプロセッサのみが表示されます。このようなコンパイラの場合、ユーザーインターフェイスにデータ型のサイズは表示されません。データ型のサイズについては、設定を参照してください。
Polyspace Platform ユーザーインターフェイス (デスクトップ製品のみ) — Polyspace Platform ユーザーインターフェイスではこのオプションの名前は [プロセッサ] であり、サポートされるターゲットは別のリストで表示されます。プロセッサを参照してください。オプション [ターゲットプロセッサタイプ] でサポートされるターゲット (設定にリストされます) は、Polyspace Platform ユーザーインターフェイスで直接選択することはできません。psprj Polyspace プロジェクトファイルを Polyspace Platform ユーザーインターフェイスで開く場合、プロジェクトで使用されるターゲットはカスタムターゲットプロセッサに変換されます。このターゲットは [プロセッサ] オプションにリストされます。
コマンドラインとオプションファイル — オプション -target を使用します。コマンドライン情報を参照してください。

このオプションを使用する理由

プロセッサのデータ型のサイズやその他のプロパティに合わせて Polyspace 実行時チェックの一部が調整されるように、ターゲットプロセッサを指定します。

たとえば、i386 などの 32 ビットのプロセッサでは、x86_64 などの 64 ビットプロセッサに比べて小さな値で変数がオーバーフローする可能性があります。Polyspace 解析に x86_64 を選択しても、コードを i386 プロセッサに展開する場合、Polyspace の結果が必ずしも適切になるとは限りません。

ターゲットプロセッサを選択後、char の既定の符号が符号付きか符号なしかを指定できます。どちらの符号属性を指定するか判断するには、通常使用するコンパイラ設定を使用して、次のコードをコンパイルします。

#include <limits.h>
int array[(char)UCHAR_MAX]; /* If char is signed, the array size is -1

このコードをコンパイルすると、char の既定の符号は符号なしになります。たとえば、GCC コンパイラでは、-fsigned-char フラグを指定してコードをコンパイルします。-funsigned-char フラグを指定してコンパイルすると失敗します。

設定

既定値: i386

次の表は、generic、GCC、Clang、Visual Studio^® の各コンパイラと組み合わせて使用する場合のさまざまなターゲットプロセッサの各基本データ型の想定サイズを示しています。一部のターゲットでは、[ターゲットプロセッサタイプ] ドロップダウンリストの右にある [編集] ボタンをクリックすることで、既定のサイズを変更できます。このようなターゲットのオプション値は表中で大かっこで囲んで示しています。

ターゲット	char	short	int	long	long long	float	double	long double^a	ポインター	char の既定の符号	endian	アライメント
`i386`	8	16	32	32	64	32	64	96	32	符号付き	リトル	32
`sparc`	8	16	32	32	64	32	64	128	32	符号付き	ビッグ	64
`m68k`^b	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
`hc08`^c	8	16	16 [32]	32	32	32	32 [64]	32 [64]	16^d	符号なし	ビッグ	32
`hc12`	8	16	16 [32]	32	32	32	32 [64]	32 [64]	32⁶	符号付き	ビッグ	32
`mpc5xx`	8	16	32	32	64	32	32 [64]	32 [64]	32	符号付き	ビッグ	32
`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	符号付き	リトル	128
`arm`	8	16	32	32	64	32	64	64	32	符号付き	ビッグ	64
`arm64`	8	16	32	64	64	32	64	128	64	符号付き	ビッグ	128
`riscv`	8	16	32	32	64	32	64	128	32	符号付き	ビッグ	128
`riscv64`	8	16	32	64	64	32	64	128	64	符号付き	ビッグ	128
`mcpu...(詳細)`^g	8 [16]	8 [16]	16 [32]	32	32 [64]	32	32 [64]	32 [64]	16 [32]	符号付き	リトル	32
^a For targets where the size of `long double` is greater than 64 bits, the size used for computations is not always the same as the size listed in this table. The exceptions are: For targets `i386`, `x86_64` and `m68k`, 80 bits are used for computations, following the practice in common compilers. For the target `tms320c3x`, 40 bits are used for computation, following the TMS320C3x specifications. If you use a Visual compiler, the size of `long double` used for computations is the same as size of `double`, following the specification of Visual C++^® compilers. ^b The M68k family (68000, 68020, and so on) includes the “ColdFire” processor ^c Non-ANSI C specified keywords and compiler implementation-dependent pragmas and interrupt facilities are not taken into account by this support ^d All kinds of pointers (near or far pointer) have 2 bytes (hc08) or 4 bytes (hc12) of width physically. ^e The `c18` target supports the type `short long` as 24 bits in size. ^f Use option `-long-is-32bits` to support Microsoft^® C/C++ Win64 target. ^g `mcpu` is a reconfigurable Micro Controller/Processor Unit target. You can use this type to configure one or more generic targets. For more information, see `Generic target options`.

ネイティブにサポートされるコンパイラに加えて、Polyspace ではさまざまな専用コンパイラをサポートしています。以下の専用コンパイラに対してサポートされるターゲットプロセッサを選択できます。

ARM^® v5 コンパイラのターゲット — ARM v5 コンパイラ (-compiler armcc) を参照してください。
ARM v6 コンパイラのターゲット — ARM v6 コンパイラ (-compiler armclang) を参照してください。
NXP CodeWarrior^® コンパイラのターゲット — NXP CodeWarrior コンパイラ (-compiler codewarrior) を参照してください。
Cosmic コンパイラのターゲット — Cosmic コンパイラ (-compiler cosmic) を参照してください。
Diab コンパイラのターゲット — Diab コンパイラ (-compiler diab) を参照してください。
Green Hills^® コンパイラのターゲット — Green Hills コンパイラ (-compiler greenhills) を参照してください。
IAR Embedded Workbench コンパイラのターゲット — IAR Embedded Workbench コンパイラ (-compiler iar-ew) を参照してください。
MPLAB XC8 C コンパイラのターゲット — MPLAB XC8 C コンパイラ (-compiler microchip) を参照してください。
Renesas^® コンパイラのターゲット — Renesas コンパイラ (-compiler renesas) を参照してください。
TASKING コンパイラのターゲット — TASKING コンパイラ (-compiler tasking) を参照してください。
Texas Instruments^® コンパイラのターゲット — Texas Instruments コンパイラ (-compiler ti) を参照してください。

ヒント

使用するプロセッサが一覧にない場合は、特性が同じ類似のプロセッサを使用するか、mcpu 汎用ターゲットプロセッサを作成します。汎用ターゲットオプションを参照してください。
オプション -custom-target を使用して基本的な型のサイズなどを明示的に記述することによって、カスタムターゲットを作成することもできます。
構成で -custom-target と -target の両方を使用してターゲットが指定されている場合、解析では -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

例 (Code Prover): polyspace-code-prover -target m68k

例 (Bug Finder Server): polyspace-bug-finder-server -target m68k

例 (Code Prover Server): polyspace-code-prover-server -target m68k

一部のターゲットの既定値は、特定のコマンドラインオプションを使用してオーバーライドできます。汎用ターゲットオプションの「コマンドラインオプション」の節を参照してください。

参考

Polyspace 解析オプション

-custom-target

Polyspace 結果

ローカル変数サイズのより低い推定値 (Polyspace Code Prover) | ローカル変数サイズのより高い推定値 (Polyspace Code Prover)

ターゲット プロセッサ タイプ (-target)

説明