Configure Analysis Precision

Configure Code Prover assumptions and verification precision

Use precision options to configure the verification precision. More precise verification produces fewer orange checks but requires more computational resources. You can configure:

  • Global precision — Specify options that impact the precision at the engine level. These precision options can impact any Polyspace® Code Prover™ analysis.

  • Files and functions — These options specify how Code Prover analyses functions and source files.

  • Arrays and pointers — These options specify how arrays and pointers are modeled and analyzed.

  • Assembly code — These options specify how assembly functions are handled.

Polyspace Options

expand all

Precision level (-O0 | -O1 | -O2 | -O3)Specify a precision level for the verification
Verification level (-to)Specify number of times the verification process runs on your code
Verification time limit (-timeout)Specify a time limit on your analysis
Sensitivity context (-context-sensitivity)Store call context information to identify function call that caused errors
Improve precision of interprocedural analysis (-path-sensitivity-delta)Avoid certain verification approximations for code with fewer lines
Specific precision (-modules-precision)Specify source files you want to verify at higher precision than the remaining verification
-consider-external-array-access-unsafeRemove the default assumption that external arrays of unspecified size can be safely accessed at any index
-improve-pointer-analysis-precisionEnable more precise pointer analysis mode in Code Prover (Since R2022a)
-no-assumption-on-absolute-addressesRemove assumption that absolute address usage is valid
Consider environment pointers as unsafe (-stubbed-pointers-are-unsafe)Specify that environment pointers can be unsafe to dereference unless constrained otherwise
-consider-external-array-access-unsafeRemove the default assumption that external arrays of unspecified size can be safely accessed at any index
-improve-pointer-analysis-precisionEnable more precise pointer analysis mode in Code Prover (Since R2022a)
-asm-begin -asm-endExclude compiler-specific asm functions from analysis
Ignore assembly code (-ignore-assembly-code)Specify that assembly instructions in C/C++ code cannot modify C/C++ variables (Since R2023a)
Ignore assembly code (-ignore-assembly-code)Specify that assembly instructions in C/C++ code cannot modify C/C++ variables (Since R2023a)
-code-behavior-specificationsAssociate behaviors with code elements such as functions
Float rounding mode (-float-rounding-mode)Specify rounding modes to consider when determining the results of floating point arithmetic
Consider volatile qualifier on fields (-consider-volatile-qualifier-on-fields)Assume that volatile qualified structure fields can have all possible values at any point in code

Topics

Related Information