Code prover wants userdef function for critical section

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?

Answer 1

[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

[Stein Heselmans]

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]

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!