#pragma
ДирективыВерификация игнорирует большинство #pragma
директивы, поскольку они не содержат информацию, относящуюся к верификации.
Однако при верификации учитывается поведение этих прагм.
Pragma | Эффект на верификацию |
---|---|
| В верификацию игнорируется содержание между прагмами. Если вы используете |
#pragma hdrstop | Для Visual C++® компиляторы, верификация останавливает обработку предварительно скомпилированных заголовков в точке, где она встречается с прагмой. |
#pragma once | Эта верификация позволяет включать текущий исходный файл только один раз в компиляцию. |
#pragma pack(n) , #pragma pack(push[,n]) , #pragma pack(pop) | В верификацию учитывается выравнивание границ, заданное в прагмах.
Для получения дополнительной информации см. следующий пример. |
# pragma inline global или # pragma inline | Функция рассматривается верификацией как встроенная функция. В частности, по умолчанию Code Prover сгенерировал main не вызывает эти функции непосредственно с предположением, что они вызываются в других функциях. |
| Функция верификации не встроена func . |
# ошибка | Если верификация встречается с директивой, то он останавливается. Для получения дополнительной информации смотрите Ошибка, связанная с Директивой об ошибках #. |
Для получения дополнительной информации о прагмах см. документацию компилятора. Если верификация не учитывает определенную прагму из предыдущего списка, смотрите, указали ли вы правильный компилятор для своей верификации. Для получения дополнительной информации смотрите Compiler (-compiler)
.
Например, в этом коде директивы # pragma pack
форсировать новый контур выравнивания в колодце. Проверка типа «User» (Пользователь) выполняет проверку (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; }