# Compile the program for use with KLEE (generating LLVM bytecode).
user@machine:~/einstein$ clang -I../klee/include -emit-llvm -c einstein.c
einstein.c:128:3: warning: implicit declaration of function '__assert_fail' is invalid in C99 [-Wimplicit-function-declaration]
klee_assert(!(
^
../klee/include/klee/klee.h:96:6: note: expanded from macro 'klee_assert'
: __assert_fail (#expr, __FILE__, __LINE__, __PRETTY_FUNCTION__)) \
^
1 warning generated.
# Run KLEE on the bytecode
user@machine:~/einstein$ klee --libc=uclibc --posix-runtime einstein.bc
KLEE: NOTE: Using klee-uclibc : /home/user/klee/Release+Asserts/lib/klee-uclibc.bca
KLEE: NOTE: Using model: /home/user/klee/Release+Asserts/lib/libkleeRuntimePOSIX.bca
KLEE: output directory is "/home/user/einstein/klee-out-1"
KLEE: WARNING: undefined reference to function: klee_posix_prefer_cex
KLEE: WARNING ONCE: calling external: syscall(16, 0, 21505, 51755536)
KLEE: WARNING ONCE: calling __user_main with extra arguments.
KLEE: ERROR: (location information missing) ASSERTION FAIL: !( norwegian_first_house() && brit_house_red() && swede_pet_dog() && dane_drink_tea() && g_near_w() && green_drink_coffee() && n_near_c() && pall_pet_birds() && yellow_smoke_dunhill() && center_drink_milk() && german_smoke_prince() && n_near_w() && n_near_b() && h_near_d() && masters_drink_beer() && someone_pet_fish() )
KLEE: NOTE: now ignoring this error at this location
KLEE: done: total instructions = 1776493
KLEE: done: completed paths = 26958
KLEE: done: generated tests = 26957
# A violation of the assertion that no solution exists was found - therefore a solution does exist, so let's see it.
user@machine:~/einstein$ ls klee-last/*.assert.err
klee-last/test024010.assert.err
user@machine:~/einstein$ ktest-tool klee-last/test024010.ktest
ktest file : 'klee-last/test024010.ktest'
args : ['einstein.bc']
num objects: 2
object 0: name: 'model_version'
object 0: size: 4
object 0: data: '\x01\x00\x00\x00'
object 1: name: 'e'
object 1: size: 25
object 1: data: 'nycwddbhtnbrbmpswdbmggfcr'
# Let's break the result down into lines for each person.
# n y c w d
# d b h t n
# b r b m p
# s w d b m
# g g f c r
# ^
# The last line contains the answer: the German ('g') lives in the green ('g') house, has a pet fish ('f'), drinks coffee ('c'), and smokes Prince ('r').
Comments