Exponenta Banner

Ограничения автоматического оранжевого тестера

Примечание

Автоматический оранжевый тестер будет удален в следующем релизе.

Автоматический оранжевый тестер имеет следующие ограничения:

Неподдерживаемые платформы

Автоматический оранжевый тестер не поддерживается на Mac.

Неподдерживаемые опции Polyspace

Программное обеспечение не поддерживает следующие опции с -automatic-orange-tester.

  • -div-round-down

  • -char-is-16bits

  • -short-is-8bits

В сложение программное обеспечение не поддерживает глобальные утверждения в коде формы Pst_Global_Assert(A,B) .

Опции с ограничениями

Не указывайте следующее с -automatic-orange-tester:

  • -allow-non-finite-floats

  • -check-subnormal

  • -data-range-specification (в глобальном режиме assert)

  • -target [c18 | tms320c3c | x86_64 | sharc21x61]

Вы должны использовать -target mcpu опция вместе с -pointer-is-32bits.

Неподдерживаемые стандартные программы C

Программное обеспечение не поддерживает верификацию кода С, который содержит вызовы следующих стандартных программ:

  • va_start

  • va_arg

  • va_end

  • va_copy

  • setjmp

  • sigsetjmp

  • longjmp

  • siglongjmp

  • signal

  • sigset

  • sighold

  • sigrelse

  • sigpause

  • sigignore

  • sigaction

  • sigpending

  • sigsuspend

  • sigvec

  • sigblock

  • sigsetmask

  • sigprocmask

  • siginterrupt

  • srand

  • srandom

  • initstate

  • setstate

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

Поддержка