I have been trying to trace back the problems I'm having with KLEE (see the test failures to which I referred last week) and have started to get suspicious even of the simplest warnings.
When I run tutorial example 1 (the islower.c example) with a clean system I get the following warnings: $ klee islower.o KLEE: output directory = "klee-out-0" WARNING: Linking two modules of different data layouts! WARNING: Linking two modules of different data layouts! WARNING: Linking two modules of different data layouts! KLEE: done: total instructions = 70 KLEE: done: completed paths = 3 KLEE: done: generated tests = 3 The correct number of tests is generated and the tests themselves are valid (as described in the tutorial page). However, trying to read LinkModules.cpp where the warning appears, it's not clear (to me) what is being linked and what the two layouts are. I am using llvm version 2.6 (having downgraded from 2.7): $klee --version Low Level Virtual Machine (http://llvm.org/): llvm version 2.6 Optimized build with assertions. Built Jun 16 2010(15:23:17). Registered Targets: x86 - 32-bit X86: Pentium-Pro and above x86-64 - 64-bit X86: EM64T and AMD64 $ llvm-gcc --version llvm-gcc (GCC) 4.2.1 (Based on Apple Inc. build 5649) (LLVM build 2.6) Cheers Chris Hobbs
