Code Prover Assumptions About `#pragma` Directives

The verification ignores most #pragma directives, because they do not carry information relevant to the verification.

However, the verification takes into account the behavior of these pragmas.

Pragma	Effect on Verification
`#pragma asm` and `#pragma endasm` `#asm` and `#endasm`	The verification ignores the content between the pragmas. If you use `#pragma inline_asm func`, the verification considers that the function `func` contains assembly level instructions and ignores the function body.
`#pragma hdrstop`	For Visual C++^® compilers, the verification stops processing precompiled headers at the point where it encounters the pragma.
`#pragma once`	The verification allows the current source file to be included only once in a compilation.
`#pragma pack(n)`, `#pragma pack(push[,n])`, `#pragma pack(pop)`	The verification takes into account the boundary alignment specified in the pragmas. `#pragma pack` without an argument is treated as `#pragma pack(1)`. For more information, see the following example.
`#pragma inline global func` or `#pragma inline func`	The verification considers the function `func` as an inline function. In particular, by default, the Code Prover generated `main` does not call these functions directly with the assumption that they are called in other functions.
`_Pragma("inline=never")` `func`	The verification does not inline function `func`.
`#error message`	The verification stops if it encounters the directive. For more information, see Fix Polyspace Compilation Errors Related to #error Directive.

For more information on the pragmas, see your compiler documentation. If the verification does not take into account a certain pragma from the preceding list, see if you specified the right compiler for your verification. For more information, see Compilation toolchain (Static analysis).

For instance, in this code, the directives #pragma pack(n) force a new alignment boundary in the structure. The User assertion checks in the main function are green because the verification takes into account the behavior of the directives. The verification uses these options:

-target: i386 (char: 1 byte, int: 4 bytes)
Compilation toolchain (Static analysis): 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;
}

Code Prover Assumptions About #pragma Directives

Code Prover Assumptions About `#pragma` Directives