source:
CIVL/mods/dev.civl.com/examples/svcomp17/unique_loop.c@
cb4d4f4
| Last change on this file since cb4d4f4 was aad342c, checked in by , 3 years ago | |
|---|---|
|
|
| File size: 310 bytes | |
| Rev | Line | |
|---|---|---|
| [addb943] | 1 | extern void __VERIFIER_assume(int); |
| 2 | extern void __VERIFIER_error() __attribute__ ((__noreturn__)); | |
| 3 | extern int __VERIFIER_nondet_int(void); | |
| 4 | ||
| 5 | int main() { | |
| 6 | int y = 1; | |
| 7 | ||
| 8 | for(int i=0; i<2; i++) { | |
| 9 | if (y > 0) { | |
| 10 | y = __VERIFIER_nondet_int(); | |
| 11 | } | |
| 12 | } | |
| 13 | ||
| 14 | if (y < 0) { | |
| 15 | ERROR: __VERIFIER_error(); | |
| 16 | } | |
| 17 | } |
Note:
See TracBrowser
for help on using the repository browser.
