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 | |
| Rev | Line | |
|---|---|---|
| [aad342c] | 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.
