Azzera filtri
Azzera filtri

Code prover wants userdef function for critical section

8 visualizzazioni (ultimi 30 giorni)
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?

Risposta accettata

Alexandre De Barros
Alexandre De Barros il 30 Ago 2017
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 Commenti
Stein Heselmans
Stein Heselmans il 31 Ago 2017
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 il 31 Ago 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!

Accedi per commentare.

Più risposte (0)

Tag

Community Treasure Hunt

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

Start Hunting!

Translated by