Bug #1069: BLAST goes to local label out instead of global one or vice versa - BLAST - Open-Source Projects

Actions

Copy link

Bug #1069

open

BLAST goes to local label out instead of global one or vice versa

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

Status:

New

Priority:

Normal

Assignee:

Category:

CIL

Target version:

Start date:

04/12/2011

Due date:

% Done:

Estimated time:

Detected in build:

41b2b9632f441a890ed26345cc44d3d8ce6fdd25

Platform:

Published in build:

Description

===
linux-2.6.37 39_7 drivers/bluetooth/hci_uart.ko    ldv_main3_sequence_infinite_withcheck_stateful
(false unsafe:label)
BT_DBG("hu %p", hu);
goto local label out (marked as __label__) misinterprets as leading to global label out
===
linux-2.6.37    39_7 drivers/input/serio/ps2mult.ko    ldv_main0_sequence_infinite_withcheck_stateful
(false unsafe:label)
dev_dbg(&serio->dev, "Received %02x flags %02x\n", data, dfl);
local label out
===
linux-2.6.37    39_7 drivers/net/8139too.ko    ldv_main0_sequence_infinite_withcheck_stateful
(false unsafe:label)
netdev_dbg macro declares local label out
goes to local label out instead of global one
===
linux-2.6.37    39_7 drivers/net/ethoc.ko    ldv_main0_sequence_infinite_withcheck_stateful
(false unsafe:label)
dev_dbg(&dev->dev, "stopping queue\n"); 
goto global out instead of local one

Actions

Copy link

Updated by Evgeny Novikov about 13 years ago

Our C backend may be adjusted to provide unique labels as workaround. Although it will be just a workaround.

Actions

Copy link

Updated by Pavel Shved about 13 years ago

Eugene Novikov wrote:

Our C backend may be adjusted to provide unique labels as workaround. Although it will be just a workaround.

Actually, we might want to name these "workarounds" "simplifications of C code to support more Static Verifiers", and they will become mainstream. :-)

Actions

Copy link