Project

General

Profile

Actions
Copy link

Bug #1334

open

CIL translates local label out into a global one

Added by Vadim Mutilin almost 13 years ago. Updated over 9 years ago.

Status:
New
Priority:
Normal
Assignee:
-
Category:
CIL
Start date:
06/08/2011
Due date:
% Done:

0%

Estimated time:
Detected in build:
657406aad
Platform:
Published in build:

Description

The example of a construction in driver drivers/input/misc/cm109.ko

 do { do { __label__ do_printk; __label__ out; static struct _ddebug descriptor __attribute__((__used__)) __attribute__((section("__verbose"), aligned(8))) = { "cm109", __func__, "/work/experiments/test_cpachecker/work/current--X--drivers/input/misc/cm109.ko--X--defaultlinux-2.6.37--X--32_1--X--cpachecker/linux-2.6.37/csd_deg_dscv/11/dscv_tempdir/dscv/ri/32_1/drivers/input/misc/cm109.c.common.c", "### URB IRQ: [0x%02x 0x%02x 0x%02x 0x%02x] keybit=0x%02x\n", 348, 0 }; do { if (__builtin_expect(!!(*&descriptor.enabled), 0)) goto do_printk; } while (0); goto out; do_printk: dev_printk("<7>", &urb->dev->dev, "### URB IRQ: [0x%02x 0x%02x 0x%02x 0x%02x] keybit=0x%02x\n", dev->irq_data->byte[0], dev->irq_data->byte[1], dev->irq_data->byte[2], dev->irq_data->byte[3], dev->keybit); out: ; } while (0); } while (0);

CPAchecker fails with 

Duplicate label out in function cm109_urb_irq_callback in line 6374: out:

Actions
Copy link
 #1

Updated by Evgeny Novikov almost 10 years ago

Proper place for CIL related bugs is its bugzilla, since we will unlikely fix them by ourselves. So reopen this issue there and mark this here.

Actions
Copy link
 #2

Updated by Vadim Mutilin over 9 years ago

  • Category set to CIL
Actions
Copy link
 #3

Updated by Mikhail Mandrykin over 9 years ago

Current CIL (bc1cb8e676e71c0adabe04da5d760d2c85f24268) correctly renames local labels and transforms

do { do {
  __label__ do_printk;
  __label__ out;
  do { if (b) goto do_printk; } while (0); goto out; do_printk: goto out; out: ; } while (0); } while (0);
out:
 return 1;

into 
  while (1) {
    while (1) {
      while (1) {
        if (b) {
          goto do_printk___0;
        }
        break;
      }
      goto out___0;
      do_printk___0:
      goto out___0;
      out___0: ;
      break;
    }
    break;
  }
  out:

Actions
Copy link

Also available in: Atom PDF