Configure Run-time Checks

Modify the behavior of Polyspace^® run-time checks

Configure how Polyspace analyzes your code and checks for runtime errors:

Overflow — Configure how Polyspace calculates an overflow on signed and unsigned integers.
Pointers — Configure how Polyspace analyzes pointers and function pointers.
Dead code — Configure how Polyspace detects dead code.
Floating point — Configure how Polyspace handles nonfinite and nonnumber floating points.

Polyspace Options

Overflow

`Allow negative operand for left shifts (-allow-negative-operand-in-shift)`	Allow left shift operations on a negative number
`Overflow mode for signed integer (-signed-integer-overflows)`	Specify whether result of overflow is wrapped around or truncated
`Overflow mode for unsigned integer (-unsigned-integer-overflows)`	Specify whether result of overflow is wrapped around or truncated
`-show-similar-overflows`	Show all overflows in wrap-around mode

Pointers

`Detect stack pointer dereference outside scope (-detect-pointer-escape)`	Find cases where a function returns a pointer to one of its local variables
`Enable pointer arithmetic across fields (-allow-ptr-arith-on-struct)`	Allow arithmetic on pointer to a structure field so that it points to another field
`Allow incomplete or partial allocation of structures (-size-in-bytes)`	Allow a pointer with insufficient memory buffer to point to a structure
`Permissive function pointer calls (-permissive-function-pointer)`	Allow type mismatch between function pointers and the functions they point to

Dead Code

Detect uncalled functions (-uncalled-function-checks) Detect functions that are not called directly or indirectly from main or another entry point function

Floating Point

`Consider non finite floats (-allow-non-finite-floats)`	Enable an analysis mode that incorporates infinities and NaNs
`Infinities (-check-infinite)`	Specify how to handle floating-point operations that result in infinity
`NaNs (-check-nan)`	Specify how to handle floating-point operations that result in NaN
`Subnormal detection mode (-check-subnormal)`	Detect operations that result in subnormal floating-point values

Code Behavior Specification

-code-behavior-specifications Associate behaviors with code elements such as functions

Parameters of Stubbed Function

-check-parameter-of-stubbed-functions Enable checking pointer parameters of stubbed functions

Topics

Modify Default Behavior of Runtime Checks

Modify or Disable Code Prover Run-Time Checks

Disable a subset of run-time checks in Code Prover.
- Modify Code Prover Run-Time Checks Through Code Behavior Specifications
Detect Overflows in Buffer Size Computation
Detect overflows earlier during buffer size computation instead of later during buffer usage.

Related Information

Configure Analysis Precision