Fix Polyspace Compilation Errors Related to TASKING Compiler

If you choose tasking for the option Compilation toolchain (Static analysis), you can encounter this issue.

Issue

During Polyspace^® analysis, you see an error related to an extension specific to the Tasking compiler, for instance, the Special Function Register data type.

Solution

Enable Support for SFR Types

When compiling with the TASKING compiler, you typically use the following compiler flags to specify where Special Function Register (SFR) data types are declared:

--cpu=xxx: The compiler implicitly #includes the file sfr/regxxx.sfr in your source files. Once #include-ed, you can use Special Function Registers (SFR-s) declared in that .sfr file.
--alternative-sfr-file: The compiler uses an alternative SFR file instead of the regular SFR file. You can use Special Function Registers (SFR-s) declared in that alternative SFR file.

If you specify the TASKING compiler for your Polyspace analysis, the analysis makes the following assumptions about these compiler flags:

--cpu=xxx: The analysis chooses a specific value of xxx. If you use a different value with your TASKING compiler, you can encounter an error during Polyspace analysis.
The xxx value that the Polyspace analysis uses depends on your choice of Target processor type (-target):
- tricore: tc1793b
- c166: xc167ci
- rh850: r7f701603
- arm: ARMv7M
--alternative-sfr-file: The analysis assumes that you do not use an alternative SFR file. If you use one, you can encounter an error.

Use the command-line option -compiler-parameter in your Polyspace analysis as follows. You use this command-line option to make Polyspace aware of your compiler flags. In the user interface, you can enter the command-line option in the field Other. You can enter the option multiple times.

--cpu=xxx: For your Polyspace analysis, use
```
-compiler-parameter --cpu=xxx
```
Here, xxx is the value that you use when compiling with your compiler.
--alternative-sfr-file: For your Polyspace analysis, use
```
-compiler-parameter --alternative-sfr-file
```
If you still encounter an error because Polyspace is not able to locate your .asfr file, explicitly #include your .asfr file in the preprocessed code using the option Include (-include).
Typically, the path to the file is Tasking_C166_INSTALL_DIR\include\sfr\regCPUNAME.asfr. For instance, if your TASKING compiler is installed in C:\Program Files\Tasking\C166-VX_v4.0r1\ and you use the CPU-related flag -Cxc2287m_104f or --cpu=xc2287m_104f, the path is C:\Program Files\Tasking\C166-VX_v4.0r1\include\sfr\regxc2287m.asfr.
You can also encounter the same issue with alternative sfr files when you trace your build command. For more information, see Requirements for Polyspace Project Creation from Build Systems.

Enable Support for CPU-s Other Than TC1793

If you choose tasking for the option Compilation toolchain (Static analysis), the CPU used is TC1793. If you use a different CPU, set the following analysis options in your project:

Disabled preprocessor definitions (-U): Undefine the macro __CPU_TC1793B__.
Preprocessor definitions (-D): Define the macro __CPU__. Enter __CPU__=xxx, where xxx is the name of your CPU.
Additionally, define the equivalent of the macro __CPU_TC1793B__ for your CPU. For instance, enter __CPU_TC1793A__.

Instead of manually specifying your compiler, if you trace your build command (makefile), Polyspace can detect your CPU and add the required definitions in your project.

Avoid Unsupported Constructs

Polyspace does not support some constructs specific to the TASKING compiler.

For the list of unsupported constructs, see codeprover_limitations.pdf in polyspaceroot\polyspace\verifier\code_prover_desktop. Here, polyspaceroot is the Polyspace installation folder, for instance, C:\Program Files\Polyspace\R2019a.