Automatic Orange Tester (-automatic-orange-tester)

(To be removed) Specify that Automatic Orange Tester must be executed after verification

The Automatic Orange Tester will be removed in a future release. See Compatibility Considerations.

Description

This option affects a Code Prover analysis only. Use this option only if you review the Code Prover results in the Polyspace^® desktop products.

Specify that the Automatic Orange Tester must be executed at the end of the verification.

Set Option

User interface (desktop products only): In your project configuration, the option is on the Advanced Settings node. See Dependency for other options you must also enable.

Command line and options file: Use the option -automatic-orange-tester. See Command-Line Information.

Why Use This Option

The Automatic Orange Tester runs dynamic tests on your code. The dynamic tests help you determine if an orange check represents a real run-time error or an imprecision of Polyspace analysis. For a tutorial, see Test Orange Checks for Run-Time Errors (Polyspace Code Prover).

To run the Automatic Orange Tester after verification, you must select this option before verification. During verification, Polyspace generates additional source code to test each orange check for errors. When you run the Automatic Orange Tester later, the software uses this instrumented code for testing.

Settings

On

After verification, when you run the Automatic Orange Tester, Polyspace creates tests for unproven code and runs them.

Off (default)

You cannot launch the Automatic Orange Tester after verification.

Dependency

This option is available only if you set Source code language (-lang) to C or C-CPP.

Tips

• To launch the Automatic Orange Tester, after verification, open your results. Select Tools > Automatic Orange Tester.

• When using the automatic orange tester, you cannot:

  • Select Division round down under Target & Compiler.

  • Select the options c18, tms320c3c. x86_64 or sharc21x61 for Target & Compiler > Target processor type.

  • Specify the type char as 16-bit or short as 8-bit using the option mcpu...(Advanced) for Target & Compiler > Target processor type. For the same option, you must specify the type pointer as 32-bit.

  • Specify global asserts in the code, having the form Pst_Global_Assert(A,B). In global assert mode, you cannot use Constraint setup under Inputs & Stubbing.

  • Select these options related to floating-point verification: Subnormal detection mode and Consider non finite floats.

Command-Line Information

Parameter: -automatic-orange-tester

Default: Off

Example (Code Prover): polyspace-code-prover -sources file_name -lang c -automatic-orange-tester

Compatibility Considerations

Automatic Orange Tester will be removed

Not recommended starting in R2020b

The Automatic Orange Tester will be removed in a future release. In the desktop interface, you set this option in the Configuration pane under the Advanced Settings node.

If you use these command-line options in your scripts, remove them:

• -automatic-orange-tester

• -automatic-orange-tester-loop-max-iteration

• -automatic-orange-tester-tests-number

• -automatic-orange-tester-timeout