Hi Alexandre,
Both cases essentially get compiled into the same LLVM code. When
evaluating the (c==2) branch, KLEE will put [(c==2) && !(c==1)] into the
query, whose 2nd construct is unnecessary since c==2 and c==1 are mutually
exclusive.
The problem is the plain if-else (and if) statement doesn't imply
mutually exclusiveness. For example
if(c<0){}
else if(c<10){}
else{}
c<0 and and c<10 are not mutually exclusive.
Regards,
James
On Tue, Jan 31, 2012 at 2:03 AM, Alexandre Gouraud <
[email protected]> wrote:
> Hello,
>
> I am not a KLEE expert at all, but I would never write such C code. Why
> not using either:
>
> if(c==1) {}
> else if (c==2) {}
> else {}
>
> or even better:
>
> switch (c)
> {
> case 1: {...;break;}
> case 2: {...;break;}
> default: {...;break;}
> }
>
> Wouldn't klee understand the cases are exclusive written this way ?
>
> AG.
>
> Le 31 janvier 2012 03:06, James Hongyi Zeng <[email protected]> a écrit
> :
>
>> Hi all,
>>
>> I am wondering whether I can explicitly tell KLEE that a set of
>> if-statements are mutually exclusive. In the following example, KLEE
>> generates 3 STP queries. Since c==2 and c==1 are mutually exclusive, I
>> would like klee not to include !(c==1) in c==2 STP query. Is it possible?
>>
>> Thanks,
>> James
>>
>> #include <klee/klee.h>
>>
>> void f(int c) {
>> if(c==1) {printf("Do A\n");}
>> if(c==2) {printf("Do B\n");}
>> }
>>
>> int main() {
>> int c;
>> klee_make_symbolic(&c, sizeof(c), "input");
>> f(c);
>> }
>>
>>
>>
>>
>> _______________________________________________
>> klee-dev mailing list
>> [email protected]
>> http://keeda.Stanford.EDU/mailman/listinfo/klee-dev
>>
>>
>
>
> --
> Alexandre
>
_______________________________________________
klee-dev mailing list
[email protected]
http://keeda.Stanford.EDU/mailman/listinfo/klee-dev
