rajen@edsel.ece.cmu.edu (Ramchandani Rajen Sham) (05/11/91)
I am looking for any code that will enable me to perform symbolic simulation/ abstract execution of any high level procedural language, like pascal or or C . It would be nice if it has the capability of resolving brach conditions whenever possible. Or on the other hand if you have some program that is capable of deciding if a statement is true or false depending on the conditions it has seen so far i would like to hear from you. what is mean is: given the following hypothetical code fragment sum = 0; loop read ( x, y); -(1) if x > 2 then sum = sum + x - 2 else sum = sum + x ; -(2) if y > x && y > 2 then sum = sum + y - 2 else sum = sum + y; -(3) end loop the executer would trace a path thus PC(1): input x1, y1; PC(2): ( x1 > 2 AND sum = x1 - 2 ) OR (x1 <= 2 AND sum = x1) PC(3): ( x1 > 2 AND sum = x1 - 2) AND (y1 > x1 && y1 > 2 AND sum = sum + y1 -2 ) pruned to ( x1 > 2 AND y1 > x1 AND sum = x1 + y1 -4) by the resolver [ i.e it was able to deduce that y1 >2 was redundant] OR ( ...............................) The last thing on this wish list of mine is if you have some program that generates input data values to satisfy a given set of conditions, will be equalities, inequalities and contain boolean operations. If you have any pointers to similar work being done elsewhere i could like to hear from you. Thanks a lot Please email responses to rajen@edsel.ece.cmu.edu