source:
CIVL/examples/showStates/symbolicArrayWrite.cvl@
53e15b1
| Last change on this file since 53e15b1 was 9fce4f1, checked in by , 11 years ago | |
|---|---|
|
|
| File size: 308 bytes | |
| Line | |
|---|---|
| 1 | #include <civlc.cvh> |
| 2 | |
| 3 | typedef struct Point{ |
| 4 | double x; |
| 5 | double y; |
| 6 | } Point; |
| 7 | |
| 8 | typedef struct Line{ |
| 9 | Point start; |
| 10 | Point end; |
| 11 | } Line; |
| 12 | |
| 13 | $input int N; |
| 14 | $input int K; |
| 15 | $assume(0 <= K && K < N); |
| 16 | |
| 17 | void main(){ |
| 18 | Line A[N]; |
| 19 | Point p0={0,0}, p1={1,1}; |
| 20 | Line l0={p0, p1}; |
| 21 | |
| 22 | A[K]=l0; |
| 23 | $assert(A[K].start.x==0); |
| 24 | } |
| 25 |
Note:
See TracBrowser
for help on using the repository browser.
