• '_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 'CmdKeywords' to 'fprintRTF' either in backbone or branch, for the correct taint propagation toward the sink

Path should NOT have an outgoing edge from 'print_usage', because tainted data cannot flow through the node

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

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

Path should NOT have an outgoing edge from 'open_path', because tainted data cannot flow through the node

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

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

Path should NOT have an outgoing return edge from 'open_cfg', because tainted data cannot flow through the node

Path should NOT have an outgoing edge from 'diagnostics', because tainted data cannot flow through the node

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

Path should NOT have an outgoing edge from 'getTmpPath', because tainted data cannot flow through the node

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

Path should NOT include a return edge from 'my_fgetc' to 'ScanBbl' in backbone, because tainted data cannot flow along the edge

Path should NOT include a return edge from 'my_fgets' to 'ScanBbl' in backbone, because tainted data cannot flow along the edge

Path should NOT include a return edge from 'my_fgets' to 'FilterAuxFile' in backbone, because tainted data cannot flow along the edge

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

Path should NOT have an outgoing edge from 'PutJpegFile', because tainted data cannot flow through the node

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

Path should NOT include a call edge from 'PutHexFile' to 'fprintRTF' in backbone, because tainted data cannot flow along the edge

Path should NOT have an outgoing return edge from 'PutHexFile', because tainted data cannot flow through the node

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

Path should include a return edge from 'getBraceParam' to 'CmdKeywords' either in backbone or branch, for the correct taint propagation toward the sink

Path should include a return edge from 'getBraceParam0' to 'getBraceParam' either in backbone or branch, for the correct taint propagation toward the sink

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

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

Path should include a return edge from 'getBraceParam' to 'CmdKeywords' either in backbone or branch, for the correct taint propagation toward the sink