[klee-dev] A need for a shared library in KLEE

s obsolete: https://github.com/klee/klee/issues/237 -- Regards, Marko Dimjašević . University of Utah https://dimjasevic.net/marko . PGP key ID: 1503F0AA Learn email self-defense! https://emailselfdefense.fsf.org signature.asc Description: This is a digitally signed me

Re: [klee-dev] A need for a shared library in KLEE

t really needed. If it is not needed, then that would save me the trouble of adding a SONAME attribute to the shared library, which is a must for Debian packages. -- Regards, Marko Dimjašević . University of Utah https://dimjasevic.net/marko . PGP key ID: 1503F0AA Learn e

Re: [klee-dev] A need for a shared library in KLEE

On Tue, 2016-02-23 at 13:25 -0700, Marko Dimjašević wrote: > I am aware of that. However, that still doesn't answer my question - > is > the shared version of the library needed? ... and let me answer my own question: it is needed. Cristian, as you pointed to the example, there is

[klee-dev] Doxygen documentation link not working

error. -- Regards, Marko Dimjašević . University of Utah https://dimjasevic.net/marko . PGP key ID: 1503F0AA Learn email self-defense! https://emailselfdefense.fsf.org signature.asc Description: This is a digitally signed message part ___ klee-d

[klee-dev] Implementing support for the Firehose file format

s would be implemented, that would be highly appreciated. -- Regards, Marko Dimjašević . University of Utah https://dimjasevic.net/marko . PGP key ID: 1503F0AA Learn email self-defense! https://emailselfdefense.fsf.org signature.asc Description: This is a digitally signed me

Re: [klee-dev] Implementing support for the Firehose file format

tructure for Debian. Debile expects analysis tools to produce results in the Firehose format. -- Regards, Marko Dimjašević . University of Utah https://dimjasevic.net/marko . PGP key ID: 1503F0AA Learn email self-defense! https://emailselfdefense.fsf.org signature.asc De

[klee-dev] KLEE unable to load a symbol

ing as I'm expecting it might be quite common for many other packages too. -- Regards, Marko Dimjašević . University of Utah https://dimjasevic.net/marko . PGP key ID: 1503F0AA Learn email self-defense! https://emailselfdefense.fsf.org signature.asc De

[klee-dev] Segmentation fault when testing Flex

ame $f).bc The .bc file flex.bc is available from: http://soarlab.org/files/klee/sut/flex-2.5.39/flex.bc -- Regards, Marko Dimjašević . University of Utah https://dimjasevic.net/marko . PGP key ID: 1503F0AA Learn email self-defense! https://emailselfdefense.fsf.org signature.asc D

Re: [klee-dev] KLEE unable to load a symbol

On Thu, 2016-05-26 at 15:30 -0600, Marko Dimjašević wrote: > For example, these files from the apt package have the same issue: > So I'd say the problem is quite common. I ran KLEE without making anything symbolic on over 30 Debian source packages and this really is a common problem.

Re: [klee-dev] KLEE unable to load a symbol

ke to understand them at some point too. -- Regards, Marko Dimjašević . University of Utah https://dimjasevic.net/marko . PGP key ID: 1503F0AA Learn email self-defense! https://emailselfdefense.fsf.org signature.asc Description: This is a

[klee-dev] Updating KLEE-uClibc to the most recent version of uClibc

n how to debug the issue with dc.bc above or on anything related, I would appreciate it. [1] https://github.com/klee/klee/issues/404#issuecomment-222302440 [2] https://github.com/klee/klee-uclibc [3] https://www.debian.org/ports/ -- Kind regards, Marko Dimjašević . University

[klee-dev] Writing tests for KLEE

ts directory. I see only 3 meaningful C++ files in there. Therefore, can you confirm this is how unit tests should be written for KLEE, or is the guide outdated? -- Regards, Marko Dimjašević . University of Utah https://dimjasevic.net/marko . PGP key ID: 1503F0AA Learn email self-

Re: [klee-dev] Writing tests for KLEE

