Exponenta Banner

-asm-begin -asm-end

Исключить специфичные для компилятора asm функции из анализа

Синтаксис

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

Описание

-asm-begin "mark1[,mark2,...]" -asm-end "mark1[,mark2,...]" исключает из анализа специфичные для компилятора функции исходного кода языка сборки. Вы должны использовать эти две опции вместе.

Polyspace® распознает большинство встроенных сборок по умолчанию. Используйте опцию только в случае возникновения ошибок компиляции из-за введения кода сборки. Для получения дополнительной информации смотрите Допущения о коде сборки.

Отметьте обидный кодовый блок двумя #pragma директивы, один в начале кода сборки и один в конце. При использовании команды задайте эти метки в том же порядке для -asm-begin как они для -asm-end.

Если анализ запускается из пользовательского интерфейса (только для десктопных продуктов Polyspace), на панели Configuration можно ввести эту опцию в поле Other. См. Other.

Примеры

Блок кода разделяется #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:

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

  • Код Code Prover:

    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 отметьте конец соответствующих разделов.

Совет

Если вы используете Polyspace в качестве расширений You Code в IDE, введите эту опцию в файл опций анализа. См. файл опций.

См. также

Темы

Документация Polyspace Code Prover

Поддержка