• '_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 call edges 'png_read_end'--->'png_handle_unknown'--->'read_chunk_callback' in backbone, because there is a sanitization logic along the nodes

Path should NOT include call edges 'png_read_info'--->'png_handle_unknown'--->'read_chunk_callback' in backbone, because there is a sanitization logic along the nodes

Path should have an incoming call edge to 'png_handle_unknown', to define a necessary variable used in the sink

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

'rwpng_read_image24_libpng' cannot return from 'png_read_end' and then call 'rwpng_create_row_pointers', since 'rwpng_read_image24_libpng' always calls 'rwpng_create_row_pointers' before calling 'png_read_end'

Path should NOT include a call edge from 'rwpng_read_image24_libpng' to 'rwpng_create_row_pointers' in backbone, because there is a sanitization logic along the nodes

Path should NOT include a return-call sequence of 'rwpng_read_image24_libpng'--(R)-->'rwpng_read_image24'--(R)-->'read_image'--(R)-->'pngquant_file'--(C)-->'write_image'--(C)-->'rwpng_write_image24'--(C)-->'rwpng_create_row_pointers' in backbone, because there is a sanitization logic along the nodes

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

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

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

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

Path should NOT include a call edge from 'deflateInit2_' 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

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

UNSAT (False Alarm)

Path should NOT include call edges 'png_read_end'--->'png_handle_unknown'--->'read_chunk_callback' in backbone, because there is a sanitization logic along the nodes

Path should NOT include call edges 'png_read_info'--->'png_handle_unknown'--->'read_chunk_callback' in backbone, because there is a sanitization logic along the nodes

Path should have an incoming call edge to 'png_handle_unknown', to define a necessary variable used in the sink

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

'rwpng_read_image24_libpng' cannot return from 'png_read_end' and then call 'rwpng_create_row_pointers', since 'rwpng_read_image24_libpng' always calls 'rwpng_create_row_pointers' before calling 'png_read_end'

Path should NOT include a call edge from 'rwpng_read_image24_libpng' to 'rwpng_create_row_pointers' in backbone, because there is a sanitization logic along the nodes

Path should NOT include a return-call sequence of 'rwpng_read_image24_libpng'--(R)-->'rwpng_read_image24'--(R)-->'read_image'--(R)-->'pngquant_file'--(C)-->'write_image'--(C)-->'rwpng_write_image24'--(C)-->'rwpng_create_row_pointers' in backbone, because there is a sanitization logic along the nodes

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

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

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

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

Path should NOT include a call edge from 'deflateInit2_' 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

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

UNSAT (False Alarm)