Weak symbols in codeprover
8 visualizzazioni (ultimi 30 giorni)
Stein Heselmans il 31 Ago 2017
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:
So what does codeprover support in order to mark a function as weak, over writable by other implementation.
Alexandre De Barros il 31 Ago 2017
when you write "The codeprover doesn't seem to understand this attribute", do you mean that you have a compilation error?
If yes, I can't reproduce it when selecting "gnu4.6" as the "compiler" in Polyspace (version R2017a).
What version of Polyspace do you use, and what is the value associated to the -compiler option?
Più risposte (0)
Code Verification Polyspace Bug Finder Configure and Run Analysis Complete List of Polyspace Bug Finder Analysis Engine Options Command-Line Only Options