source:
CIVL/examples/ACSLTransformation/predicate-bad_decl_twice.cvl@
a0b7ab5
| Last change on this file since a0b7ab5 was d70594d, checked in by , 8 years ago | |
|---|---|
|
|
| File size: 226 bytes | |
| Rev | Line | |
|---|---|---|
| [d70594d] | 1 | #pragma CIVL ACSL |
| 2 | ||
| 3 | int x = 9; | |
| 4 | ||
| 5 | /*@ predicate eq(int a, int b) = | |
| 6 | @ a == x && b == x; | |
| 7 | @ | |
| 8 | @ predicate eq(int a, int b); | |
| 9 | @*/ | |
| 10 | int main(){ | |
| 11 | int a = 9; | |
| 12 | int b = 9; | |
| 13 | ||
| 14 | $assert(eq(a, b)); | |
| 15 | x = 8; | |
| 16 | $assert(!eq(a, b)); | |
| 17 | } |
Note:
See TracBrowser
for help on using the repository browser.
