Code prover wants userdef function for critical section

2 次查看（过去 30 天）
Stein Heselmans
Stein Heselmans 2017-8-30
评论： Stein Heselmans 2017-8-31
From code-prover i get this error:
Stubbing standard library functions ...
Propagating data types... 50%
Propagating data types... 100%
Analyzing data type mismatch... 50%
Analyzing data type mismatch... 100%
Finalizing data type handling
Stubbing unknown functions ...
Error: Verifier found an error in parameter -critical-section: function "fenter_critical" must be a userdef function
Error: Verifier found an error in parameter -critical-section: function "fexit_critical" must be a userdef function
Command option was:
polyspace-code-prover-nodesktop ... -critical-section-begin fenter_critical:cs1 -critical-section-end fexit_critical:cs1 ...
The functions are defined as:
void fenter_critical(void) {}
void fexit_critical(void) {}
How do i solve this error?

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

采纳的回答

Alexandre De Barros
Hello,
can you check if fenter_critical() and fexit_critical() are always declared in every file where they are used? I can reproduce the same message with this code:
//void fenter_critical(void);
//void fexit_critical(void);
void task(void) {
fenter_critical();
fexit_critical();
};
void main() {
}
If the declarations are uncommented, then there is no problem.
--- Alex
  2 个评论
Stein Heselmans
Stein Heselmans 2017-8-31
Thanks for the swift reply. Yes, i am sure they are defined in every file.
We have a _POLYSPACE_ flag that we pass to polyspace-code-prover-nodesktop for polyspace analysis. That flag is never passed to our compiler, so the 'production' build does not pass that flag to gcc.
We have
#if defined(__POLYSPACE__)
#define ENTER_SECTION(TYPE) fenter_critical()
#define EXIT_SECTION() fexit_critical()
#else
#define ENTER_SECTION(TYPE) ...some target specific code (inline asm)...
#define EXIT_SECTION() ...some target specific code (inline asm)...
#endif
and fenter/exit_critical() is only defined when building for _POLYSPACE_
Your answer made me try another thing: passing this _POLYSPACE_ flag to the compiler also for the production build. This made the whole thing work.
Does that mean that all symbols that are used in the polyspace-code-prover-nodesktop command need to be there for the underlying make command as well?
How can we mock our atomic sections for codeprover?
Stein Heselmans
Stein Heselmans 2017-8-31
Forget my previous comment: due to a stupid typo in my Makefile, the _POLYSPACE_ flag wasn't passed on to polyspace-code-prover-nodesktop. Fixed that, and it works like expected.
The symbol-set in the production build and codeprover build don't need to be exactly the same!

请先登录，再进行评论。

更多回答（0 个）

类别

在 Help Center 和 File Exchange 中查找有关 Polyspace Code Prover 的更多信息

标签

产品

Community Treasure Hunt

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

Start Hunting!

Translated by