On Sun, Mar 14, 2010 at 1:39 PM, David Brumley <dbrumley at gmail.com> wrote: >> Hi, >> >> I just checked in a patch for building KLEE with LLVM 2.7. I have >> tested it on Linux x86_32 with LLVM 2.6 and 2.7 and on Darwin x86_32 >> and x86_64. I'd appreciate it if someone can test it on Linux x86_64. > > Hi, > I was interested in the "Darwin" part. Last time I tried to build klee > on a Mac Klee built fine, but uclib failed. A fairly quick look made > it seem like porting it would be hard. ?Does uclibc also work on > darwin, and if so, does anyone have build tips/patches?
KLEE itself should work fine on Darwin. uClibc on Darwin is hopeless, though, at least in the way we use it on Linux. I really want a solution to this, as it is what usually blocks me from doing real work on KLEE -- my only linux box is fairly old/slow. There are two possible long term solutions to this problem: (1) Use uClibc by cross compiling to a linux environment. This still requires work in KLEE to accurately model the fact that it is simulating a linux environment. Just running syscall isn't likely to work well! :) (2) Figure out how to build Darwin's libc with llvm-gcc/clang, and integrate that with KLEE. I've never looked at the Darwin Libc project, so I have no idea how easy/hard this is. If it turned out to be easy to build a libc .bc file (for example, there is little to no inline asm), this might not be too hard. - Daniel > > Thanks! > -David > > >> >> Please let me know of any problems. >> >> ?- Daniel >> _______________________________________________ >> klee-dev mailing list >> klee-dev at keeda.stanford.edu >> http://keeda.Stanford.EDU/mailman/listinfo/klee-dev >> >
