Project

General

Profile

Bug #9340

Use LDV functions for allocating memory

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

Status:
Closed
Priority:
Urgent
Assignee:
Category:
Environment model
Target version:
Start date:
10/19/2018
Due date:
% Done:

0%

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

Description

In Klever 2.0 EMG puts generated models into separate C files that are not instrumented. Because of this, say, when models use kzalloc, this function definition calls kmalloc with a special flag for zeroing memory that is not known by verification backends. The particular example is the alloc_etherdev_mqs model, but likely there are other ones.

History

#1

Updated by Ilja Zakharov 8 months ago

  • Status changed from New to Resolved

This is a single case. I do not observe any other incorrect functions anymore. Fixed in klever-2.0.

#2

Updated by Evgeny Novikov 8 months ago

  • Status changed from Resolved to Closed

Branch klever-2.0 passed all tests and I merged it to master in 72be796e3 marked as v2.0rc1.

Also available in: Atom PDF