Exponenta Banner

- asm-начните - asm-конец

Исключите специфичные для компилятора функции 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:

  • Средство поиска ошибки:

    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"

  • Сервер средства поиска ошибки:

    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 Code Prover
Поддержка