Exponenta Banner
exponenta event banner

Допущения о #pragma Директивы

Верификация игнорирует большинство #pragma директивы, поскольку они не содержат информацию, относящуюся к верификации.

Однако при верификации учитывается поведение этих прагм.

PragmaЭффект на верификацию

#pragma asm и #pragma endasm

#asm и #endasm

В верификацию игнорируется содержание между прагмами.

Если вы используете # pragma inline_asm func, верификация считает, что функция func содержит инструкции уровня сборки и игнорирует тело функции.

#pragma hdrstopДля Visual C++® компиляторы, верификация останавливает обработку предварительно скомпилированных заголовков в точке, где она встречается с прагмой.
#pragma onceЭта верификация позволяет включать текущий исходный файл только один раз в компиляцию.
#pragma pack(n), #pragma pack(push[,n]), #pragma pack(pop)

В верификацию учитывается выравнивание границ, заданное в прагмах.

#pragma pack без аргумента рассматривается как #pragma pack(1).

Для получения дополнительной информации см. следующий пример.

# pragma inline global func или # pragma inline funcФункция рассматривается верификацией func как встроенная функция. В частности, по умолчанию Code Prover сгенерировал main не вызывает эти функции непосредственно с предположением, что они вызываются в других функциях.

_Pragma("inline=never") func

Функция верификации не встроена func.
# ошибка message

Если верификация встречается с директивой, то он останавливается.

Для получения дополнительной информации смотрите Ошибка, связанная с Директивой об ошибках #.

Для получения дополнительной информации о прагмах см. документацию компилятора. Если верификация не учитывает определенную прагму из предыдущего списка, смотрите, указали ли вы правильный компилятор для своей верификации. Для получения дополнительной информации смотрите Compiler (-compiler).

Например, в этом коде директивы # pragma pack (n) форсировать новый контур выравнивания в колодце. Проверка типа «User» (Пользователь) выполняет проверку main функция зеленая, потому что верификация учитывает поведение директивы. В верификацию используются следующие опции:

#include <assert.h>

#pragma pack(2)

struct _s6 {
    char c;
    int i;
} s6;

#pragma pack() /* Restores default packing: pack(4) */

struct _sb {
    char c;
    int i;
} sb;

#pragma pack(1)

struct _s5 {
    char c;
    int i;
} s5;


int main(void) {
    assert(sizeof(s6) == 6);
    assert(sizeof(sb) == 8);
    assert(sizeof(s5) == 5);
    return 0;
}

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

Поддержка