Project

General

Profile

Actions

Bug #9340

closed

Use LDV functions for allocating memory

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

Status:
Closed
Priority:
Urgent
Assignee:
Category:
Environment models
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.

Actions #1

Updated by Ilja Zakharov over 5 years 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.

Actions #2

Updated by Evgeny Novikov over 5 years 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.

Actions

Also available in: Atom PDF