Declare ldv_inline_asm() before usage
Since verifiers do not interpret Inline Assembler Klever replaces it with calls to stub function ldv_inline_asm(). But it does not care about this function is declared before usage that can result in tricky conflicts on merging source files together.
Updated by Evgeny Novikov 11 months ago
- Status changed from New to Resolved
I fixed the issue in branch fix-ldv-inline-asm-decl. From now there is a special header presets/jobs/specifications/ldv/common.h that is added at the beginning of all instrumented C source files including models. The branch is tested.