[klee-dev] Write to symbolic position

[Weiqi Wang]

Hi,

I’m wondering whether klee generate constraints when a concrete value is written to symbolic position? I tried a toy program and it seemed klee doesn’t. Specifically, I added a `buf[1] = ‘9’ before the password check in check_password(). But I only get constraint: (Eq 104 (Read w8 0 A-data)) due to short-circuit evaluation. What I would like to see are two constriants: (Eq 104 (Read w8 0 A-data)) and (Eq 57 (Read w8 1 A-data))

Is there an easy way to add this feature? Could you give me some hint on which file to modify?

Best,
Weiqi
-------------- next part --------------
HTML attachment scrubbed and removed