Hi, there is some documentation for ZESTI at
https://srg.doc.ic.ac.uk/projects/zesti/. Unfortunately, the project is
not maintained anymore.
Best,
Cristian
On 14/12/2016 12:46, Papapanagiotakis-Bousy, Iason wrote:
Hi Thuan,
Thank you for pointing me to those two tools. Are you aware if there is
any documentation for ZESTI ?
Regards,
Jason
------------------------------------------------------------------------
*From:* thuanpv....@gmail.com <thuanpv....@gmail.com> on behalf of Thuan
Pham <thua...@comp.nus.edu.sg>
*Sent:* 14 December 2016 10:23:41
*To:* Papapanagiotakis-Bousy, Iason
*Cc:* klee-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 S2E. For seed mode in KLEE,
you need somehow convert your concrete input to a .ktest file so KLEE
can read it.
The two approaches you tried should not work. First approach will result
in a constraint Phi ^ (x==value) where Phi is the path constraints so
the result is always x=value as you got or unsatisfiable. The second one
also does not work because by writing a concrete value to a symbolic
variable, you will write concrete value to the memory area allocated for
this variable in the symbolic memory model of KLEE -> that memory area
will not be symbolic anymore, it is concrete.
Hope it will helps,
Thuan
On Mon, Dec 12, 2016 at 8:33 PM, Papapanagiotakis-Bousy, Iason
<iason.papapanagiotakis-bousy...@ucl.ac.uk
<mailto:iason.papapanagiotakis-bousy...@ucl.ac.uk>> wrote:
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
program) and execute the program in KLEE with that value and record
the symbolic constraints encountered.
I've tried the following two approaches:
1) using klee_assume(x==the_value_of_my_choice)
this does not seem to work as the only constraint that is generated
in kquery is the one I've given to klee_assume.
2) assigning a value to the symbolic variable
int x;
klee_make_symbolic(&x, sizeof(x), "x");
x=the_value_of_my_choice
this does not seem to work either as the resulting kquery file has
an empty query "(query [] false)".
How could I pick the value used during concolic execution and get
the symbolic constraints?
Thank you in advance for your suggestions.
Best regards,
Jason
_______________________________________________
klee-dev mailing list
klee-dev@imperial.ac.uk <mailto:klee-dev@imperial.ac.uk>
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
<https://mailman.ic.ac.uk/mailman/listinfo/klee-dev>
_______________________________________________
klee-dev mailing list
klee-dev@imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
_______________________________________________
klee-dev mailing list
klee-dev@imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
