[klee-dev] Constructing constraints

[李永超]

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.
-------------- next part --------------
HTML attachment scrubbed and removed