bbe_alarm1_1
path 1



(User Feedback)

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


path 2



(User Feedback)

Path should NOT have an incoming edge to 'bn_printf', because there is a string sanitization in the node


UNSAT (false alarm)





bbe_alarm1_2
path 1



(User Feedback)

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


path 2



(User Feedback)

Path should NOT have an incoming edge to 'bn_printf', because there is a string sanitization in the node


UNSAT (false alarm)





bbe_alarm1_3
path 1



(User Feedback)

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


path 2



(User Feedback)

Path should NOT have an incoming edge to 'bn_printf', because there is a string sanitization in the node


UNSAT (false alarm)