Options at Command Line Only

Descriptions of options available only at command line

An option on the command line corresponds directly to an option on the Configuration pane in the user interface. The options below are exceptions to this rule. The basic options correspond to menu items and fields elsewhere in the user interface. The advanced options do not appear in the user interface. On the Configuration pane, you have to specify the command-line form of these options in the field Other.

Analysis Options

expand all

-authorSpecify project author
-dateSpecify date of analysis
-doc | -documentationDisplay Polyspace documentation in help browser
-generate-launching-script-forExtract information from project file
-h | -helpDisplay list of possible options
-ISpecify include folder for compilation
-import-commentsImport review information from previous analysis
-list-all-valuesDisplay valid option arguments for a given command-line option
-options-fileRun Polyspace using list of options
-progSpecify name of project
-report-output-nameSpecify name of report
-results-dirSpecify the results folder
-schedulerSpecify cluster or job scheduler
-sourcesSpecify source files
-sources-list-fileSpecify file containing list of sources
-verif-versionAssign a version identifier
-v | -versionDisplay Polyspace version number
-asm-begin -asm-endExclude compiler-specific asm functions from analysis
-code-behavior-specificationsMap imprecisely analyzed function to standard function for precise analysis
-consider-external-array-access-unsafeRemove the default assumption that external arrays of unspecified size can be safely accessed at any index
-custom-targetCreate a custom target processor with specific data type sizes
-dump-preprocessing-infoShow all macros implicitly defined during a particular analysis
-max-processesSpecify maximum number of processors for analysis
-no-assumption-on-absolute-addressesRemove assumption that absolute address usage is valid
-non-preemptable-tasksSpecify functions that represent nonpreemptable tasks
-options-for-sourcesSpecify analysis options specific to a source file
-preemptable-interruptsSpecify functions that represent preemptable interrupts
-regex-replace-rgx -regex-replace-fmtMake replacements in preprocessor directives
-show-similar-overflowsShow all overflows in wrap-around mode
-submit-job-from-previous-compilation-resultsSpecify that the analysis job must be resubmitted without recompilation
-tmp-dir-in-results-dirKeep temporary files in results folder
-xml-annotations-descriptionApply custom code annotations to Polyspace analysis results

Polyspace Code Prover Documentation

Support