Project

General

Profile

Bug #10127

Declare ldv_inline_asm() before usage

Added by Evgeny Novikov 3 months ago. Updated 3 months ago.

Status:
Closed
Priority:
Urgent
Category:
Environment model
Target version:
Start date:
02/20/2020
Due date:
% Done:

0%

Estimated time:
Detected in build:
svn
Platform:
Published in build:

Description

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.

History

#1

Updated by Evgeny Novikov 3 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.

#2

Updated by Evgeny Novikov 3 months ago

  • Status changed from Resolved to Closed

Tests passed, so, I merged the branch to master in f31697a4b.

Also available in: Atom PDF