Check Behavior

Modify default behavior of run-time checks

To modify the default behavior of a run-time check, use the check behavior options. For instance, by default, the Overflow check detects overflows in computations with signed integers only. You can specify that the check must also detect overflows in computations with unsigned integers.

Polyspace Options

expand all

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

Initialization

`Disable checks for non-initialization (-disable-initialization-checks)`	Disable checks for non-initialized variables and pointers
`Check that global variables are initialized after warm reboot (-check-globals-init)`	Check that global variables are assigned values in designed initialization code (Since R2020a)

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

Impact Analysis

`Enable impact analysis (-impact-analysis)`	Check for presence or absence of impact between program elements designated as sources and sinks (Since R2023b)
`Specify sources and sinks (-impact-specifications)`	Specify XML file that identifies program elements as sources and sinks for impact analysis (Since R2023b)
`Show impact analysis results only (-impact-analysis-only)`	Skip regular Code Prover checks for run-time errors and perform impact analysis only (Since R2023b)

Stack Usage

Calculate stack usage (-stack-usage) Compute and display the estimates of stack usage (Since R2022a)

Topics

Modifying Default Behavior of Run-time Checks

Specify Polyspace Analysis Options
Specify Polyspace^® analysis options in Polyspace user interface, other IDE-s or scripts.
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.

Setting up Impact Analysis

Prove Absence of Impact Between Objects in C/C++ Program
Set up impact analysis in Polyspace Code Prover™, define sources and sinks.
Source and Sink Specifications for Impact Analysis in Polyspace Code Prover
Look up XML syntax for designating variables and function arguments as sources and sinks.
Event and Memory Zone Specifications for Impact Analysis in Polyspace Code Prover
Look up XML syntax for specifying events and memory zones associated with impact sinks.