• '_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 a call edge from 'nonfatal' to 'dupvprintf' either in backbone or branch, for the correct taint propagation toward the sink

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

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

Path should include a call edge from 'nonfatal' to 'dupvprintf' either in backbone or branch, for the correct taint propagation toward the sink

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

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

Path should include a call edge from 'nonfatal' to 'dupvprintf' either in backbone or branch, for the correct taint propagation toward the sink

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

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

Path should include a call edge from 'nonfatal' to 'dupvprintf' either in backbone or branch, for the correct taint propagation toward the sink

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

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

Path should include a call edge from 'nonfatal' to 'dupvprintf' either in backbone or branch, for the correct taint propagation toward the sink

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

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

Path should include a call edge from 'nonfatal' to 'dupvprintf' either in backbone or branch, for the correct taint propagation toward the sink

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

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

Path should include a call edge from 'nonfatal' to 'dupvprintf' either in backbone or branch, for the correct taint propagation toward the sink

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

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

Path should include a call edge from 'nonfatal' to 'dupvprintf' either in backbone or branch, for the correct taint propagation toward the sink

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

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

Path should include a call edge from 'nonfatal' to 'dupvprintf' either in backbone or branch, for the correct taint propagation toward the sink

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

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

Path should include a call edge from 'nonfatal' to 'dupvprintf' either in backbone or branch, for the correct taint propagation toward the sink

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

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

Path should include a call edge from 'nonfatal' to 'dupvprintf' either in backbone or branch, for the correct taint propagation toward the sink

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

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

Path should include a call edge from 'nonfatal' to 'dupvprintf' either in backbone or branch, for the correct taint propagation toward the sink

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

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

Path should include a call edge from 'nonfatal' to 'dupvprintf' either in backbone or branch, for the correct taint propagation toward the sink

Path should include a call edge from 'nonfatal' to 'dupvprintf' either in backbone or branch, for the correct taint propagation toward the sink

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

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

Path should include a call edge from 'nonfatal' to 'dupvprintf' either in backbone or branch, for the correct taint propagation toward the sink

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

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

Path should include a call edge from 'nonfatal' to 'dupvprintf' either in backbone or branch, for the correct taint propagation toward the sink

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

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

Path should include a call edge from 'nonfatal' to 'dupvprintf' either in backbone or branch, for the correct taint propagation toward the sink

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

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