Replace assembly with C-model for codeprover

In our embedded software, we have some assembly library (set of .S files, but also inline asm in other .c/h files) to perform mathematical calculations. We know codeprover cannot work with these, so we would like to replace them with C-models. We created a set of C-files that implement those models.

Is there a way to tell codeprover to replace these asm-functions with the C-models in the analysis?

Answer 1

[Matt Rhodes]

Hi Stein-

There are a few options for this. Which of them you use depends on how the code builds and links, as well as whether you are allowed to make any modifications. You might have to use more than one of them at the same time.

1. Just Add It:Since your build just links against some of the other files, and you have headers for the function calls in .h files, you can just add C versions of those functions by adding those files to the list of sources to verify. Without the definitions, the functions get stubbed. When you add them, there is no reason to stub and it will use your C version.
2. Swapping Definitions:For assembly that is wrapped in functions, if they are isolated from the other non-assembly code, you can simply provide a different .c file the C definition during verification, leaving out the version with the assembly definition. In some cases, definitions might be inline in your header file. Hopefully not since this is not the best practice. If this is the case though, you might add an additional -I include path, higher in the priority list, so that the alternate definition is found for the Polyspace verification. If the header file has too much not related to assembly, you probably wont want to switch them. In that case, then one of the next two options could help with this.
3. Conditional Compilation:If you can modify your code, another approach is to add conditional compilation directives. Some people will use a POLYSPACE macro, though I'd caution to use one just for the assembly in case you need to add other, such as POLYSPACE_ASSEMBLY_ALTERNATE or similar. If you can take this approach, many people like that it doubles as a way to further document the intent of the assembly.
4. Post Pre-processor Processing:This option is the least invasive means of providing alternate definitions when you can't modify the source files. Its too much to explain here if you've not used it already, so please refer to the documentation page, Command/script to apply to preprocessed files (-post-preprocessing-command)
5. Support and Application Engineers:Lastly, if you still need help with this, I'd encourage you to reach out to support or ask your account representative to put you in touch with a local Polyspace Application Engineer to help you out.