Strings in JPF-symbc

[Pedro Louro]

Hi,

I´m working on a big project (https://services.txt.it/fastfix-
project/) that may use jpf-symbc but it will need to work with
strings.
What is the state of the development with the strings, and is there
any roadmap?

Best Regards
Pedro Louro

[Willem]

Strings should be finished in the very near future. Before end of July.

You can try it even now, but a better version will be done soon.

Bye,
Willem

--Sent from my iPad

[Gideon Redelinghuys]

Hi,

I've uploaded our new rewritten symbolic string execution engine last
week.

Symbolic string execution supports the operations:

equal
contains
startswith
endswith
trim
substring
indexOf
charAt
length
concat

The plan at the moment is to thoroughly test, debug and fix the
current source code. After that (around mid-September) I'll extend the
supported operations.

On Jul 13, 4:10 pm, Willem <wil...@gmail.com> wrote:
> Strings should be finished in the very near future. Before end of July.
>
> You can try it even now, but a better version will be done soon.
>
> Bye,
> Willem
>
> --Sent from my iPad
>

[Pedro Louro]

Hello,

Thanks for the responses. I´ve just checked out the jpf-core and jpf-
symb and tried the strings with a simple example. I don´t know if I´m
wrong but I noticed:
1. It doesnt work having a String parameter and a non String
parameter;
2. It doesnt seem that the String condition is solved to a TestCase.

Is there any problem with my testing or this ins´t yet working?

Best Regards
Pedro Louro

1:
java.lang.AssertionError
at gov.nasa.jpf.jvm.StackFrame.getLocalAttr(StackFrame.java:683)
at
gov.nasa.jpf.symbc.SymbolicListener.instructionExecuted(SymbolicListener.java:
261)
at gov.nasa.jpf.jvm.JVM.notifyInstructionExecuted(JVM.java:667)
at gov.nasa.jpf.jvm.ThreadInfo.executeInstruction(ThreadInfo.java:
2260)
at gov.nasa.jpf.jvm.ThreadInfo.executeTransition(ThreadInfo.java:
2211)
at
gov.nasa.jpf.jvm.SystemState.executeNextTransition(SystemState.java:
656)
at gov.nasa.jpf.jvm.JVM.forward(JVM.java:1694)
at gov.nasa.jpf.search.Search.forward(Search.java:487)
at gov.nasa.jpf.search.DFSearch.search(DFSearch.java:78)
at gov.nasa.jpf.JPF.run(JPF.java:534)
at gov.nasa.jpf.JPF.start(JPF.java:166)
at sun.reflect.NativeMethodAccessorImpl.invoke0(Native Method)
at sun.reflect.NativeMethodAccessorImpl.invoke(Unknown Source)
at sun.reflect.DelegatingMethodAccessorImpl.invoke(Unknown Source)
at java.lang.reflect.Method.invoke(Unknown Source)
at gov.nasa.jpf.tool.Run.call(Run.java:76)
at gov.nasa.jpf.tool.RunJPF.main(RunJPF.java:86)
---------------------- JPF error stack trace ---------------------
gov.nasa.jpf.JPFListenerException: exception during
instructionExecuted() notification
at gov.nasa.jpf.jvm.JVM.notifyInstructionExecuted(JVM.java:678)
at gov.nasa.jpf.jvm.ThreadInfo.executeInstruction(ThreadInfo.java:
2260)
at gov.nasa.jpf.jvm.ThreadInfo.executeTransition(ThreadInfo.java:
2211)
at
gov.nasa.jpf.jvm.SystemState.executeNextTransition(SystemState.java:
656)
at gov.nasa.jpf.jvm.JVM.forward(JVM.java:1694)
at gov.nasa.jpf.search.Search.forward(Search.java:487)
at gov.nasa.jpf.search.DFSearch.search(DFSearch.java:78)
at gov.nasa.jpf.JPF.run(JPF.java:534)
at gov.nasa.jpf.JPF.start(JPF.java:166)
at sun.reflect.NativeMethodAccessorImpl.invoke0(Native Method)
at sun.reflect.NativeMethodAccessorImpl.invoke(Unknown Source)
at sun.reflect.DelegatingMethodAccessorImpl.invoke(Unknown Source)
at java.lang.reflect.Method.invoke(Unknown Source)
at gov.nasa.jpf.tool.Run.call(Run.java:76)
at gov.nasa.jpf.tool.RunJPF.main(RunJPF.java:86)
Caused by: java.lang.AssertionError
at gov.nasa.jpf.jvm.StackFrame.getLocalAttr(StackFrame.java:683)
at
gov.nasa.jpf.symbc.SymbolicListener.instructionExecuted(SymbolicListener.java:
261)
at gov.nasa.jpf.jvm.JVM.notifyInstructionExecuted(JVM.java:667)
... 14 more

2:
****************************
PC # = 4
CONST_8 <= CONST_30 &&
CONST_8 >= CONST_1 &&
command_1_SYMSTRING[8] == CONST_8 &&
command_1_SYMSTRING[8] == Length_0_[8]
SPC # = 1
(command_1_SYMSTRING[engineOn] equals CONST_engineOn)
****************************

====================================================== Method
Summaries
Symbolic values: command_1_SYMSTRING[**UNDEFINED**]

handleCommand(don't care)



On 14 Jul, 12:17, Gideon Redelinghuys <gjredelingh...@gmail.com>
wrote: