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
_______________________________________________ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
