You can break this down into two steps:
1. Figure out what the Expr for your constraint looks like
2. Figure out how to build that constraint
For 1, the easiest thing is to create a simple program that uses
klee_print_expr on your expression then run the program through klee.
For example
int main() {
int i = 0;
char buf[10];
klee_make_symbolic(&buf, sizeof(buf), "buf");
klee_print_expr("buf[i] != 0", buf[i] != 0);
return 0;
}
prints
buf[i] != 0:(ZExt w32 (Eq false
(Eq 0 (Read w8 0 buf))))
if you also make i symbolic you get
buf[i] != 0:(ZExt w32 (Eq false
(Eq 0
(Read w8 (Extract w32 0 (SExt w64 (ReadLSB w32 0 i)))
buf))))
For 2, there's no quick solution, just farmiliarize yourself with the
Expr API. include/klee/Expr.h is a good starting point
Paul
On 15/01/14 06:38, 李永超 wrote:
Hi,
I am reading KLEE source code recently to add some functionality to it.
Now I am confused about the constructing of constraints. As far as I
know about
KLEE implementation, constraints are essentially represented by /Expr/.
But this
is still not clear enough, say, consider I want to represent a
constraint like
/'buf[i] != 0'/, where /buf/ is an array of char and /i/ is an integer.
How should I construct
an /Expr/ so that I can add this constraint to current path constraints?
Thanks,
Yongchao.
_______________________________________________
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
