The way I'm using
> KLEE is by directly inputting a .ll file (the one I originally shared). The
> only thing that comes to my mind is setting the *optnone* attribute. In
> other words, how would you make sure that KLEE doesn't optimize feasible
> paths?
>
> Kind regards,
> Manuel
int me at that work?
I am particularly interested in how to write a test harness that directly
invokes functions in the drivers because the most obvious approach of using
a usermode test program to invoke KLEE on the entire kernel is...
unappealing.
--
Alastair Reid
ps The bits that I know how
With the workshop fast approaching, I have been waiting for registration to
open (and wondering if the workshop is only open to those presenting).
https://srg.doc.ic.ac.uk/klee21/registration.html
--
Alastair
___
klee-dev mailing list
I am trying to chase down a bug that occurs while applying KLEE to a
multi-module Rust program (assembly.ll is approx 200k lines).
I'm hoping for suggestions of what might be wrong and/or how to narrow down
the cause of the bug.
What I am seeing in the stack trace is
that
Hi KLEE-devs,
A quick update on where we got to with Rust verification over at Google
- We am able to compile/link most Rust programs to generate LLVM bitcode.
(The main obstacle at the moment is crates that include C code.)
- We can run KLEE on that bitcode directly
Details:
hich
> > tries to lift mostly memory barriers into LLVM intrinsics that are
> > handles as NOPs. More complex things are hard to handle.
> > (
> https://github.com/klee/klee/blob/088fc21e12c9675161172899be5ef5051f1ae96b/lib/Module/RaiseAsm.cpp
> )
> >
> > Hope that
t to check which is
preferred and there are a few possible variants (sketched at the end)
--
Alastair Reid
ps Here is the change. It ignores all intrinsics on the above list during
the Cleaner pass (but still reports an error if it hits them during
execution).
The main goal of this code is to avo
that pretends to support a single thread.
I'm guessing that a dummy library would mostly consist of a bunch of
functions that return constant values because there is only one thread, no
lock contention, etc.
And I'm also guessing that somebody has already implemented such a library.
--
Alastair Reid
ps
Is there a function that I can use in a program to distinguish between
running under KLEE and replaying a ktest using libkleeRuntest?
The reason that I want this is so that my test harness can print symbolic
values when replaying with concrete values but does not do so when running
under KLEE.
