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 Compiler (-compiler).

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 processor type (-target): i386 (char: 1 byte, int: 4 bytes)

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