[klee-dev] Zesti: Making a particular instruction as sensitive

[Sandeep Dasgupta]

Hello Sir,

Currently I am working on Zesti to solve a problem which is similar to 
one described below.

I have a static analysis which could figure out what all things a could 
get assigned in the following code segment.

if(...) {
     a = 1;
} else {
     if(...) {
         a = 2;
     } else {
         a = 3;
     }
}

Now the static analyzer will put the following  test and expect the 
symbolic engine to explore all possible paths
that can assign to a and make the following condition true. If there is 
a bug in the analyzer and hence cannot interpret the
disjuncts correctly then the abort will get hit.

*if(a == 1 || a == 2 || a == 3) {*
     // I am OK
} else {
     abort;
}

Here my goal is to make the bolded statement sensitive so that zesti can 
explore all the alternative paths reaching that statement.
The challenge is there could be many similar conditional statement and i 
have to deliberately make the bolded one as sensitive. Can you suggest 
me ways of doing that.



-- 
*With Thanks and Regards,*
Sandeep Dasgupta
-------------- next part --------------
HTML attachment scrubbed and removed