Hi Jiri,

I have successfully compiled (current mainline) klee on OS X although
it does require a bit of tweaking of the makefiles. I will try and
push these to mainline at some point but currently have been occupied
with other priorities when I have time to hack on klee.

One issue which remains even with my changes are that uclibc itself
does not work on klee. I'm not sure what you are hoping to use klee
for, but if it is not a closed program (fully self contained, or with
only minimal dependencies on libc) then adding support for a different
libc which can work on OS X is a fair hunk of work.

I've recently moved to Apple, so as you might imagine I am quite
motivated to do these work, but it is a ways down the road (after an
open source release and work that Cristian and I have planned on the
constraint solver side of klee).

 - Daniel

On Thu, Dec 11, 2008 at 3:24 PM, Raimondas Sasnauskas
<raimondas.sasnauskas at cs.rwth-aachen.de> wrote:
> Hi Jiri,
>
> On 11.12.2008, at 23:26, Ji?? ?im?a wrote:
>>
>> Has any of you successfully compiled on OS X (Darwin Kernel Version
>> 9.5.0)? Thanks.
>
> I've tried it once. Some of the compilation errors could be fixed
> by minor manual changes, but I didn't know how to fix the issues with
> __ctype_* functions (it seems taht they aren't available on Mac OS X):
>
> In lib/Executor.cpp
>
> #ifndef WINDOWS
>  /* From /usr/include/errno.h: it [errno] is a per-thread variable. */
>  int *errno_addr = __errno_location();
>  addExternalObject(state, (void *)errno_addr, sizeof *errno_addr, 0, false);
>
>  /* from /usr/include/ctype.h:
>       These point into arrays of 384, so they can be indexed by any
> `unsigned
>       char' value [0,255]; by EOF (-1); or by any `signed char' value
>       [-128,-1).  ISO C requires that the ctype functions work for `unsigned
> */
>    // XXX: there is some confusion over whether starts at *addr or *addr-128
>  let(addr, __ctype_b_loc());
>  MemoryObject *ref = 0;
>  ref = addExternalObject(state, (void *)(*addr-128), 384 * sizeof **addr, 0,
> true);
>  addExternalObject(state, addr, 4, ref, true);
>
>  let(lower_addr, __ctype_tolower_loc());
>  ref = addExternalObject(state, (void *)(*lower_addr-128), 384 * sizeof
> **lower_addr, 0, true);
>  addExternalObject(state, lower_addr, 4, ref, true);
>
>  let(upper_addr, __ctype_toupper_loc());
>  ref = addExternalObject(state, (void *)(*upper_addr-128), 384 * sizeof
> **upper_addr, 0, true);
>  addExternalObject(state, upper_addr, 4, ref, true);
> #endif
>
>
>
> - Raimondas
>
> --
> Raimondas Sasnauskas, PhD Student
> Distributed Systems Group
> RWTH Aachen University
> http://ds.cs.rwth-aachen.de/members/sasnauskas
>
>
>
>
>
>
>
> _______________________________________________
> klee-dev mailing list
> klee-dev at keeda.Stanford.EDU
> http://keeda.Stanford.EDU/mailman/listinfo/klee-dev
>
>

Reply via email to