An Alarm Classification Using Shovel

'_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

glpsol_alarm1_1

path 1

(User Feedback)

Path should NOT include a call edge from 'printf_func' to 'print_text' in backbone, because there is a string sanitization in the latter node

UNSAT (false alarm)

glpsol_alarm1_2

path 1

(User Feedback)

Path should NOT include a call edge from 'printf_func' to 'print_text' in backbone, because there is a string sanitization in the latter node

UNSAT (false alarm)

glpsol_alarm1_3

path 1

(User Feedback)

Path should NOT include a call edge from 'printf_func' to 'print_text' in backbone, because there is a string sanitization in the latter node

UNSAT (false alarm)

glpsol_alarm1_4

path 1

(User Feedback)

Path should NOT include a call edge from 'printf_func' to 'print_text' in backbone, because there is a string sanitization in the latter node

UNSAT (false alarm)

glpsol_alarm1_5

path 1

(User Feedback)

Path should NOT include a call edge from 'printf_func' to 'print_text' in backbone, because there is a string sanitization in the latter node

UNSAT (false alarm)

glpsol_alarm1_6

path 1

(User Feedback)

Path should NOT include a call edge from 'printf_func' to 'print_text' in backbone, because there is a string sanitization in the latter node

UNSAT (false alarm)