[klee-dev] Questions about cex and klee_assume()

[Paul Marinescu]

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 <antiagainst at gmail.com> 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
> klee-dev at imperial.ac.uk
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev

-------------- next part --------------
HTML attachment scrubbed and removed