main
|
Last change
on this file was ea777aa, checked in by Alex Wilton <awilton@…>, 3 years ago |
|
Moved examples, include, build_default.properties, common.xml, and README out from dev.civl.com into the root of the repo.
git-svn-id: svn://vsl.cis.udel.edu/civl/trunk@5704 fb995dde-84ed-4084-dfe6-e5aef3e2452c
|
-
Property mode
set to
100644
|
|
File size:
1.6 KB
|
| Line | |
|---|
| 1 | pointer_t {
|
|---|
| 2 | int b;
|
|---|
| 3 | int offset;
|
|---|
| 4 | }
|
|---|
| 5 |
|
|---|
| 6 | CASE 0:
|
|---|
| 7 | requires \valid(p);
|
|---|
| 8 | assigns *p;
|
|---|
| 9 | ensures *p == 0;
|
|---|
| 10 | f(int * p);
|
|---|
| 11 |
|
|---|
| 12 | PROPOSED SOLUTION 0:
|
|---|
| 13 | int H0[1][];
|
|---|
| 14 | pointer_t p';
|
|---|
| 15 | requires p' == {0, 0};
|
|---|
| 16 | assigns H0[p'.b][p'.offset + 0];
|
|---|
| 17 | ensures H0[p'.b][p'.offset + 0] == 0;
|
|---|
| 18 | p = &H0[p'.b][p'.offset];
|
|---|
| 19 | f(p);
|
|---|
| 20 |
|
|---|
| 21 | ##############################################################
|
|---|
| 22 |
|
|---|
| 23 | CASE 1:
|
|---|
| 24 | typedef struct t {
|
|---|
| 25 | int * x;
|
|---|
| 26 | } T;
|
|---|
| 27 |
|
|---|
| 28 | requires \valid(p) && \valid(p->x + 0 .. 10);
|
|---|
| 29 | assigns *(p->x);
|
|---|
| 30 | ensures (p->x[0]) == 0;
|
|---|
| 31 | f(T * p);
|
|---|
| 32 |
|
|---|
| 33 | PROPOSED SOLUTION 1:
|
|---|
| 34 | T H0[1][];
|
|---|
| 35 | int H1[2][];
|
|---|
| 36 | int p';
|
|---|
| 37 | requires p' == {0,0} && H0[p'.b][p'.offset].x' == {1, 0};
|
|---|
| 38 | assigns H1[H0[p'][0].x'.b][H0[p'][0].x'.offset + 0];
|
|---|
| 39 | ensures H1[H0[p'][0].x'.b][H0[p'][0].x'.offset + 0] == 0;
|
|---|
| 40 | p = H0[p'];
|
|---|
| 41 | p->x = H1[H0[p'][0].x'];
|
|---|
| 42 | f(p);
|
|---|
| 43 |
|
|---|
| 44 | ##############################################################
|
|---|
| 45 |
|
|---|
| 46 | CASE 2:
|
|---|
| 47 | requires \valid(p) || p == MPI_IN_PLACE;
|
|---|
| 48 | f(void *p);
|
|---|
| 49 |
|
|---|
| 50 | PROPOSED_SOLUTION 2:
|
|---|
| 51 | char H0[1][];
|
|---|
| 52 | int H1[2][];
|
|---|
| 53 | int p';
|
|---|
| 54 | int MIPS = 1;
|
|---|
| 55 | H1[MIPS][0] = MPI_IN_PLACE_SPOT;
|
|---|
| 56 | requires p' == 0 || p' == MIPS;
|
|---|
| 57 |
|
|---|
| 58 | ##############################################################
|
|---|
| 59 |
|
|---|
| 60 | CASE 3:
|
|---|
| 61 | requires \valid(p + 0 .. 10) && \valid(p[0 .. 10] + 0 .. 10);
|
|---|
| 62 | assigns p[0 .. 10][0 .. 10];
|
|---|
| 63 | f(void **p);
|
|---|
| 64 |
|
|---|
| 65 | PROPOSED_SOLUTION 2:
|
|---|
| 66 | int H0[1][]; //'char *' is 'int' as well
|
|---|
| 67 | char H1[11][];
|
|---|
| 68 |
|
|---|
| 69 | requires p' == 0 && FORALL i; 0<=i<=10 ==> H0[p'][i] == 1 + i;
|
|---|
| 70 | assigns H1[H0[p'][0 .. 10]][0 .. 10];
|
|---|
| 71 |
|
|---|
| 72 | ##############################################################
|
|---|
| 73 |
|
|---|
| 74 | Possible patterns of pointer p in expressions:
|
|---|
| 75 | p[n] -> H0[p'][n]
|
|---|
| 76 |
|
|---|
| 77 | p->x -> H0[p'].x
|
|---|
| 78 |
|
|---|
| 79 | *p -> H0[p'][0]
|
|---|
| 80 |
|
|---|
| 81 | p + n -> &H0[p'][0] + n
|
|---|
| 82 |
|
|---|
| 83 | p - q -> UNIMPLEMENTED/ either within an array or UNDEFINED
|
|---|
| 84 |
|
|---|
| 85 |
|
|---|
| 86 |
|
|---|
| 87 |
|
|---|
Note:
See
TracBrowser
for help on using the repository browser.
