polyspace code prover: cosmic compiler issue

Hello All,

Polyspace does not recognize the "if" construct for cosmic compiler. Is there a workaround for this issue?

Error: this operator is not allowed in a preprocessing expression

# if (__XGATE_CHECK_VAR__ == 'X')

^

Code:

# if defined( MAKE_DEPEND )

/* The GNU compiler does not understand the following if-directive => make the dependency generator work... */

# else

# define __XGATE_CHECK_VAR__ __TRGT__[0]

# if (__XGATE_CHECK_VAR__ == 'X')

# else

# define V_MEMRAM1_FAR @gpage /* MCS12x part */

# if (V_COMPVERSION >= 407)

# define V_MEMRAM3_FAR @far /* MCS12x part */

# else

# define V_MEMRAM3_FAR /* MCS12x part */

# endif

# endif

# endif

#endif

Answer 1

[Anirban]

Hi,

It is not the #if per se, but the [0] of __TRGT__[0] that is causing the problem. Following the standard, Polyspace does not support evaluations of expressions in preprocessor directives. Some compilers allow this but it is not supported in Polyspace yet.

There are several noninvasive ways to work around the issue, but all of them involving effectively replacing __TRGT__[0] with something else for the purposes of the analysis:

• Assuming this code occurs in a header, you can make a copy of the header and replace the __TRGT__[0] with something else (depending on whether you want the #if or #else branch to be analyzed). You can place the copy in a separate folder and provide this folder as the first include folder in the project. This would cause the copy of the header to override the actual header during the analysis.
• You can use the options -regex-replace-rgx and -regex-replace-fmt to make the replacement without modifying the actual source code.

Answer 2

[Karpakam Subramanian]

Hello Anirban,

Thank you for the suggestion. Will try the solution provided , thanks.