Exponenta Banner

-asm-begin -asm-end

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

Синтаксис

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

Описание

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

Polyspace® распознает большинство встроенных ассемблеров по умолчанию. Используйте опцию, только если ошибки компиляции происходят из-за введения ассемблерного кода. Для получения дополнительной информации смотрите Предположения Об Ассемблерном коде (Polyspace Code Prover).

Отметьте незаконный блок кода двумя #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"

  • Программа автоматического доказательства кода:

    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"

  • Сервер программы автоматического доказательства кода:

    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 в качестве Вас Расширения кода в ИДАХ, введите эту опцию в файл опций анализа. Смотрите файл опций.

Смотрите также

Темы

Документация Polyspace Bug Finder

Поддержка