[klee-dev] Adding support for another C library

Dan Liew dan at su-root.co.uk
Mon Oct 17 23:47:57 BST 2016


On 17 October 2016 at 22:52, Marko Dimjašević <marko at cs.utah.edu> wrote:
> Hi Dan,
>
> On Mon, 2016-10-17 at 09:44 +0100, Dan Liew wrote:
>> That is likely the cause error. This comes from a rather hacky
>> implementation of a linker inside KLEE.
>>
>> I've mentioned this before that but this is something I'd like to
>> remove from KLEE. I think that **all** linking (and optimization)
>> should be done outside of KLEE using other tools because this would
>> simplify KLEE's implementation and would be far cleaner.
>
> I don't agree with your root-cause reasoning in this case. I tried to
> perform the same linking outside KLEE, i.e. with the llvm-link tool, yet
> I got the same outcome.

The "I'd like to remove..." is a side comment.



More information about the klee-dev mailing list