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:
Actions