1.23
2.0
acw/focus-triggers
main
test-branch
| Rev | Line | |
|---|
| [a6c4add] | 1 | #pragma CIVL ACSL
|
|---|
| [aad342c] | 2 | //======================== civlc.cvh =======================
|
|---|
| 3 | typedef struct $proc $proc;
|
|---|
| [a6c4add] | 4 | /*@ depends_on \nothing;
|
|---|
| 5 | @*/
|
|---|
| [aad342c] | 6 | $system[civlc] void $wait($proc p);
|
|---|
| 7 | //================== structsInFunction.cvl =================
|
|---|
| 8 | void process() {
|
|---|
| 9 | int a;
|
|---|
| 10 | int b;
|
|---|
| 11 | a = b = 10;
|
|---|
| 12 | }
|
|---|
| 13 | int main() {
|
|---|
| 14 | $proc p = $spawn process();
|
|---|
| 15 | $wait(p);
|
|---|
| 16 | }
|
|---|
Note:
See
TracBrowser
for help on using the repository browser.
