On Sat, Jun 12, 2010 at 1:18 AM, Liu Jian <gjk.liu at gmail.com> wrote: > > > On Fri, Jan 29, 2010 at 2:07 PM, Daniel Dunbar <daniel at zuster.org> wrote: >> >> Hi Liu Jian, >> >> On Sun, Dec 27, 2009 at 6:16 PM, Liu Jian <gjk.liu at gmail.com> wrote: >> > Hi all, >> > >> > ??? I will try to apply klee to check Xen (e.x. version 3.3.0) source >> > code >> > like >> > your similar work to HiStar. But meet so many errors, most of them about >> > link and inline asm. Is there any detail stuff describing how do you >> > deal >> > with >> > HiStar?? thank! >> >> We wrote a custom driver for HiStar which called the kernel system >> call routines directly, and hand coded the calls to initialize the >> kernel state. Fortunately, HiStar didn't have inline assembly pieces >> in the core kernel, and building it with llvm-gcc was quite simple. >> >> If you want to test something with inline assembly, you will have to >> rewrite those parts in C or something which can be compiled to LLVM IR >> before you can use KLEE effectively. > > ? ? Is there direction on how to rewrite a inline assembly with C? thanks!
Sorry, not really. Inline asm can be quite complicated, and of course sometimes it is used when there is no direct C equivalent. - Daniel > > ? ? Liu Jian >
