source:
CIVL/mods/dev.civl.com/examples/backend/symbolicConstants.cvl@
e49edeb
| Last change on this file since e49edeb was aad342c, checked in by , 3 years ago | |
|---|---|
|
|
| File size: 180 bytes | |
| Rev | Line | |
|---|---|---|
| [8f3107d] | 1 | |
| 2 | ||
| 3 | void foo(){ | |
| 4 | int a; | |
| 5 | ||
| 6 | $havoc(&a); | |
| 7 | $assume(a<10); | |
| 8 | } | |
| 9 | ||
| 10 | void goo(){ | |
| 11 | int b, c; | |
| 12 | $havoc(&b); | |
| 13 | //$assume(b>0); | |
| 14 | $havoc(&c); | |
| 15 | $assert(b<10); | |
| 16 | } | |
| 17 | ||
| 18 | int main(){ | |
| 19 | foo(); | |
| 20 | goo(); | |
| 21 | } |
Note:
See TracBrowser
for help on using the repository browser.
