The answer is indeed yes to both questions. Regarding the origin of the term 'counterexample', it's likely related to the fact that a that a solution from KLEE's point of view is a counterexample from STP's point of view (because STP decides validity while KLEE looks for satisfiability).
Paul On 12 Jan 2014, at 02:51, Lei Zhang <[email protected]> wrote: > Hi All, > > I am reading KLEE's source code in order to add some functionalities for it. > After struggling with the details for a long time, I still have difficulties > with the following questions. Can somebody shed light on it? Any explanation > will be highly appreciated. Thanks! > > 1) Lots of places use "counter example (cex)" as parts of the names. For me, > counter examples mean instances that disprove a statement. However, from my > understanding of the code, couter examples just mean "some assignments that > satisfy a set of constraints" or "no solution", which is quite the opposite. > If this is actually the case, why is the misleading "counter example" used? > Maybe it is better to change it? > > Besides, klee_prefer_cex() only gives "preference" of the argument constraint > without forcing it (meaning test cases violate the constraint can also be > generated), while klee_assume() forces the argument constraint to be true. Is > this right? > > 2) If I first klee_make_symbolic() a large range of memory, and then doing > lots of pointer calculation and klee_assume(), will this actually enforce the > constraints on the underlying memory? For example, for the following code, > > struct A { > int f1; // 4 bytes > bool f2; // 1 byte > bool f3[10]; // 10 bytes > }; > > void *f = malloc(1000); > klee_make_symbolic(f, sizeof(f)); > struct A *p1 = (struct A *) f; > klee_assume(p1->f2 == 0); > // will this make the 5th byte of f to be 0? > struct A *p2 = (struct A *) ( (char *) f + sizeof(struct A) + 3 ); > klee_assume(p2->f3[0] == 1); > // will this make the (15 + 3 + 6)th byte of f to be 1? > > By working through how the code handles the statements, I think the answer to > the above question are both yes. But my code just does not behave as I > expected. So I just need to double check my understanding. > > Thanks in advance! > > -- > Best regards, > Lei Zhang > _______________________________________________ > klee-dev mailing list > [email protected] > https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
_______________________________________________ klee-dev mailing list [email protected] https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
