Project

General

Profile

Actions
Copy link

Bug #930

open

CIL's simeplemem does not respect line numbers

Added by Pavel Shved over 13 years ago. Updated almost 10 years ago.

Status:
New
Priority:
Low
Assignee:
Vadim Mutilin
Category:
CIL
Target version:
-
Start date:
03/11/2011
Due date:
% Done:

0%

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

Description

While the CIL source code demonstrates the obvious effort to keep the line numbers, it just doesn't work. As shown in bug #928, when CIL inserts its "simplemem" additional variables the line numbers are not kept. Here is an excerpt:

                                               Location: id=721#2 src="/home/tester/ldv/workdir/envs/1/work/work-3e1f2356ce231488dc1fa844e5ce91bcb59fc2a1/drivers/media/video/au0828/au0828-video.c/work/current--X--commands.xml--X--defaultshadows--X--32_7/artificial_env_1/csd_deg_dscv/23/dscv_tempdir/dscv/ri/32_7/drivers/media/video/videobuf-core.c"; line=1062
     Block(mem_15@videobuf_read_stream = * (q@videobuf_read_stream ).int_ops;)
                                               Location: id=721#3 src=""; line=-1
     Pred(* (mem_15@videobuf_read_stream ).magic  ==  304484355)
                                               Location: id=721#5 src=""; line=-1
     Block(__cil_tmp25@videobuf_read_stream = 0;)

The first assignment contains a proper line number, while two others do not. ETV, after bug #928 fixes, just doesn't show the line number for them.

CIL should be fixed.

Actions
Copy link
 #1

Updated by Pavel Shved almost 13 years ago

This would require adjusting core CIL "visitor" functionality. Wouldn't touch it now.

Actions
Copy link
 #2

Updated by Pavel Shved almost 13 years ago

  • Project changed from Linux Driver Verification to BLAST
  • Category deleted (BLAST)
Actions
Copy link
 #3

Updated by Vadim Mutilin almost 10 years ago

  • Category set to CIL
  • Assignee changed from Pavel Shved to Vadim Mutilin
Actions
Copy link
 #4

Updated by Mikhail Mandrykin almost 10 years ago

Current development version (bc1cb8e676e71c0adabe04da5d760d2c85f24268) with
--dosimplify --dosimpleMem assigns line numbers in this snippet correctly:

  int d = pf->b[i]; // Line 33


#line 33
  __cil_tmp4 = i * 4UL;
#line 33
  __cil_tmp5 = 4 + __cil_tmp4;
#line 33
  __cil_tmp6 = (unsigned long )pf;
#line 33
  __cil_tmp7 = __cil_tmp6 + __cil_tmp5;
#line 33
  d = *((int *)__cil_tmp7);
Actions
Copy link

Also available in: Atom PDF