source: CIVL/mods/dev.civl.com/examples/direct/switch.c@ cb4d4f4

main test-branch
Last change on this file since cb4d4f4 was aad342c, checked in by Stephen Siegel <siegel@…>, 3 years ago

Performing huge refactor to incorporate ABC, GMC, and SARL into CIVL repo and use Java modules.

git-svn-id: ​svn://vsl.cis.udel.edu/civl/trunk@5664 fb995dde-84ed-4084-dfe6-e5aef3e2452c
  • Property mode set to 100644
File size: 619 bytes
Line 
1extern void __VERIFIER_error() __attribute__ ((__noreturn__));
2extern void __VERIFIER_assume(int);
3extern int __VERIFIER_nondet_int();
4
5int main( ) {
6 /* Switch on case 1 */
7 int input = 1;
8 switch (input) {
9 case 1:
10 break;
11 case 2:
12 break;
13 default:
14 __VERIFIER_error();
15 break;
16 }
17
18 /* Fallthrough */
19 switch (input) {
20 case 1:
21 case 2:
22 break;
23 default:
24 __VERIFIER_error();
25 break;
26 }
27
28 /* Default */
29 input = 5;
30 switch (input) {
31 case 1:
32 break;
33 case 2:
34 break;
35 default:
36 __VERIFIER_error();
37 break;
38 }
39 return 0;
40}
Note: See TracBrowser for help on using the repository browser.