Hi Luke,
As KLEE builds on LLVM, the value is either part of an SSA register or a
heap/global allocation.
In the first case, the register’s value can be accessed via `eval()`, i.e.
for a Load instruction
visitor in the Expr hierarchy, or something similar, but could not find it.
>
> Thanks again,
> Oleg
>
> On 12/12/23 05:42, Nowack, Martin wrote:
>> Hi Haozhi Fan,
>>
>> The symbolic names are generated using the call `klee_make_symbolic`
>> indirectly or directly in
Hi Yukai Zhao,
Can you provide the output of your KLEE run?
My guess is that `max`, `min` are treated as external functions that forces a
and b to be concretised, i.e. which leads to only one path being generated.
But let’s have a look at your output to confirm this.
Best,
Martin
> On 12. Dec
Hi Haozhi Fan,
The symbolic names are generated using the call `klee_make_symbolic` indirectly
or directly in your software under test.
KLEE tracks the memory object that have been associated with these calls
Hi Dennis,
KLEE currently doesn’t support newer LLVM versions than 14.
We are working on this but it’s not in a stage for upstreaming it yet.
Unfortunately you have to stick with LLVM 14 in this case.
Best,
Martin
> On 1. Oct 2023, at 11:23, Dennis Luehring wrote:
>
> Standard Clang 17.0.1
Hi Alex,
The remaining patches are not submitted yet and need some cleaning.
But in a nutshell, `-tc-type` is set based on type of goal the test has: bug
finding vs. coverage.
They are slightly different in both cases, please refer to the TestComp
documentation (categories).
Hi Dan,
We are always looking for contributors and contributions ;)
A good starting point for KLEE development is:
https://klee.github.io/docs/developers-guide/
>From a technical perspective, it is not trivial but not too hard either.
The main function you are interested in is
hank you.
> Best regards,
> Delphine
>
>> -Message d'origine-
>> De : Nowack, Martin
>> Envoyé : mardi 25 avril 2023 15:59
>> À : LONGUET Delphine
>> Cc : klee-dev
>> Objet : Re: [klee-dev] Symbolic calls to mqueue.h functions ?
>>
>>
Hi,
> On 24. Apr 2023, at 10:53, LONGUET Delphine
> wrote:
>
>
> I am trying to execute Klee on a code using mqueue.h and despite the
> -posix-runtime and -libc=uclibc options, functions mq_open, mq_close, etc,
> remain "undefined references". I can see that there actually are
>
Hi Tareq,
I can highly recommend you the following documents to get an understanding of
the internal details of debug information and LLVM that KLEE uses in the first
place:
* https://llvm.org/docs/SourceLevelDebugging.html
* https://llvm.org/docs/HowToUpdateDebugInfo.html
For the examples
Hi David,
Have a look at https://klee.github.io/publications for a multitude of use cases
that KLEE has been used successfully:
That said, the larger your application is the more challenging it becomes to
test it with any method.
In those cases it becomes useful to test parts of the
Hi all,
A quick reminder: the early registration deadline is approaching fast -
tomorrow, 10th August.
Looking forward to welcome you in person.
The KLEE 2022 Organisers
> On 29. Jul 2022, at 16:00, Nowack, Martin wrote:
>
> Hi all,
>
> We are delighted to host this Se
Hi all,
We are delighted to host this September the 3rd International KLEE Workshop on
Symbolic Execution at Imperial:
3rd International KLEE Workshop on Symbolic Execution
15–16 September 2022 • London, UK and Online
https://srg.doc.ic.ac.uk/klee22/
In-person registration is now open
includes libc++, I am not sure if this proves that I am using this
> library correctly?
>
> -- 原始邮件 --
> 发件人: "Nowack, Martin" ;
> 发送时间: 2022年6月21日(星期二) 晚上11:09
> 收件人: "房合钧"<1106929...@qq.com>;
> 抄送: "klee-dev";
guess. Depending on where exactly you insert the call, by any chance is
the call executed multiple times?
(Maybe cross-check it with a dirty but useful `llvm::errs() << “shm_open has
been called\n”;` or `klee_warning(“...")`)
Best,
Martin
Best wishes,
Chaoqi
On Jun 27, 2022, at 22:1
Hi Chaoqi,
Can you clarify: Do you want to test software that uses `shm_*` or do you want
communicate with the KLEE process itself?
KLEE should not modify any `shm` allocated objects.
The only unintended modification that could happen is if your tested
application uses external function calls
Hi,
One issue could be that during compilation the wrong include files are used.
Make sure you use the include files provided with libc++ implementation you use
for KLEE.
Please refer to the following documentation to get further information:
Hi Mario,
On 20. Jun 2022, at 18:44, Mario García Pérez
mailto:mgarc...@gmail.com>> wrote:
Hi,
I'm using klee with gnat-llvm generated bytecodes (to execute symbolically Ada
programs) and I have some problems.
When executing the program there are done some runtime checks, that are done by
Hi Marco,
Maybe the following helps you:
https://github.com/klee/klee/blob/292600cf54d5fd73278f67a4f98c2f955cbdaa10/test/Feature/DefineFixedObject.c
Best,
Martin
On 16. Jun 2022, at 20:43, Carrasco, Manuel G
mailto:m.carra...@imperial.ac.uk>> wrote:
Hi Marco!
I have a program that when
https://github.com/NixOS/nixpkgs/blob/3ddd960a3b575bf3230d0e59f42614b71f9e0db9/pkgs/build-support/cc-wrapper/default.nix#L338
Best,
Martin
Morgan
On Tue, Jan 11, 2022 at 2:30 AM Nowack, Martin
mailto:m.now...@imperial.ac.uk>> wrote:
Hi Morgan,
Just looked at the build instruct
Hi Morgan,
Just looked at the build instructions:
https://github.com/NixOS/nixpkgs/blob/master/pkgs/applications/science/logic/klee/default.nix#L53
"-DKLEE_RUNTIME_BUILD_TYPE=${buildType}"
I would recommend to handle the build type for the `KLEE_RUNTIME_BUILD_TYPE`
separate from the
Hi Jeroen,
Thank you very much for this question.
The problem is mainly a time issue. Somebody needs to port the changes to the
newer version of KLEE,
adds test cases and open a PR. Another aspect to keep in mind are potential
license issues.
>From an engineering perspective, nothing should be
Hi Alastair,
On 28. Jun 2021, at 15:02, Alastair Reid
mailto:adr...@google.com>> wrote:
Hi,
Instruction does not dominate all uses!
%.i0385 = phi i64 [ , ], [ %.i0664, %2236 ], [ %.i0381,
%2227 ], !dbg !30427
%.upto04194 = insertelement <4 x i64> undef, i64 %.i0385, i32 0
This looks
't fix the mentioned issue which is
printf("%s%s%n\n", , , ).
Please notice that it is %s that determines whether a or b is zero or not.
Thank you all the same!
Best,
Mingyi
________
From: Nowack, Martin mailto:m.now...@imperial.ac.uk>>
Sent: Tuesday, May 11
Hi Manuel, hi Alastair,
Currently, KLEE runs still the `CFGSimplificationPass` even with `—optimize`
off.
https://github.com/klee/klee/blob/24badb5bf17ff586dc3f1856901f27210713b2ac/lib/Module/KModule.cpp#L288
This might be not necessary anymore for recent LLVM versions.
The best way forward
Hi Mingyi,
You’ve hit a bug in KLEE.
Thanks for your detailed description - I just opened PR based on your test case
https://github.com/klee/klee/pull/1407 that fixes the issue.
Feel free to apply those changes locally to try them out.
The test case is based on your example and works with the
Hi Russell,
There are currently two examples in the repository already:
https://github.com/klee/klee/tree/master/utils/data/Queries
Those examples use KLEE’s kquery languages.
In general this is quite application specific and what might have been harder
queries 4 years ago might be super fast
Hi,
There are a couple of missing features.
Can you open an issue https://github.com/klee/klee/issues ? we can continue the
discussion there.
Best,
Martin
On 15. Dec 2020, at 13:41, JingXiaoni
mailto:jingxia...@icloud.com>> wrote:
Hi all,
l have some problems
on using klee,need your help
Hi Alastair,
I would also rather use option 3.
Normally, the `LowerIntrinsic` pass should try to replace appropriate calls if
possible. It should not terminate it.
Beside your attached code, I would suggest to change the following code line in
`lib/Core/Executor.cpp`:
Hi Xuan,
I’m sorry for the very late reply.
The problem you are describing is the following:
The files you’re compiling, e.g. from `get_sign.c` do contain calls, which KLEE
handles internally (i.e. `klee_make_symbolic`):
```
...
int main() {
int a;
klee_make_symbolic(, sizeof(a), "a");
Hi,
On 11.12.19 13:43, Nani Hutagaol wrote:
>
> 2. I had read some email from
> https://www.mail-archive.com/klee-dev@imperial.ac.uk/. Until now, all the
> question just discuss about numerical program. Then, I also read some
> publication paper from https://klee.github.io/publications/, but all
Hi,
Please have a look at the following discussion:
https://github.com/klee/klee/pull/70
Thinks have changed upstream. It could be worth to reconsider it.
Best,
Martin
On 22.11.19 07:23, Gleb Popov wrote:
Hello.
I'm working on adding support for following module-level inline asm in KLEE:
2019 at 2:20 PM Nowack, Martin
mailto:m.now...@imperial.ac.uk>> wrote:
Hi Gleb,
There are two major building blocks:
First, the built libc does *not* contain library calls that are intercepted by
the POSIX layer.
It’s on my list to eventually change this. Most of the patches in klee-uclibc
Hi Gleb,
There are two major building blocks:
First, the built libc does *not* contain library calls that are intercepted by
the POSIX layer.
It’s on my list to eventually change this. Most of the patches in klee-uclibc
just comment out those functions or redirect internally used function
Hi,
In your case, use the `ConstantExpr::alloc()` method that takes an
`llvm::APInt` as argument.
There are several `APInt` constructors that allow to create arbitrary
signed/unsigned integers (e.g.
http://llvm.org/doxygen/classllvm_1_1APInt.html#a6286f2ba84c5ad11f4a90d57cb1dd293).
Best,
Dear Wei Ma,
Could you please summarise and provide a few details how the other symbolic
execution engine is used?
This should help people to answer if this is possible with KLEE.
All the best,
Martin
On 31. Aug 2019, at 15:24, Wei MA mailto:wei...@uni.lu>> wrote:
Dear All,
Recently, I
Hi,
Currently, only queries can be printed.
Extend your code to create an empty constraint set and use the expression
(arguments[0]) as an argument:
```
std::vector> emptyCS;
ConstraintManager emptyCM(emptyCS);
Query query(emptyCM, arguments[0]);
```
Hope that helps.
Cheers,
Martin
On
Hi Qiao,
Currently, there is no direct support for this.
But, to hack it - under the assumption you don’t need the coverage-guided
searcher - you can modify the `StatsTracker::computeReachableUncovered`
function
For most LLVM tools, it should be '-v'. Just to cross check.
On 15 August 2019 11:25:34 CEST, "Zhang, RongX Z"
wrote:
Sorry, how to check this? /usr/local/bin/llvm* is installed by myself, and I
thinks it’s llvm 6.0.
From: Nowack, Martin [mailto:m.now...@imperial.ac.uk]
Sent
Can you check which LLVM version usr/local/bin/llvm-dis uses?
Cheers,
Martin
On 15 August 2019 11:12:02 CEST, "Zhang, RongX Z"
wrote:
Yes, clang is in my PATH and clang version is 6.0.0.
Thanks
Rong
From: Nowack, Martin [mailto:m.now...@imperial.ac.uk]
Sent: Thursday, August 15, 20
Dear Rong,
Can you check if clang is in your PATH?
'clang -v' should print out 6.0 as well.
Clang is not necessarily installed as a dependency of LLVM.
Hope that helps.
Best,
Martin
On 15 August 2019 09:26:23 CEST, "Zhang, RongX Z"
wrote:
Hi ,
I am installing KLEE on Clear Linux, when I
Hi,
There are a couple of options to drive KLEE. First, use
`-only-output-states-covering-new`, this only generates test cases which are
covering new instructions.
Otherwise every path through an application found by KLEE will have a test case
generated even though it doesn’t cover new
Hi Alberto,
The function `selectState()` returns the state you would like KLEE to work on
next.
So this is always only one state maximum.
The update function is KLEE’s callback to your searcher to inform you which
states have been added or removed.
But, you should not make any assumption on
43 matches
Mail list logo
