case Cn: if ( i ++ == 0) pem (TN(C == (Cn)));
INST(Sn)
default: if ( i ++ == 0) { pem (TN(C!= (C1)));
pem (TN(C!= (C2)));
.
.
.
pem (TN(C!= (Cn)));
}INST(Sn+1)
}}
106
Automatic Generation of Symbolic Traces
The reason why we use i here is that cases serve just as labels. After
the code for one case is done, execution falls through to the next unless
we take explicit action to escape. The flag i is used to ensure that only
the condition that is true is included in the trace subprogram.
7. RETURN Statement:
INST(return;) = pem (TN(return));
return;
INST(return E;) = pem (TN(return E));
return E;
8. EXIT Statement:
INST(exit;) = pem (TN(exit));
exit;
INST(exit E;) = pem (TN(exit E));
exit E;
9. Labeled Statement:
INST(LABEL: S) = LABEL: INST(S)
10. Compound Statement:
INST({declaration-list
statement-list})
= {
declaration-list
INST(statement-list)
} INST(S1; S2) = INST(S1)
INST(S2)
11. Other Statements:
INST(break;) = break;
INST(continue;) = continue;
INST(goto LABEL;) = goto LABEL;
INST(;) = ;
107
Appendix A: Examples
Presented in this appendix are four examples showing in various degrees
of detail how the present method can be applied to programs written in
C++.
Example A.1 shows how to insert constraints into a program to form a
subprogram representing an execution path. It also shows how the rules
developed in Chapter 3 can be used to simplify the subprogram to the
extent possible.
Pages:
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115