Thanks, Paul! In the example you given, a default rule can be added to
catch !(c==1) && !(c==2). But it is a waste to consider !(c==1) in the
(c==2) case since they can not be true at the same time.
Here is a longer version: I have a long list of if-statements. Each
statement contains a very complex expression. What I know is that at a
given time, only one of them can be true (think of it as a switch
statement). If I write it like this
if(rule<1>) {Do 1}
if(rule<2>)) {Do 2}
...
if(rule<n>)) {Do n}
{Do n+1}
The generated STP queries will be
1: (rule<1>)
2: (rule<2>))&&(!rule<1>)
...
n: (rule<n>)&&(!rule<1>)&&(!rule<2>)&&(!rule<3>)...&&(!rule<n-1>)
default: (!rule<1>)&&(!rule<2>)&&(!rule<3>)...&&(!rule<n-1>)&&(!rule<n>)
If fact, because they're mutually exclusive, hence no priority is implied.
The STP queries can be
1: (rule<1>)
2: (rule<2>)
...
n: (rule<n>)
default: (!rule<1>)&&(!rule<2>)&&(!rule<3>)...&&(!rule<n-1>)&&(!rule<n>)
The latter case will generate much shorter queries.
Regards,
James
On Tue, Jan 31, 2012 at 5:38 PM, Paul Marinescu <
[email protected]> wrote:
> Hi James,
> It doesn't seem like what you're trying to do is sound. Take this slightly
> modified example:
>
> #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");
> klee_assume(c == 1 || c == 2);
> f(c);
> }
>
> If you don't consider !(c==1), you'll end up saying that a path which
> doesn't print anything is feasible. Perhaps you need to explain in more
> detail what you want to do.
>
> Paul
>
> On 31 Jan 2012, at 02:06, James Hongyi Zeng wrote:
>
> > 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
>
>
_______________________________________________
klee-dev mailing list
[email protected]
http://keeda.Stanford.EDU/mailman/listinfo/klee-dev
