GNU bug report logs - #72106
[PATCH 0/3] gnu: klee: Enable test suite

Previous Next

Full log

View this message in rfc822 format

From: Sören Tempel <soeren <at> soeren-tempel.net>
To: Liliana Marie Prikler <liliana.prikler <at> gmail.com>
Cc: 72106 <at> debbugs.gnu.org
Subject: [bug#72106] [PATCH 0/3] gnu: klee: Enable test suite
Date: Sun, 14 Jul 2024 20:29:48 +0200

Hi Liliana,

Thanks for your feedback, I added a v2 to incorporate your feedback.

Liliana Marie Prikler <liliana.prikler <at> gmail.com> wrote:
> Can we use a wrapper instead?

Sure, good idea! I modified the patch to wrap klee-stats instead.
Haven't done that so far so please check if I did it correctly :)

> > Lastly, I also passed a custom #:strip-directories argument to avoid
> > stripping of LLVM bitcode which (prior to this patchset) caused
> > strip(1) to emit several warnings in the build log.
>
> There is only .bca files in there, right?

Only .bca files and one shared library (libkleeRuntest.so) are in /lib.
Does stripping of shared libraries do anything? If so: Should we just
live with the warnings or should we strip that file individually?

> > P.S.: I also think it might be worthwhile to only enable the KLEE
> > package on x86_64 Linux <https://issues.guix.gnu.org/71925#18>.  Let
> > me know if I should add that as well :-)
>
> Ah, yes, good catch.

I added two additional commits to set supported-systems for KLEE.

Best,
Sören

Previous Next

GNU bug tracking system
Copyright (C) 1999 Darren O. Benham, 1997,2003 nCipher Corporation Ltd, 1994-97 Ian Jackson.