Hi Weiqi,
Note that such an assignment does not impose any constraints on the
input, which is why you don't see them in the path constraints
(otherwise a simple code snippet such as buf[1] = '9'; buf[2] = '0'
would be considered infeasible). You might want to check the initial
KLEE paper
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
