Weak symbols in codeprover

2 次查看（过去 30 天）
Stein Heselmans
Stein Heselmans 2017-8-31
评论： Stein Heselmans 2017-9-6
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_IMPLEMENTATION
void foo(void)
{
}
#endif
So what does codeprover support in order to mark a function as weak, over writable by other implementation.

请先登录，再回答此问题。

采纳的回答

Alexandre De Barros
Hello,
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?
Best regards,
Alexandre
  3 个评论
显示 1更早的评论
Alexandre De Barros
Alexandre De Barros 2017-9-1
A workaround is to make these functions static inside the Polyspace verification.
Hence, multiple definitions will be allowed.
Could you contact the support? They will tell you how to do that.
Best regards,
Alexandre
Stein Heselmans
Stein Heselmans 2017-9-6
I guess those static function would more or less be the same as my proposed workaround (#ifndef NO_FOO_IMPLEMENTATION). I'ld rather go with that

请先登录，再进行评论。

更多回答（0 个）

类别

在 Help Center 和 File Exchange 中查找有关 Get Started with Polyspace Products for Ada 的更多信息

标签

产品

Community Treasure Hunt

Find the treasures in MATLAB Central and discover how the community can help you!

Start Hunting!

Translated by