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
[email protected]
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
