Is there a possibility to make replacements in preprocessor directives in Polyspace Code Prover R2019b?

I have a question concerning Macro definitions:

Is it possible to overwrite a special value which is defined by macro in order to have another verification behavior?

In the example below I want to manipulate CONSTANT_A and set it to 0 although it is set to 2 in the code. My goal is to force the verification to analyze also the else-path without touching the code.

#include <stdio.h>
#define CONSTANT_A (2)

#if (CONSTANT_A != 0)
#define MY_MACRO(_var) {_var = 0;}
#else 
#define MY_MACRO(_var) {_var = 1;}
#endif

int main(void)
{
int a = 10; 
int b = 20;
int res = a + b; 
MY_MACRO(res); 
return 0; 
}

Is there a possibility?

Answer 1

[MathWorks Support Team]

To change a MACRO within the C file before preprocessing, you can write files with corresponding regular expressions and specify them as described here:

https://www.mathworks.com/help/bugfinder/ref/regexreplacergxregexreplacefmt.html

The specified files (match.rxt and replace.txt) must be specified with their absolute paths.

The option itself is then entered in the configuration under "Other" in the Advanced Settings, in the form:

-regex-replace-rgx <path-to>\match.txt -regex-replace-fmt <path-to>\replace.txt

If you need more information about regular expressions, you can also refer to the MATLAB documentation here:

https://www.mathworks.com/help/matlab/matlab_prog/regular-expressions.html