Modify or Disable Code Prover Run-Time Checks

A Code Prover analysis exhaustively checks source code for common run-time errors. The exhaustive nature of the static analysis is designed to prevent the errors from occurring at run time in safety critical software. Because of the safety critical intent of the analysis, Code Prover does not allow you to:

• Selectively disable specific run-time checks.

• Hide results of run-time checks from the results list through source code annotations. You can justify the results through annotations but the justified results continue to appear in the results list.

You can choose to suppress specific results by applying filters after the analysis or even creating filtered reports. If you create a filtered report from the Code Prover results, the report shows the filters and reflects your choices. For more information, see:

• Filter and Sort Results in Polyspace Platform User Interface or Filter and Sort Results in Polyspace Access Web Interface (Polyspace Access)

• Generate Reports from Polyspace Results or polyspace-report-generator

However, you can modify the default behavior of certain checks and completely disable the checks for initialization. When you generate a report from the analysis results, the report shows the use of these options.

This topic lists the options that modify the default behavior of certain run-time checks. Note that though an option primarily addresses a specific type of check, checks of other types are also impacted. See Code Prover Analysis Following Red and Orange Checks.

Integer Overflow

Check	Default Behavior	Option
Invalid shift operations	Left shifts are not allowed on signed operands.	Allow negative operand for left shifts (-allow-negative-operand-in-shift)
Overflow	Signed integer overflows are forbidden.	Overflow mode for signed integer (-signed-integer-overflows)
Overflow	Unsigned integer overflows are not detected.	Overflow mode for unsigned integer (-unsigned-integer-overflows)

Floating Point Overflow

Check	Default Behavior	Option
Overflow Invalid operation on floats	Non-finite floats are not considered.	Consider non finite floats (-allow-non-finite-floats) Infinities (-check-infinite) NaNs (-check-nan)
Subnormal float	Subnormal results are not detected.	Subnormal detection mode (-check-subnormal)

Initialization

Check	Default Behavior	Option
Non-initialized local variable Non-initialized variable Non-initialized pointer Return value not initialized	Checks for initialization are performed only when a variable is read.	Disable checks for non-initialization (-disable-initialization-checks)
Global variable not assigned a value in initialization code	Checks for global variable initialization is performed only when the variable is read.	Ignore default initialization of global variables (-no-def-init-glob) Check that global variables are initialized after warm reboot (-check-globals-init)

Library Functions

Check	Default Behavior	Option
Invalid use of standard library routine	Only Standard Library routines are checked for validity of arguments. User-defined library functions are not checked.	-code-behavior-specifications

Pointers

Check	Default Behavior	Option
Illegally dereferenced pointer	Pointers to a structure field cannot point to another field.	Enable pointer arithmetic across fields (-allow-ptr-arith-on-struct)
Illegally dereferenced pointer	Pointers to a structure must have enough buffer for the entire structure.	Allow incomplete or partial allocation of structures (-size-in-bytes)
Illegally dereferenced pointer	Stack pointer dereference outside scope is not detected.	Detect stack pointer dereference outside scope (-detect-pointer-escape)
Correctness condition	Function pointer mismatches are not allowed.	Permissive function pointer calls (-permissive-function-pointer)

Unreachable Code or Dead Code

Checker	Default Behavior	Option
Function not called Function not reachable	Uncalled functions and functions called from unreachable code are not reported.	Detect uncalled functions (-uncalled-function-checks)