Actions
Bug #1334
openCIL translates local label out into a global one
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:
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.
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