main
| Rev | Line | |
|---|
| [1b85498] | 1 | $input int n;
|
|---|
| 2 | $assume(n > 0);
|
|---|
| 3 |
|
|---|
| 4 | typedef struct {
|
|---|
| 5 | int x;
|
|---|
| 6 | float y;
|
|---|
| 7 | } simple_t;
|
|---|
| 8 |
|
|---|
| 9 | int main() {
|
|---|
| 10 | simple_t s[n] = (simple_t[n])$lambda(int j) (simple_t){42, .9};
|
|---|
| 11 |
|
|---|
| 12 | $assert($forall (int i : 0 .. n-1) s[i].x == 42 && s[i].y == 0.9);
|
|---|
| 13 |
|
|---|
| 14 | simple_t s2[n] = (simple_t[n])$lambda(int i) (simple_t){.y = .9, .x = 42};
|
|---|
| 15 |
|
|---|
| 16 | $assert($forall (int i : 0 .. n-1) s2[i].x == 42 && s2[i].y == 0.9);
|
|---|
| 17 |
|
|---|
| 18 | simple_t s3[n] = (simple_t[n])$lambda(int i) (simple_t){.y = .9};
|
|---|
| 19 |
|
|---|
| 20 | $assert($forall (int i : 0 .. n-1) s3[i].x == 0 && s3[i].y == 0.9);
|
|---|
| 21 |
|
|---|
| 22 | simple_t s4[n] = (simple_t[n])$lambda(int i) (simple_t){i};
|
|---|
| 23 |
|
|---|
| 24 | $assert($forall (int i : 0 .. n-1) s4[i].x == i && s4[i].y == 0.0);
|
|---|
| 25 | }
|
|---|
Note:
See
TracBrowser
for help on using the repository browser.