source:
CIVL/examples/mem/mem_tests/mem_convertion4.cvl
| Last change on this file was 5257f98, checked in by , 2 months ago | |
|---|---|
|
|
| File size: 352 bytes | |
| Rev | Line | |
|---|---|---|
| [5257f98] | 1 | #include<mem.cvh> |
| 2 | #include<stdlib.h> | |
| 3 | #include<pointer.cvh> | |
| 4 | ||
| 5 | $input int N; | |
| 6 | $assume(N > 10); | |
| 7 | int *a; | |
| 8 | int *b[4]; | |
| 9 | ||
| 10 | int main() { | |
| 11 | a = (int *)malloc(sizeof(int) * N); | |
| 12 | for (int i = 0; i < 4; i++) | |
| 13 | b[i] = &a[i]; | |
| 14 | ||
| 15 | $mem m = a + (0 .. N-1); | |
| 16 | ||
| 17 | m = a + (0 .. N-2); | |
| 18 | m = a + 1; | |
| 19 | m = a + (0 .. N-2) + (0 .. N-2); | |
| 20 | $assert($equals(&m, &m)); | |
| 21 | free(a); | |
| 22 | } |
Note:
See TracBrowser
for help on using the repository browser.
