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!
Liu Jian
-------------- next part --------------
An HTML attachment was scrubbed...
URL:
http://keeda.Stanford.EDU/pipermail/klee-dev/attachments/20100612/08d8e6d8/attachment.html
