Директивы #pragma

`#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 функция является зеленой, потому что верификация учитывает поведение директив. Верификация использует эти опции:

Target processor type (-target): i386 'char': 1 байт, int: 4 байта)
Compiler (-compiler): gnu4.9

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

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

`#pragma` Директивы

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

Поддержка

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

#pragma Директивы

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

Поддержка

`#pragma` Директивы