Code Prover Verification

Verify whole application or module

To specify whether you are verifying a complete application with a main function or a module without a main function, use the Code Prover verification options. If you are verifying a module, the software generates a main function for you. To fine-tune the generated main function, use these options.

Polyspace Options

expand all

Verify whole applicationStop verification if sources files are incomplete and do not contain a main function
Show global variable sharing and usage only (-shared-variables-mode)Compute global variable sharing and usage without running full analysis
Verify initialization section of code only (-init-only-mode)Check initialization code alone for run-time errors and other issues
Verify module or library (-main-generator)Generate a main function if source files are modules or libraries that do not contain a main
Variables to initialize (-main-generator-writes-variables)Specify global variables that you want the generated main to initialize
Initialization functions (-functions-called-before-main)Specify functions that you want the generated main to call ahead of other functions
Functions to call (-main-generator-calls)Specify functions that you want the generated main to call after the initialization functions
Verify files independently (-unit-by-unit)Option to verify each source file independently of other source files
Common source files (-unit-by-unit-common-source)Specify files that you want to include with each source file during a file by file verification
Main entry point (-main)Specify a Microsoft Visual C++ extensions of main
Analyze class contents only (-class-only)Do not analyze code other than class methods
Skip member initialization check (-no-constructors-init-check)Do not check if class constructor initializes class members
Functions to call within the specified classes (-class-analyzer-calls)Specify class methods that you want to verify
Class (-class-analyzer)Specify classes that you want to verify
Verify model generated code (-main-generator)Specify that a main function must be generated if it is not present in source files
Parameters (-variables-written-before-loop)Specify variables that the generated main must initialize before the cyclic code loop
Inputs (-variables-written-in-loop)Specify variables that the generated main must initialize in the cyclic code loop
Initialization functions (-functions-called-before-loop)Specify functions that the generated main must call before the cyclic code loop
Step functions (-functions-called-in-loop)Specify functions that the generated main must call in the cyclic code loop
Termination functions (-functions-called-after-loop)Specify functions that the generated main must call after the cyclic code loop

Topics