Hi George, This link is pretty useful for me.
In my experiments, I use multiple thread applications. They execute socket functions. Thanks for your information ! I will forward this email to Dazhi too. He developed white-box test tool with symbolic execution before. He may be interested in the network-Klee. Sincerely, Wenhua Wang ________________________________________ From: George Argyros [[email protected]] Sent: Saturday, October 16, 2010 12:20 To: Wang, Wenhua Cc: klee-dev at keeda.stanford.edu Subject: Re: [klee-dev] one question about applying Klee to multi-file applications. Hi Wang, If you intend to test network applications with klee, you will probably encounter errors when trying to execute socket functions. See http://keeda.stanford.edu/pipermail/klee-dev/2010-June/000411.html Btw, does anyone plan to implement a network model for klee? Regards, George On Wed, Oct 13, 2010 at 10:03 PM, Wang, Wenhua <wenhua.wang at mavs.uta.edu> wrote: > Dear Sir/Madam, > I have run Klee in our experiments. It is an excellent tool. > But, I have a question about applying Klee to multi-file applications. > I think, so far, Klee can not be applied to multi-file applications. Is it > exactly right ? > I reached this conclusion because Klee failed when I applied > to Ghttpd-1.4-4. You can check the source code of Ghttpd-1.4-4 in the > attachment. > Klee failed to generate an executable file by combining *.o files. > The following is the error information. You can also check them in the > attachment. > ~~~~~~ > root at wwh-desktop:/usr/llvm2.7/llvm-2.7/klee/mytest/ghttpd-1.4-4# make > llvm-gcc --emit-llvm -g -c -o main.o main.c > main.c: In function ?main?: > main.c:88: warning: cast from pointer to integer of different size > llvm-gcc --emit-llvm -g -c -o protocol.o protocol.c > llvm-gcc --emit-llvm -g -c -o util.o util.c > util.c: In function ?Log?: > util.c:225: warning: assignment makes pointer from integer without a cast > util.c:227: warning: incompatible implicit declaration of built-in function > ?strftime? > llvm-gcc -o ghttpd main.o protocol.o util.o > main.o: file not recognized: File format not recognized > collect2: ld returned 1 exit status > make: *** [ghttpd] Error 1 > ~~~~~~ > In my experiments, I just used "llvm-gcc" to replace "GCC" in the makefile > and used "--emit-llvm -g" to replace other gcc option flags in the makefile. > > Please write to me, if I applied Klee to multi-file applications in a wrong > way. > Thanks! > Sincerely, > > Wenhua Wang > _______________________________________________ > klee-dev mailing list > klee-dev at keeda.stanford.edu > http://keeda.Stanford.EDU/mailman/listinfo/klee-dev > >
