source:
CIVL/examples/focus/simpleForShift.cvl
| Last change on this file was 6d5b8a3, checked in by , 8 months ago | |
|---|---|
|
|
| File size: 252 bytes | |
| Rev | Line | |
|---|---|---|
| [6d5b8a3] | 1 | #pragma CIVL ACSL |
| 2 | $input int N; | |
| 3 | $assume(0 < N); | |
| 4 | int a[N]; | |
| 5 | ||
| 6 | int main() { | |
| 7 | /*@ loop assigns a[0..N-1]; | |
| 8 | @ focus F+1 | a[F]; | |
| 9 | @*/ | |
| 10 | for (int i = 1; i <= N; i++) { | |
| 11 | a[i-1] = 0; | |
| 12 | } | |
| 13 | ||
| 14 | ||
| 15 | //@ focus F; | |
| 16 | $assert($forall(int i:0..N-1) a[i] == 0); | |
| 17 | } |
Note:
See TracBrowser
for help on using the repository browser.
