File tree 1 file changed +12
-10
lines changed
1 file changed +12
-10
lines changed Original file line number Diff line number Diff line change @@ -244,30 +244,32 @@ The table below summarizes the coverage criteria that CBMC supports.
244
244
245
245
<table class="fancy">
246
246
247
+ <tr><th>Criterion</th><th>Definition</th></tr>
248
+
247
249
<tr><td>assertion</td>
248
- <td>For every assertion, generate a test that reaches it</td></tr>
250
+ <td class="alt" >For every assertion, generate a test that reaches it</td></tr>
249
251
250
- <tr><td>location</td>
251
- <td>For every location, generate a test that reaches it</td></tr>
252
+ <tr><td class="alt" >location</td>
253
+ <td class="alt" >For every location, generate a test that reaches it</td></tr>
252
254
253
255
<tr><td>branch</td>
254
- <td>Generate a test for every branch outcome</td></tr>
256
+ <td class="alt" >Generate a test for every branch outcome</td></tr>
255
257
256
- <tr><td>decision</td>
257
- <td>Generate a test for both outcomes of every Boolean expression
258
+ <tr><td class="alt" >decision</td>
259
+ <td class="alt" >Generate a test for both outcomes of every Boolean expression
258
260
that is not an operand of a propositional connective</td></tr>
259
261
260
262
<tr><td>condition</td>
261
263
<td>Generate a test for both outcomes of every Boolean expression</td></tr>
262
264
263
- <tr><td>mcdc</td>
264
- <td>Modified Condition/Decision Coverage (MC/DC)</td></tr>
265
+ <tr><td class="alt" >mcdc</td>
266
+ <td class="alt" >Modified Condition/Decision Coverage (MC/DC)</td></tr>
265
267
266
268
<tr><td>path</td>
267
269
<td>Bounded path coverage</td></tr>
268
270
269
- <tr><td>cover</td>
270
- <td>Generate a test for every <code>__CPROVER_cover</code> statement.
271
+ <tr><td class="alt" >cover</td>
272
+ <td class="alt" >Generate a test for every <code>__CPROVER_cover</code> statement
271
273
</td></tr>
272
274
273
275
</table>
You can’t perform that action at this time.
0 commit comments