• '_prologue_' is an imaginary function that initialize argc, argv
  
• Solid arrow means call edge
  
• Dotted arrow means return edge
  
• Green arrow means branch (pair of call & return)
  
For details, see II-A.'Backbone-Branch Decomposition' section of our paper

Path should include one of the following edges :
(1) Call edge from scsi_match to idmessage
(2) Call edge from verify_SG_version to idmessage,
for the correct taint propagation to the sink

If path includes a call edge from 'verify_SG_version' to 'idmessage' either in backbone or branch, then path should NOT have an incoming edge to 'verify_SG_version', for the correct taint propagation to the sink

If path includes a call edge from 'scsi_match' to 'idmessage' either in backbone or branch, then path should NOT have an incoming edge to 'scsi_match', for the correct taint propagation to the sink

Path should include one of the following edges :
(1) Call edge from scsi_match to idmessage
(2) Call edge from verify_SG_version to idmessage,
for the correct taint propagation to the sink

If path includes a call edge from 'verify_SG_version' to 'idmessage' either in backbone or branch, then path should NOT have an incoming edge to 'verify_SG_version', for the correct taint propagation to the sink

If path includes a call edge from 'scsi_match' to 'idmessage' either in backbone or branch, then path should NOT have an incoming edge to 'scsi_match', for the correct taint propagation to the sink

Path should include one of the following edges :
(1) Call edge from scsi_match to idmessage
(2) Call edge from verify_SG_version to idmessage,
for the correct taint propagation to the sink

If path includes a call edge from 'verify_SG_version' to 'idmessage' either in backbone or branch, then path should NOT have an incoming edge to 'verify_SG_version', for the correct taint propagation to the sink

If path includes a call edge from 'scsi_match' to 'idmessage' either in backbone or branch, then path should NOT have an incoming edge to 'scsi_match', for the correct taint propagation to the sink

Path should NOT have an incoming edge to 'idperror', because tainted data cannot flow through the node

Path should NOT have an incoming edge to 'idperror', because tainted data cannot flow through the node

Path should NOT have an incoming edge to 'idperror', because tainted data cannot flow through the node

Path should NOT have an incoming edge to 'callback', because tainted data cannot flow through the node

Path should NOT have an incoming edge to 'callback', because tainted data cannot flow through the node

Path should NOT have an incoming edge to 'callback', because tainted data cannot flow through the node