-asm-begin -asm-end

将编译器特定的 asm 函数排除在分析之外

语法

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

描述

-asm-begin "mark1[,mark2,...]" -asm-end "mark1[,mark2,...]" 将编译器特定的汇编语言源代码函数排除在分析之外。您必须同时使用这两个选项。

默认情况下，Polyspace® 可识别大多数内联汇编器。仅当由于引入了汇编代码而导致编译错误时，才使用此选项。有关详细信息，请参阅Code Prover Assumptions About Assembly Code。

使用两个 #pragma 指令标记有问题的代码块，一个放在汇编代码的开头，一个放在末尾。在命令使用中，为 -asm-end 提供这些标记的顺序需与为 -asm-begin 提供标记的顺序相同。

在用户界面（仅限 Polyspace 桌面端产品）中，在配置窗格的其他字段中输入此选项。请参阅其他。

示例

代码块以 #pragma start1 和 #pragma end1 分隔。这些名称必须与其对应选项采用相同的顺序。以下任一项：

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

下面的示例标记了两个要排除的函数，即 foo_1 和 foo_2。

代码：

#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 命令：

  • 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 和 asm_begin_bar 标记要忽略的汇编源代码段的开头。asm_end_foo 和 asm_end_bar 标记这些对应代码段的末尾。

提示

如果您使用 IDE 中的 Polyspace as You Code 扩展，请在分析选项文件中输入此选项。请参阅选项文件。

另请参阅

主题