-asm-begin -asm-end

Exclude compiler-specific asm functions from analysis

Syntax

-asm-begin "mark1[,mark2,...]" -asm-end "mark1[,mark2,...]"


Description

-asm-begin "mark1[,mark2,...]" -asm-end "mark1[,mark2,...]" excludes compiler-specific assembly language source code functions from the analysis. You must use these two options together.

Polyspace^® recognizes most inline assemblers by default. Use the option only if compilation errors occur due to introduction of assembly code. For more information, see Code Prover Assumptions About Assembly Code (Polyspace Code Prover).

Mark the offending code block by two #pragma directives, one at the beginning of the assembly code and one at the end. In the command usage, give these marks in the same order for -asm-begin as they are for -asm-end.

If you are running an analysis from the user interface (Polyspace desktop products only), on the Configuration pane, you can enter this option in the Other field. See Other.

Examples

A block of code is delimited by #pragma start1 and #pragma end1. These names must be in the same order for their respective options. Either:

-asm-begin "start1" -asm-end "end1"

or

-asm-begin "mark1,...markN,start1" -asm-end "mark1,...markN,end1"

The following example marks two functions for exclusion, foo_1 and foo_2.

Code:

#pragma asm_begin_foo
int foo(void) { /* asm code to be ignored by Polyspace */ }
#pragma asm_end_foo

#pragma asm_begin_bar
void bar(void) { /* asm code to be ignored by Polyspace */ }
#pragma asm_end_bar

Polyspace Command:

• Bug Finder:

  polyspace-bug-finder -lang c -asm-begin "asm_begin_foo,asm_begin_bar"
            -asm-end "asm_end_foo,asm_end_bar"

• Code Prover:

  polyspace-code-prover -lang c -asm-begin "asm_begin_foo,asm_begin_bar"
           -asm-end "asm_end_foo,asm_end_bar"

• Bug Finder Server:

  polyspace-bug-finder-server -lang c -asm-begin "asm_begin_foo,asm_begin_bar"
            -asm-end "asm_end_foo,asm_end_bar"

• Code Prover Server:

  polyspace-code-prover-server -lang c -asm-begin "asm_begin_foo,asm_begin_bar"
           -asm-end "asm_end_foo,asm_end_bar"

asm_begin_foo and asm_begin_bar mark the beginning of the assembly source code sections to be ignored. asm_end_foo and asm_end_bar mark the end of those respective sections.

Tips

If you use Polyspace as You Code extensions in IDEs, enter this option in an analysis options file. See options file.