Project

General

Profile

Actions
Copy link

Bug #10127

closed

Declare ldv_inline_asm() before usage

Added by Evgeny Novikov about 4 years ago. Updated about 4 years ago.

Status:
Closed
Priority:
Urgent
Assignee:
Evgeny Novikov
Category:
Environment models
Target version:
3.0
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.

Actions
Copy link
 #1

Updated by Evgeny Novikov about 4 years 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.

Actions
Copy link
 #2

Updated by Evgeny Novikov about 4 years ago

  • Status changed from Resolved to Closed

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

Actions
Copy link

Also available in: Atom PDF