source:
CIVL/examples/experimental/multInLoopCond.cvl@
160ecd0
| Last change on this file since 160ecd0 was 6cc497b, checked in by , 12 years ago | |
|---|---|
|
|
| File size: 240 bytes | |
| Rev | Line | |
|---|---|---|
| [6cc497b] | 1 | /* Commandline execution: |
| 2 | * civl verify multInLoopCond.cvl | |
| 3 | * */ | |
| [13953d1] | 4 | $input int N; |
| 5 | $input int M; | |
| 6 | $assume N > 0 && N < 3; | |
| 7 | $assume M > 0 && M < 3; | |
| 8 | ||
| 9 | void main() { | |
| 10 | int k = M*N; | |
| 11 | int a[k]; | |
| 12 | ||
| 13 | for (int i = 0; i < k; i++) { | |
| 14 | a[i] = i; | |
| 15 | } | |
| 16 | } |
Note:
See TracBrowser
for help on using the repository browser.
