Exponenta Banner

Предположения о #pragma Директивы

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

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

ПрагмаЭффект на верификации

#pragma asm и #pragma endasm

#asm и #endasm

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

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

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

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

#pragma pack без аргумента обработан как #pragma pack(1).

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

#pragma встраивают глобальный func или #pragma встраивают funcВерификация рассматривает функциональный func как подставляемая функция. В частности, по умолчанию Программа автоматического доказательства Кода сгенерировала main не вызывает эти функции непосредственно учитывая, что они называются в других функциях.

_Pragma("inline=never") func

Верификация не делает подставляемой функции func.
#error message

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

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

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

Например, в этом коде, директивах #pragma пакет (n) обеспечьте новый контур выравнивания в структуре. Пользовательское утверждение регистрируется в 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

Поддержка