[asm] Re: Re: call for help

[Sai Zhang <szhang@xxxxxxxxxxxxxxxxx>]

Zhongxian is right. but you need to notice that JPF only support primitive types for symbolic execution. 

String, and other Object types are not supported yet (as far as I know)

Best

-Sai

2010/7/9 Zhongxian Gu <zgu@xxxxxxxxxxx>

Hi,

If you want a symbolic execution framework for java, I suggest you to take a look at Java Path Finder.

Best

Zhongxian

2010/7/9 yiqiuping1986 <yiqiuping1986@xxxxxxx>

Hi, everybody,

  

   I am a newer for ASM. Several days ago when I looked for a tool

help me do symbolic execution on Java program, I found ASM. Then I 

began to learn it through asm-guide. But after several days, I got 

some confused whether it can help me. 

   I want ASM to implement that every time when I give an input to a 

java program, ASM execut the program symbolic, and return a path 

contraint representing the execution path. Then I will add the contraints 

in the path contraint to a solver, and let the solver give me another 

solution which must lead to a different path in the program.

For example, for the next simple exampe:

 

public class myclass {

public static void main(string[] args) {

int solutions = args[1];

 

           while （solutions）{

int [2] a = solutionFromSolver();

pathConstraint = ASM_symbolicExecution(program, a);

 

                addContraintsToSolver()；

solution --;

}

    

public int program(int a, int b) {

if (a[0]>10)

if (a[1] < 5)

return 1;

      else return 2;

else if (a[1] >= 5)

      return 3;

 

return 4;

}

}

}

So when a = {7, 8}, then I want to give the path contraint, 

pc = {X0 <= 10, X1 >= 5}(X0 and X1 are the symbolic value of 

a[0] and a[1]).  So could sombody tell whether ASM can return 

me a path contraint after a symboic execution? If it can, which 

part I shoulde pay close attention on in the asm-guid.pdf？

   Thank you very much.

   Best regards to you all~

 

2010-07-09

---

yiqiuping1986

 

2010-07-09

---

yiqiuping1986

--
You receive this message as a subscriber of the asm@xxxxxxx mailing list.
To unsubscribe: mailto:asm-unsubscribe@xxxxxxx
For general help: mailto:sympa@xxxxxxx?subject=help
OW2 mailing lists service home page: http://www.ow2.org/wws

14.7/5.0
This incoming message has been identified by the UCD central filters as
possible spam.  This attachment is provided so that you can review the
reasons the message was tagged, and to assist with additional filtering
if you wish to supplement the central filters with your own local rules.

If you have further questions please email ithelp@xxxxxxxxxxx for
assistance.

Content analysis details:   (14.7 points, 5.0 required)

 pts rule name              description
---- ---------------------- --------------------------------------------------
 4.1 BAYES_99               BODY: Bayesian spam probability is 99 to 100%
                           [score: 0.9999]
 3.5 RCVD_IN_UCDXBL         RBL: Appears in XBL
                           [124.16.139.196 listed in xbl.ucdavis.edu]
 0.7 SPF_NEUTRAL            SPF: sender does not match SPF record (neutral)
 2.9 FRT_SYMBOL             BODY: ReplaceTags: Symbol
 1.7 TVD_FUZZY_SYMBOL       BODY: TVD_FUZZY_SYMBOL
 0.0 HTML_MESSAGE           BODY: HTML included in message
 1.8 MIME_BASE64_TEXT       RAW: Message text disguised using base64 encoding

--
Zhongxian Gu
http://wwwcsif.cs.ucdavis.edu/~gu/
Ph.D. Student in Computer Science, UC Davis
2249 Kemper Hall


--
You receive this message as a subscriber of the asm@xxxxxxx mailing list.
To unsubscribe: mailto:asm-unsubscribe@xxxxxxx
For general help: mailto:sympa@xxxxxxx?subject=help
OW2 mailing lists service home page: http://www.ow2.org/wws