IAR Embedded Workbench Compiler (-compiler iar-ew)

To override the macro definition, use the option Preprocessor definitions (-D).

To undefine a macro, use the option Disabled preprocessor definitions (-U).

Polyspace does not support the use of $Super$$ and $Sub$$ to patch symbol definitions. For instance, the following code compiles correctly, but Polyspace considers that main() calls the extern func ($Super$$func) instead of the function func defined in this code ($Sub$$func):

/* void func() declared in another file */
extern void $Super$$func(int i);

int setup = 0;

void setup_func(int i) {
  setup = i;
}

/* this function should be called instead of the original extern func() */
void $Sub$$func(int i) {
  setup_foo(i); 
  /* does some extra setup work */   
  /* ... */
}

int main() {
  assert(setup = 0);
  func(1); // Should call $Sub$$func instead of $Super$$func
  assert(setup = 1);
  return 0;
}

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

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

If you use Polyspace as You Code extensions in IDEs, enter this option in an analysis options file. See options file.