• '_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 NOT include a call edge from 'updatewindow' to 'zcalloc' in backbone, because tainted data cannot flow along the edge

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

UNSAT (False Alarm)

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

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

UNSAT (False Alarm)

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

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

UNSAT (False Alarm)

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

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

UNSAT (False Alarm)

Path should visit 'png_set_IHDR', to define a necessary variable used in the sink

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

'readpng_get_image' cannot return from 'png_read_end' and then call alloc(), since 'readpng_get_image' always calls alloc() before calling 'png_read_end'

Found Bug (True Alarm)

Path should visit 'png_set_IHDR', to define a necessary variable used in the sink

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

'readpng_get_image' cannot return from 'png_read_end' and then call alloc(), since 'readpng_get_image' always calls alloc() before calling 'png_read_end'

Path should NOT include a return-call sequence of 'readpng_init'--(R)-->'main'--(C)-->'readpng_get_image' in backbone, because there is a sanitization logic along the nodes

'main' cannot return from 'readpng_get_image' and then call 'readpng_get_image', since 'main' calls 'readpng_get_image' only once

UNSAT (False Alarm)

Path should visit 'png_set_IHDR', to define a necessary variable used in the sink

Found Bug (True Alarm)

Path should visit 'png_set_IHDR', to define a necessary variable used in the sink

Found Bug (True Alarm)

Path should visit 'png_set_IHDR', to define a necessary variable used in the sink

Found Bug (True Alarm)

Path should visit 'png_set_IHDR', to define a necessary variable used in the sink

Found Bug (True Alarm)

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

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

UNSAT (False Alarm)

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

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

UNSAT (False Alarm)