Exponenta Banner

Допущения о коде сборки

Polyspace® распознает большинство встроенных сборок как введение кода сборки. Эта верификация игнорирует код сборки, но учитывает тот факт, что код сборки может изменять переменные в коде C.

Если введение кода сборки вызывает ошибки компиляции:

  1. Встройте код сборки между my_asm_begin # pragma и # прагма my_asm_end оператор.

  2. Задайте опцию анализа -asm-begin my_asm_begin -asm-end my_asm_end.

Для получения дополнительной информации смотрите -asm-begin -asm-end.

Распознанные встроенные сборщики

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

Одна функция, содержащая код сборки

Программа заглушает функцию, которой предшествуют 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 
}

Локальные переменные в функциях с кодом сборки

Верификация игнорирует содержимое инструкций по языку сборки, но следуя инструкциям, делает некоторые предположения о:

  • Неинициализированные локальные переменные: Инструкции по сборке могут инициализировать эти переменные.

  • Инициализированные локальные переменные: Инструкции по сборке могут записать любое возможное значение в переменные, разрешенные типами данных переменных.

Для образца - функция f имеет код сборки, введенный через asm оператор.

int f(void) { 
    int val1, val2 = 0; 
    asm("mov 4%0,%%eax"::"m"(val1));
    return (val1 + val2); 
}
На return оператор, проверка Non-initialized local variable имеет следующие результаты:

  • val1: Проверка оранжевая, потому что инструкция сборки может инициализировать val1.

  • val2: Чек зеленый. Однако val2 может иметь любое int значение.

Если переменная является статической, допущения верны где угодно в теле функции, даже перед инструкциями сборки.

Документация Polyspace Code Prover

Поддержка