Code prover wants userdef function for critical section

Question

Stein Heselmans 2017-8-30

0
链接

此问题的直接链接

https://ww2.mathworks.cn/matlabcentral/answers/354574-code-prover-wants-userdef-function-for-critical-section

评论： 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?

0 个评论
显示 -2更早的评论隐藏 -2更早的评论

请先登录，再进行评论。

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

Answer 1

Alexandre De Barros 2017-8-30

0
链接

此回答的直接链接

https://ww2.mathworks.cn/matlabcentral/answers/354574-code-prover-wants-userdef-function-for-critical-section#answer_279721

在 MATLAB Online 中打开

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 2017-8-31

在 MATLAB Online 中打开

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 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!

请先登录，再进行评论。