Project

General

Profile

Actions

Feature #9539

closed

Print stub for inline Assembler

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

Status:
Closed
Priority:
Urgent
Category:
C back-end
Start date:
03/13/2019
Due date:
% Done:

0%

Estimated time:
Published in build:

Description

Inline Assembler is not interpreted by source code analysis & verification tools. Moreover, it can confuse them, e.g. CPAchecker doesn't support asm goto. So, it is better to print some stub instead of inline Assembler. For a start let's call undefined function void ldv_inline_asm(void).


Related issues 1 (0 open1 closed)

Blocks Klever - Feature #9536: Update CIFClosedEvgeny Novikov03/13/2019

Actions
Actions #1

Updated by Evgeny Novikov about 5 years ago

Actions #2

Updated by Evgeny Novikov about 5 years ago

  • Status changed from New to Closed

I supported this in 355e76d. After that we do not need source code patches either before or after Frama-C (CIL)!

Actions

Also available in: Atom PDF