MrSlippery

Hamiltonian Cycle Found with KLEE

Mar 21st, 2016
337
0
Never
Not a member of Pastebin yet? Sign Up, it unlocks many cool features!
Bash 1.30 KB | None | 0 0
  1. user@localhost:~/travel$ klee-go travel.c
  2. travel.c:52:2: warning: implicit declaration of function '__assert_fail' is invalid in
  3.       C99 [-Wimplicit-function-declaration]
  4.         klee_assert(!ham_cycle(cycle));
  5.         ^
  6. ../klee/include/klee/klee.h:96:6: note: expanded from macro 'klee_assert'
  7.    : __assert_fail (#expr, __FILE__, __LINE__, __PRETTY_FUNCTION__))    \
  8.      ^
  9. 1 warning generated.
  10. KLEE: NOTE: Using klee-uclibc : /home/user/klee/Release+Asserts/lib/klee-uclibc.bca
  11. KLEE: NOTE: Using model: /home/user/klee/Release+Asserts/lib/libkleeRuntimePOSIX.bca
  12. KLEE: output directory is "/home/user/travel/klee-out-3"
  13. Using STP solver backend
  14. KLEE: WARNING: undefined reference to function: klee_posix_prefer_cex
  15. KLEE: WARNING ONCE: calling external: syscall(16, 0, 21505, 47742720)
  16. KLEE: ERROR: /home/user/travel/travel.c:52: ASSERTION FAIL: !ham_cycle(cycle)
  17. KLEE: NOTE: now ignoring this error at this location
  18.  
  19. KLEE: done: total instructions = 2568
  20. KLEE: done: completed paths = 16
  21. KLEE: done: generated tests = 16
  22.  
  23. ktest file : 'klee-last/test000015.ktest'
  24. args       : ['travel.bc']
  25. num objects: 2
  26. object    0: name: 'model_version'
  27. object    0: size: 4
  28. object    0: data: '\x01\x00\x00\x00'
  29. object    1: name: 'cycle'
  30. object    1: size: 6
  31. object    1: data: '\x04\x02\x03\x00\x01\x04'
Advertisement
Add Comment
Please, Sign In to add comment