Re: [klee-dev] KLEE SMT query overhead

> > Are we talking about "orders of magnitude" in the milli/micro-second > range or about really expensive queries? Expensive. If it helps, I ran klee for 5 hours on the most recent version of find with the following settings: klee --simplify-sym-indices --write-cvcs --write-cov --output-module

Re: [klee-dev] KLEE SMT query overhead

Hi, On Tue, 8 Mar 2022 13:58:57 -0500 William Leeson wrote: > I'm finding that the Elapsed time reported by KLEE in solver-queries.smt2 > for a single query is different from the time reported by the solver klee > is built on (stp_simple in the docker /tmp folder). Orders of magnitude >

Re: [klee-dev] Collect path constraints with seed mode

Hi, On 21/09/2021 09:00, zy j wrote: Hi, I want to collect the path constraints of a specific PoC generated by fuzzing, I have found similar question in https://www.mail-archive.com/klee-dev@imperial.ac.uk/msg02743.html ,

Re: [klee-dev] Need help in making a structure pointer symbolic

Hi, You can make pointers symbolic in KLEE, but this might not accomplish what you hope. Making a pointer symbolic means it can refer to any address in memory, including invalid ones. Best, Cristian On 04/03/2022 08:37, Sandip Ghosal wrote: Hello Everyone, Can somebody help me to make a

Re: [klee-dev] fork() : creating child processes in KLEE's execution

Hi, KLEE does not use the system call fork() to fork states. See Executor::fork() in the code. Best, Cristian On 23/02/2022 18:40, Pansilu Pitigalaarachchi wrote: Hi, I would like to check the possible scenarios where KLEE creates a child process. 1.My current understanding is that a

Re: [klee-dev] How should the function parameter be symbolised if the function parameter is a file type?

Hi, To use symbolic files, you should use KLEE's symbolic environment support. See https://klee.github.io/docs/options/#symbolic-environment and the tutorials for information on how KLEE supports symbolic files. Best wishes, Cristian On 18/01/2022 03:46, rongze xv wrote: Hi, I am

[klee-dev] KLEE SMT query overhead

Hello, I'm working on a project dealing with SMT solvers. We are collecting queries from KLEE using the latest klee docker image with the "--use-query-log=solver:smt2" flag on. We are then dividing this file into individual queries. We run several SMT solvers on these queries and collect the