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 (в глобальной переменной утверждают режим),

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