Project

General

Profile

Actions

Bug #1334

open

CIL translates local label out into a global one

Added by Vadim Mutilin over 13 years ago. Updated about 10 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 #1

Updated by Evgeny Novikov over 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 #2

Updated by Vadim Mutilin about 10 years ago

  • Category set to CIL
Actions #3

Updated by Mikhail Mandrykin about 10 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

Also available in: Atom PDF