Linux Driver Verification

OBSERVER AUTOMATON ErrorLocationAutomaton

// This automaton detects error locations that are specified either

// by the label "ERROR" or by an assertion (function call to __assert_fail).

INITIAL STATE Init;

STATE USEFIRST Init :

MATCH LABEL [LDV_ERROR] -> ERROR;

END AUTOMATON