Project

General

Profile

Actions

Bug #1236

open

Finding model functions by ldv_ prefix

Added by Alexey Khoroshilov about 13 years ago. Updated about 13 years ago.

Status:
Open
Priority:
Normal
Category:
Infrastructure
Start date:
05/19/2011
Due date:
% Done:

0%

Estimated time:
Detected in build:
3a5698a
Platform:
Published in build:

Description

Model functions in 68_1 do not have ldv_ prefix. As a result, -fdepth may work incorrectly.


Related issues 1 (1 open0 closed)

Related to Linux Driver Verification - Feature #1306: Implement -fdepth option in the more intellectual wayOpenPavel Shved06/01/201108/18/2011

Actions
Actions #1

Updated by Vadim Mutilin about 13 years ago

  • Status changed from New to Feedback

The upper level model functions can't have ldv_ prefix because they are linked (without asectator) and should have the same name. There are no other functions in the model except nondeterministic ones which already have ldv_ prefix.

Actions #2

Updated by Pavel Shved about 13 years ago

  • Category set to Rules and Models
  • Priority changed from High to Normal

If only the upper level functions don't have this prefix, it's OK then (and it looks just as if fdepth had one less level).

Actually, I think of trying to reimplement fdepth for it to only constrain function calls which do not contain error location somewhere in their call graph.

Actions #3

Updated by Alexey Khoroshilov about 13 years ago

  • Status changed from Feedback to New
  • Priority changed from Normal to High

Вадим Мутилин wrote:

The upper level model functions can't have ldv_ prefix because they are linked (without aspectator) and should have the same name.

But what is about macrodefinitions?

Actions #4

Updated by Vadim Mutilin about 13 years ago

Macrodefinitions are not visible for BLAST

Actions #5

Updated by Alexey Khoroshilov about 13 years ago

Some time ago we stated that non-aspectator rule instrumentor is as capable as plain C macrosubstitution. But macrosubstitution is not available in current implementation of non-aspectator rule instrumentor, is it?

Actions #6

Updated by Vadim Mutilin about 13 years ago

  • Status changed from New to Feedback

Alexey, I didn't understand the question. It is not clear what do you mean by macrosubstitution. With non-aspect models we may freely use macro inside the model code, but can not connect (weave) model to the macro defined in the kernel headers.

Actions #7

Updated by Alexey Khoroshilov about 13 years ago

  • Status changed from Feedback to New

Вадим Мутилин wrote:

Alexey, I didn't understand the question. It is not clear what do you mean by macrosubstitution. With non-aspect models we may freely use macro inside the model code, but can not connect (weave) model to the macro defined in the kernel headers.

I wonder why we cannot define a macro
#define usb_put_urb ldv_usb_put_urb
and have the upper level model functions with ldv_ prefix. Is it possible in non-aspect models now?

Actions #8

Updated by Evgeny Novikov about 13 years ago

I guess that we may do this but as Pavel said it's better to forget about this (and moreover do not touch all models and nevertheless obtain not reliable results) by means of more complex analysis may be with some help of aspectator.

Actions #9

Updated by Alexey Khoroshilov about 13 years ago

That is a possible way but there is another aspect that we should keep in mind:
in current state of error trace visualizer Ctrl+F on ldv_ is an important instrument of error trace analysis (at least for me).

Actions #10

Updated by Pavel Shved about 13 years ago

Alexey Khoroshilov wrote:

That is a possible way but there is another aspect that we should keep in mind:
in current state of error trace visualizer Ctrl+F on ldv_ is an important instrument of error trace analysis (at least for me).

Doesn't ETV automatically expand all the model functions we instrument there?

Actions #11

Updated by Alexey Khoroshilov about 13 years ago

Pavel Shved wrote:

Doesn't ETV automatically expand all the model functions we instrument there?

ETV expands down to model functions and highlight them a little bit, but Ctrl+F is still more convenient tool then manual scrolling&looking on long list of error trace elements.

May be an optional button for highhighligting model functions can help to mitigate it.

Actions #12

Updated by Pavel Shved about 13 years ago

Alexey Khoroshilov wrote:

ETV expands down to model functions and highlight them a little bit, but Ctrl+F is still more convenient tool then manual scrolling&looking on long list of error trace elements.

May be an optional button for highhighligting model functions can help to mitigate it.

Maybe simply more highlighted model functions would go? With a different background color, for instance?

Actions #13

Updated by Alexey Khoroshilov about 13 years ago

Pavel Shved wrote:

Maybe simply more highlighted model functions would go? With a different background color, for instance?

Maybe, but if we more highlight all the interesting elements it would not help. So I would prefer to highlight it by user request only.

Actions #14

Updated by Vadim Mutilin about 13 years ago

Alexey Khoroshilov wrote:

Вадим Мутилин wrote:

Alexey, I didn't understand the question. It is not clear what do you mean by macrosubstitution. With non-aspect models we may freely use macro inside the model code, but can not connect (weave) model to the macro defined in the kernel headers.

I wonder why we cannot define a macro
#define usb_put_urb ldv_usb_put_urb
and have the upper level model functions with ldv_ prefix. Is it possible in non-aspect models now?

It is NOT possible!

Actions #15

Updated by Vadim Mutilin about 13 years ago

  • Subject changed from 68_1: model functions do not have ldv_ prefix to Finding model functions by ldv_ prefix
Actions #16

Updated by Vadim Mutilin about 13 years ago

I changed the topic because it not related to following discussion

Actions #17

Updated by Evgeny Novikov about 13 years ago

  • Category changed from Rules and Models to Infrastructure
  • Status changed from New to Open
  • Assignee set to Evgeny Novikov
  • Priority changed from High to Normal

After all we decided to highlight model functions in error trace in the more visible way.

Actions

Also available in: Atom PDF