source:
CIVL/mods/dev.civl.abc/examples/contract/acslDemo.c
| Last change on this file was aad342c, checked in by , 3 years ago | |
|---|---|
|
|
| File size: 293 bytes | |
| Line | |
|---|---|
| 1 | #pragma CIVL ACSL |
| 2 | enum t{RED, BLUE}; |
| 3 | |
| 4 | /*@ requires *a==BLUE; |
| 5 | @ ensures \result==*a*2; |
| 6 | @ depends_on \write(a), \read(a); |
| 7 | @ behavior aaa: |
| 8 | @ assumes *a<0; |
| 9 | @ ensures \result < 0; |
| 10 | @ behavior bbb: |
| 11 | @ assumes *a==9; |
| 12 | @ ensures \result==10; |
| 13 | @*/ |
| 14 | int f(int* a){ |
| 15 | return *a*2; |
| 16 | } |
Note:
See TracBrowser
for help on using the repository browser.
