Project

General

Profile

Actions

Bug #7935

closed

Remove more auxiliary functions properly

Added by Vadim Mutilin about 7 years ago. Updated about 7 years ago.

Status:
Closed
Priority:
Immediate
Category:
Tasks generation
Target version:
-
Start date:
02/01/2017
Due date:
% Done:

0%

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

Actions #1

Updated by Evgeny Novikov about 7 years ago

  • Category set to Tasks generation
  • Assignee set to Evgeny Novikov
Actions #2

Updated by Evgeny Novikov about 7 years ago

  • Subject changed from Couldn't visualize the error trace (linux:alloc, drivers/video/fb.ko) to Remove more auxiliary functions properly
  • Description updated (diff)
  • Status changed from New to Closed

It turned out that new code for removing auxiliary functions had too strong conditions and skipped removing seldom, in the specified example this is when functions wrapped with auxiliary ones contain calls to other functions when returning (http://lxr.free-electrons.com/source/drivers/video/fbmem.c?v=3.14#L1226). Then old code removed remaining auxiliary functions but made that bad that eventually caused troubles during visualization.

I fixed this in 681261a to master. Corresponding verification results are here: http://ldvstore:8998/jobs/65/. You can see that all marks from the latest results were successfully applied. In addition now one can see that the error trace which visualization was broken before now can be successfully visualized and even was associated with a mark created before. I assume that there not so good witnesses were produced by CPAchecker in general so there wasn't this issue.

Actions #3

Updated by Vadim Mutilin about 7 years ago

Trace looks OK to me.
Rule comments are misleading, but it is another issue #7948

Actions

Also available in: Atom PDF