Code Prover Assumptions About Assembly Code

Polyspace^® recognizes most inline assemblers as introduction of assembly code. The analysis ignores the assembly code but accounts for the fact that the assembly code can modify variables in the C code.

Recognized Inline Assemblers

Polyspace recognizes these inline assemblers as introduction of assembly code.

asm

Examples:

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__

Examples:

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

Examples:

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++;
}

Bypassing Unrecognized Assembly Instructions

If introduction of assembly code causes compilation errors:

Embed the assembly code between a #pragma my_asm_begin and a #pragma my_asm_end statement.
Specify the analysis option -asm-begin my_asm_begin -asm-end my_asm_end.

For more information, see -asm-begin -asm-end.

Analysis Assumptions Around Assembly Instructions

Entire Functions Containing Assembly Code

Single Function. The software stubs a function that is preceded by asm, even if a body is defined.

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 
}

Groups of Functions. The functions that you specify through the following pragma are stubbed automatically, even if function bodies are defined.

#pragma inline_asm(list of functions)

Code examples:

#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 
}

Functions Containing Mix of C/C++ and Assembly Code

The analysis ignores the content of assembly language instructions, but following the instructions, it makes some assumptions about:

Uninitialized local variables: The assembly instructions can initialize these variables.
Initialized local variables: The assembly instructions can write any possible value to the variables allowed by the variable data types.

If you want to avoid these conservative assumptions and ignore the assembly instructions altogether, specify the analysis option Ignore assembly code (-ignore-assembly-code).

For instance, the function f has assembly code introduced through the asm statement.

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

On the return statement, the Non-initialized local variable check has the following results:

val1: The check is orange because the assembly instruction can initialize val1.
val2: The check is green. However, val2 can have any int value.

If the variable is static, the assumptions are true anywhere in the function body, even before the assembly instructions.