: [klee-dev] Choosing the concrete values and getting the
symbolic constraints
Hi Jason,
What you want can be achieved by using concolic execution or using seed
mode in KLEE. The default mode of KLEE is symbolic execution.
For concolic execution, you can try ZESTI or S2E. For seed mode in KLEE,
you
-dev@imperial.ac.uk
Subject: Re: [klee-dev] Choosing the concrete values and getting the symbolic
constraints
Hi Jason,
What you want can be achieved by using concolic execution or using seed mode in
KLEE. The default mode of KLEE is symbolic execution.
For concolic execution, you can try ZESTI or
Hi Jason,
What you want can be achieved by using concolic execution or using seed
mode in KLEE. The default mode of KLEE is symbolic execution.
For concolic execution, you can try ZESTI or S2E. For seed mode in KLEE,
you need somehow convert your concrete input to a .ktest file so KLEE can
read it.
In Executor::getSymbolicSolution function, klee solves the constraints
along a path to generate a representative concrete value for each symbolic
variable.
If you want to get a concrete value at any program point, you can call that
function to grab one for the already visited constraints in current
Hi everyone,
I would like to know how could I specify the concrete values chosen by KLEE to
execute.
Instead of the normal mode of KLEE I would like to be able to choose a value (I
am interested only in integers and assume for simplification that there is only
one symbolic variable in the pro
