source:
CIVL/examples/languageFeatures/atomStatement.cvl@
85d4675
| Last change on this file since 85d4675 was 36b5ada, checked in by , 12 years ago | |
|---|---|
|
|
| File size: 758 bytes | |
| Rev | Line | |
|---|---|---|
| [36b5ada] | 1 | /* Commandline execution: |
| 2 | * civl verify atomStatement.cvl | |
| 3 | * */ | |
| [10e8759] | 4 | int n = 3; |
| 5 | void foo(){ | |
| [36b5ada] | 6 | int k = n; |
| 7 | k = k + 1; | |
| [10e8759] | 8 | } |
| 9 | ||
| 10 | void main(){ | |
| [36b5ada] | 11 | int i = 0; |
| 12 | int x = 3; | |
| 13 | ||
| 14 | $atom { | |
| 15 | if(i < 0) | |
| 16 | i = 1; | |
| 17 | else | |
| 18 | i = 2; | |
| 19 | } | |
| 20 | $assert i == 2; | |
| 21 | $atom | |
| 22 | if(i > 0) | |
| 23 | i = 1; | |
| 24 | else | |
| 25 | i = 2; | |
| 26 | $assert i == 1; | |
| 27 | $atom { | |
| 28 | i = 2; | |
| 29 | switch(i) { | |
| 30 | case 1: i = 2; | |
| 31 | case 2: i = 3;break; | |
| 32 | default: i = 5; | |
| [10e8759] | 33 | } |
| [36b5ada] | 34 | } |
| 35 | $assert i == 3; | |
| 36 | $atom { | |
| 37 | i = 0; | |
| 38 | for(int j = 0; j < 10; j++) { | |
| 39 | i += j; | |
| 40 | } | |
| 41 | } | |
| 42 | $assert i == 45; | |
| 43 | $atom { | |
| 44 | for(int m = 0; m < 5; m++) { | |
| 45 | $spawn foo(); | |
| [10e8759] | 46 | } |
| [36b5ada] | 47 | } |
| 48 | //nested atomic and non-pure-local atomic block | |
| 49 | $atom { | |
| 50 | n = 0; | |
| 51 | n += 1; | |
| 52 | $atom { | |
| 53 | i+=2; | |
| 54 | i += 3; | |
| 55 | } | |
| 56 | n += 9; | |
| 57 | } | |
| 58 | $assert n == 10; | |
| [10e8759] | 59 | } |
Note:
See TracBrowser
for help on using the repository browser.
