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:

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)`

Violation of Impact Specifications

Checker Default Behavior Option

Checker	Default Behavior	Option
`Expected impact` `Expected absence of impact`	Code Prover does not check for impact between program elements designated as sources and sinks.	`Enable impact analysis (-impact-analysis)` `Specify sources and sinks (-impact-specifications)` `Show impact analysis results only (-impact-analysis-only)`

Code Prover does not check for impact between program elements designated as sources and sinks.