アセンブリコードに関する Code Prover の仮定

Polyspace^® は、ほとんどのインラインアセンブラーをアセンブリコードの開始と認識します。解析では、アセンブリコードが無視されますが、このアセンブリコードは C コードで変数を変更できると見なされます。

認識されるインラインアセンブラー

Polyspace は、以下のインラインアセンブラーをアセンブリコードの開始と認識します。

asm

例:

int f(void)
{
	asm ("% reg val; mtmsr val;");
	asm("\tmove.w #$2700,sr");
	asm("\ttrap #7");
	asm(" stw r11,0(r3) ");
	assert (1); // is green
	return 1;
}

int other_ignored2(void)
{
	asm "% reg val; mtmsr val;";
	asm mtmsr val;
	assert (1); // is green
	asm ("px = pm(0,%2); \
		%0 = px1; \
		%1 = px2;"
		: "=d" (data_16), "=d" (data_32)
		: "y" ((UI_32 pm *)ram_address):
"px");
	assert (1); // is green
}

int other_ignored4(void)
{
	asm {
		port_in: /* byte = port_in(port); */
		mov EAX, 0
		mov EDX, 4[ESP]
			in AL, DX
			ret
			port_out: /* port_out(byte,port); */
		mov EDX, 8[ESP]
		mov EAX, 4[ESP]
		out DX, AL
		ret }
assert (1); // is green
}

__asm__

例:

int other_ignored6(void)
{
#define A_MACRO(bus_controller_mode) \
	__asm__ volatile("nop"); \
	__asm__ volatile("nop"); \
	__asm__ volatile("nop"); \
	__asm__ volatile("nop"); \
	__asm__ volatile("nop"); \
	__asm__ volatile("nop")
		assert (1); // is green
		A_MACRO(x);
		assert (1); // is green
		return 1;
}

int other_ignored1(void)
{
	__asm
		{MOV R8,R8
		MOV R8,R8
		MOV R8,R8
		MOV R8,R8
		MOV R8,R8}
	assert (1); // is green
}

int GNUC_include (void)
{
	extern int __P (char *__pattern, int __flags,
	int (*__errfunc) (char *, int),
	unsigned *__pglob) __asm__ ("glob64");
	__asm__ ("rorw $8, %w0" \
		: "=r" (__v) \
		: "0" ((guint16) (val)));
	__asm__ ("st g14,%0" : "=m" (*(AP)));
	__asm("" \
		: "=r" (__t.c) \
		: "0" ((((union { int i, j; } *) (AP))++)->i));
	assert (1); // is green
	return (int) 3 __asm__("% reg val");
}

int other_ignored3(void)
{
	__asm {ldab 0xffff,0;trapdis;};
__asm {ldab 0xffff,1;trapdis;};
	assert (1); // is green
	__asm__ ("% reg val");
	__asm__ ("mtmsr val");
	assert (1); // is green
	return 2;
}

#pragma asm #pragma endasm

例:

int pragma_ignored(void)
{
	#pragma asm
		SRST
	#pragma endasm
		assert (1); // is green
}

void test(void)
{
  #asm
    mov _as:pe, reg
	   jre _nop
  #endasm
	 int r;
	 r=0;
	 r++;
}

認識されないアセンブリ命令をバイパスする

アセンブリコードの開始が原因でコンパイルエラーが発生する場合は以下を行います。

アセンブリコードを #pragma my_asm_begin ステートメントと #pragma my_asm_end ステートメントの間に組み込みます。
解析オプション -asm-begin my_asm_begin -asm-end my_asm_end を指定します。

詳細は、-asm-begin -asm-endを参照してください。

解析でのアセンブリ命令に関する仮定

アセンブリコードを含む関数全体

単一の関数. 先頭に asm がある関数は、本体が定義されていてもソフトウェアでスタブ化されます。

asm int h(int tt)              // function h is stubbed even if body is defined
{ 
  % reg val;                   // ignored 
  mtmsr val;                  // ignored 
  return 3;                     // ignored 
}; 

void f(void) { 
  int x; 
  x = h(3);                     // x is full-range 
}

関数のグループ. 次のプラグマで指定した関数は、関数本体が定義されていても自動的にスタブ化されます。

#pragma inline_asm(list of functions)

コード例:

#pragma inline_asm(ex1, ex2) 
   // The functions ex1 and ex2 are 
   // stubbed, even if their bodies are defined 

int ex1(void) 
{ 
  % reg val; 
  mtmsr val; 
  return 3;                       // ignored 
}; 

int ex2(void) 
{ 
  % reg val; 
  mtmsr val; 
  assert (1);                    // ignored 
  return 3; 
}; 


#pragma inline_asm(ex3)  // the definition of ex3 is ignored 

int ex3(void) 
{ 
  % reg val; 
  mtmsr val; 				// ignored 
  return 3; 
}; 

void f(void) { 
  int x; 

  x = ex1();   				// ex1 is stubbed : x is full-range 
  x = ex2();   				// ex2 is stubbed : x is full-range 
  x = ex3();   				// ex3 is stubbed : x is full-range 
}

C/C++ とアセンブリコードが混在する関数

解析では、アセンブリ言語命令の内容は無視されますが、その命令の後、次のように仮定されます。

未初期化ローカル変数: アセンブリ命令でこれらの変数を初期化できます。
初期化されたローカル変数: アセンブリ命令で変数のデータ型で許容される可能性がある任意の値を変数に書き込むことができます。

これらの保守的な仮定を回避して、アセンブリ命令をすべて無視するには、解析オプション [アセンブリコードを無視] (-ignore-assembly-code) を指定します。

たとえば、関数 f には asm ステートメントから開始されるアセンブリコードがあるとします。

int f(void) { 
    int val1, val2 = 0; 
    asm("mov 4%0,%%eax"::"m"(val1));
    return (val1 + val2); 
}

return ステートメントの [未初期化ローカル変数] チェックは次の結果になります。

val1:アセンブリ命令により val1 を初期化できるため、チェックはオレンジになります。
val2:チェックは、グリーンになります。ただし、val2 は int 型の任意の値になる可能性があります。

変数が静的変数の場合、アセンブリ命令前でも、関数本体のどこでも仮定は true になります。

参考

-asm-begin -asm-end | アセンブリコードを無視 (-ignore-assembly-code)

アセンブリ コードに関する Code Prover の仮定

認識されるインライン アセンブラー