Dear all, I am continuing to receive the following error. WARNING: Linking two modules of different data layouts! WARNING: Linking two modules of different data layouts! WARNING: Linking two modules of different data layouts!
I think that it is related to the llvm-byte code generated by the clang compiler. Can I ignore the issue? As well I didn't find a solution for the -optimize problem. Best regards, Giuseppe 2010/4/26 Giuseppe Di Guglielmo <giuseppe.diguglielmo at gmail.com>: > Dear all, > > as preliminary remarks, I have no idea if the following issues are related > to my tiny knowledge of the tool. > > > > At the moment I am running the svn-HEAD klee as follows. The ferguson.c code > is hereby attached. > > > > # clang -I $KLEE_HOME/include/ -g -c -emit-llvm ../src/ferguson.c -o > ferguson.bc > > # klee -time-max 3600 ferguson.bc > > ... thousand of paths are covered ... > > # klee -optimize ferguson.bc > > KLEE: output directory = "klee-out-5" > > 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 = 13 > > KLEE: done: completed paths = 1 > > KLEE: done: generated tests = 1 > > > > Why does the -optimize flag produce poor results? What are these WARNING > messages? > > > > Best regards, > > Giuseppe > > > > > > > > > > -- Se non ci fosse l'ultimo momento non si riuscirebbe a fare niente.
