To avoid unproven results (orange checks) from causes outside your code, Code Prover assumes that certain kinds of inputs are safe in certain ways. For instance, pointers from external sources are assumed non-NULL by default.
See a list of assumptions here. This list shows both permissive and conservative assumptions made in the default Code Prover analysis.
Why Polyspace Verification Uses Approximations
Learn how static verification uses approximations to perform a superior run-time error checking compared to dynamic approaches.
Assumptions About Variable Ranges
The verification uses the data type of an external variable to extract its possible range of values.
Assumptions About Stubbed Functions
The verification stubs undefined functions or functions that you want stubbed, and makes certain assumptions about their arguments and return values.
Assumptions About main Function
The verification assumes some constraints on the main
function arguments.
Assumptions About Global Variable Initialization
The verification assumes initialization of global
variables by ANSI® C standards, for instance, 0 for int.
Assumptions About Volatile Variables
The verification assumes that a volatile variable can take any possible value at any point in your code.
Assumptions About Variable and Function Definitions and Declarations
The verification exhibits different behaviors for undeclared and undefined variables or functions.
Assumptions About Standard Library Float Routines
For some two-argument standard library float routines, the verification can ignore the function arguments and assume that the function returns all possible values in its range.
The verification assumes all possible values if you write to a union member but read back a different member of the same union.
Assumptions About Variables Cast as Void Pointers
The verification loses precision if you cast a variable
to a void* pointer.
Assumptions About Implicit Data Type Conversions
The verification can assume implicit type conversion for binary operations depending on the operand data types.
Assumptions About memset and memcpy
The verification checks only for certain issues when
you use memcpy and memset, and
makes some assumptions following its use.
Assumptions About #pragma Directives
The verification takes into account only certain #pragma directives
because most such directives are not relevant to the verification.
Assumptions About Assembly Code
The verification recognizes inline assemblers as introducing assembly code and ignores the operations in the assembly code.
Determination of Program Stack Usage
The verification estimates stack usage from the function call hierarchy and local variable sizes.
Limitations of Polyspace Verification
Look up the list of acknowledged limitations of Polyspace® verification regarding specific code constructs.