SymbolicPathFinder / jpf-symbc

Symbolic PathFinder
https://github.com/SymbolicPathFinder/jpf-symbc
124 stars 89 forks source link

Can SPF support test case generation for string input? #77

Open Minjuner-97 opened 2 years ago

Minjuner-97 commented 2 years ago

Hello~ In order to generate test case ,in progress jpf-symbc, I run the jpf : strings.HelloWorld.jpf. In results, I can't get the test case ,but only search start. So, can SPF support test case generation for string input? the output as follows:

[WARNING] unknown classpath element: /home/zhou/PROJECTS/tmp/jpf2/jpf-core/build/jpf-classes.jar Running Symbolic PathFinder ... symbolic.dp=choco symbolic.string_dp_timeout_ms=3000 symbolic.string_dp=abc symbolic.choco_time_bound=30000 symbolic.max_pc_length=2147483647 symbolic.max_pc_msec=0 symbolic.bvlength=32 symbolic.min_int=-2147483648 symbolic.min_long=-9223372036854775808 symbolic.min_short=-32768 symbolic.min_byte=-128 symbolic.min_char=0 symbolic.max_int=2147483647 symbolic.max_long=9223372036854775807 symbolic.max_short=32767 symbolic.max_byte=127 symbolic.max_char=65535 symbolic.min_double=4.9E-324 symbolic.max_double=1.7976931348623157E308 JavaPathfinder core system v8.0 - (C) 2005-2014 United States Government. All rights reserved.

====================================================== system under test strings.HelloWorld.main()

====================================================== search started: 8/10/22 5:25 AM null New sym int var_1_1_SYMSTRING.length min=-2147483648, max=2147483647

Warning: empty path condition

PCs: total:1 sat:1 unsat:0

string analysis: SPC # = 1 (var_1_1_SYMSTRING notequals CONST_Hello, World!) NPC constraint # = 0 string analysis: SPC # = 1 (var_1_1_SYMSTRING notequals CONST_Hello, World!) NPC constraint # = 0 *Summary*** PC is:constraint # = 0

Warning: empty path condition

PCs: total:2 sat:2 unsat:0

string analysis: SPC # = 1 (var_1_1_SYMSTRING equals CONST_Hello, World!) NPC constraint # = 0 Symbolic Exp [ var_1_1_SYMSTRING] string analysis: SPC # = 1 (var_1_1_SYMSTRING equals CONST_Hello, World!) NPC constraint # = 0 *Summary*** PC is:constraint # = 0

====================================================== Method Summaries Inputs: var_1_1_SYMSTRING No path conditions for strings.HelloWorld.hello(java.lang.String@15d)

====================================================== Method Summaries (HTML)

Test Cases Generated by Symbolic JavaPath Finder for strings.HelloWorld.hello (Path Coverage)

No path conditions for strings.HelloWorld.hello(java.lang.String@15d)

====================================================== results no errors detected

====================================================== statistics elapsed time: 00:00:00 states: new=3,visited=0,backtracked=3,end=2 search: maxDepth=2,constraints=0 choice generators: thread=1 (signal=0,lock=1,sharedRef=0,threadApi=0,reschedule=0), data=1 heap: new=354,released=22,maxLive=350,gcCycles=3 instructions: 3155 max memory: 234MB loaded code: classes=60,methods=1295

====================================================== search finished: 8/10/22 5:25 AM

Looking forward to your reply!