7;Release+Asserts' directory when building, but it has no Makefile. Instead, I ran the 'make unittests' command from the root of the code base. Finally, I did look at /usr/lib/llvm-3.4/build/unittests/Makefile.unittest that is mentioned in the error message, but I can't figure

Re: [klee-dev] Writing tests for KLEE

is was in LLVM 3.4 and on Debian I have LLVM 3.4.2 installed, it is strange they haven't incorporated your fix. -- Regards, Marko Dimjašević . University of Utah https://dimjasevic.net/marko . PGP key ID: 1503F0AA Learn email self-defense! https://emailselfdefense.fsf.org

[klee-dev] Cloud9 and KLEE - POSIX features

be an outdated project, at least according to a commit history of its Git repository: https://github.com/dslab-epfl/cloud9 It would be nice to have these features in KLEE, but probably no one found time, energy, motivation, or all of it to make it happen. -- Regards, Marko Dimjašević . Uni

Re: [klee-dev] Cloud9 and KLEE - POSIX features

in KLEE would be a great thing to have! Therefore, I'm hoping someone will find time to merge your pull request, even though it's been a year since you submitted the request. -- Regards, Marko Dimjašević . University of Utah https://dimjasevic.net/marko . PGP key ID: 1503F0A

Re: [klee-dev] Implementing support for the Firehose file format

Hi KLEE developers, On Tue, 2016-05-10 at 21:12 -0600, Marko Dimjašević wrote: > I would like to implement support for the Firehose reporting file > format in KLEE: > > https://github.com/fedora-static-analysis/firehose I am close to being done with this one. One will simply add t

Re: [klee-dev] How to compile c/c++ project to a unique LLVM IR bitcode?

to be tested by klee? You can try with the Whole Program LLVM tool: https://github.com/travitch/whole-program-llvm -- Regards, Marko Dimjašević . University of Utah https://dimjasevic.net/marko . PGP key ID: 1503F0AA Learn email self-defense! https://emailselfdefense.fsf.org s

Re: [klee-dev] Implementing support for the Firehose file format

Hi again, On Sat, 2016-07-02 at 20:24 -0600, Marko Dimjašević wrote: > A thing that I would like to put in the output file is values of input > arguments to a program for a failing test case when the POSIX runtime > is used. Usually one calls the klee-replay tool for this. Is there a >

Re: [klee-dev] LibC recommendations? [Re: Updating KLEE-uClibc to the most recent version of uClibc]

. In case I get it running, that will be great. I'll also take a look at uClibc-ng. -- Regards, Marko Dimjašević . University of Utah https://dimjasevic.net/marko . PGP key ID: 1503F0AA Learn email self-defense! https://emailselfdefense.fsf.org signature.asc Descriptio

[klee-dev] Adding support for another C library

nctions from KLEE-uClibc get renamed, e.g. "__libc_open" gets renamed to "open"? Anything else? I'd appreciate any thoughts on this matter. -- Regards, Marko Dimjašević . University of Utah https://dimjasevic.net/marko . PGP key ID: 1503F0AA Learn email self-defense!

Re: [klee-dev] Adding support for another C library

Hi again, On Fri, 2016-10-14 at 19:51 -0600, Marko Dimjašević wrote: > Earlier on this list there was a thread on what would be alternatives > to > KLEE-uClibc as the library implementation got rather old, which is > true > for its upstream as well, though to a lesser extent. He

Re: [klee-dev] Adding support for another C library

e a libc.so.bc or libc.a.bc. Therefore, it makes difference against what LLVM IR library one links. In my particular case, I've been struggling with getting all important C library symbols included, such as __cp_begin, fini_array_start and fini_array_end, etc. -- Regards, Marko Dimj

[klee-dev] Inline assembly, concurrency

I could simply rewrite the a_cas_p function in C. I would lose atomicity, but my hunch is it doesn't really matter as KLEE can't work on concurrent code anyway. Do you see any pitfalls with this idea? Maybe other suggestions on how to handle situations in which inline assembly code ex