a) Draw the Control Flow Automaton (CFA) model of the program sample. Use the numbers specified...

 

Transcribed Image Text:

a) Draw the Control Flow Automaton (CFA) model of the program sample. Use the numbers specified next to the statements (0, 1, 2) to label the CFA locations. Use a specific location err for the case when there is division with zero in statement 2, and location end for the normal termination of the program. 0: 1: 2: b int b = 25 while (25 b*b < 0) { } b = (b+25/b)/2; b) For model checking of the CFA we use location and predicate abstraction, using a single predicate (b==0). Decide whether the following path appears in the abstract state space (justify your answer): (0, true) (1, false) (2, true) (err, true). c) Someone claims that in the abstract state space he found the following counterexample to the correct behavior of the program: (0, false) (1, false) (2, false) (err, false). Check whether this path can be traversed in the concrete state space (justify your answer). a) Draw the Control Flow Automaton (CFA) model of the program sample. Use the numbers specified next to the statements (0, 1, 2) to label the CFA locations. Use a specific location err for the case when there is division with zero in statement 2, and location end for the normal termination of the program. 0: 1: 2: b int b = 25 while (25 b*b < 0) { } b = (b+25/b)/2; b) For model checking of the CFA we use location and predicate abstraction, using a single predicate (b==0). Decide whether the following path appears in the abstract state space (justify your answer): (0, true) (1, false) (2, true) (err, true). c) Someone claims that in the abstract state space he found the following counterexample to the correct behavior of the program: (0, false) (1, false) (2, false) (err, false). Check whether this path can be traversed in the concrete state space (justify your answer).