source:
CIVL/examples/languageFeatures/switch.cvl@
85d4675
| Last change on this file since 85d4675 was 36b5ada, checked in by , 12 years ago | |
|---|---|
|
|
| File size: 305 bytes | |
| Rev | Line | |
|---|---|---|
| [36b5ada] | 1 | /* Commandline execution: |
| 2 | * civl verify switch.cvl | |
| 3 | * */ | |
| [420d7f3] | 4 | #include <civlc.h> |
| 5 | $input int i; | |
| 6 | $assume i >= 0 && i < 10; | |
| 7 | ||
| 8 | void main() { | |
| 9 | switch (i) { | |
| 10 | case 0: | |
| 11 | $assert i == 0; | |
| 12 | break; | |
| 13 | case 1: | |
| 14 | case 2: | |
| 15 | case 3: | |
| 16 | $assert i < 4; | |
| 17 | break; | |
| 18 | default: | |
| 19 | $assert i > 3; | |
| 20 | } | |
| 21 | } |
Note:
See TracBrowser
for help on using the repository browser.
