Code prover wants userdef function for critical section

2 views (last 30 days)
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?

Accepted Answer

Alexandre De Barros
Alexandre De Barros on 30 Aug 2017
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) {
void main() {
If the declarations are uncommented, then there is no problem.
--- Alex
Stein Heselmans
Stein Heselmans on 31 Aug 2017
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!

Sign in to comment.

More Answers (0)

Community Treasure Hunt

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

Start Hunting!

Translated by