We use the gcc attributing in order to mark functions weak in libraries. That way projects including these libraries can overwrite the content of that weak function with custom content.
e.g. usage in a library:
void __attribute__((weak)) foo (void){}
The codeprover (polyspace-code-prover-nodesktop) doesn't seem to understand this attribute, as it is gcc specific implementation.
Does codeprover provide some alternative syntax for this?
I can see a valid alternative, but that would be quiet intrusive for our libraries:
#ifndef NO_FOO_IMPLEMENTATIONvoid foo(void){}#endif
So what does codeprover support in order to mark a function as weak, over writable by other implementation.
Best Answer