Error when trying to show the trace

[Tarciana Dias da Silva]

Hi everybody,

When i set the line below in my .jpf file:

report.console.property_violation=error,trace

It shows me the following errors:

gov.nasa.jpf.jvm.choice.ThreadChoiceFromSet {id:"<root>" ,1/1,isCascaded:false}

[SEVERE] JPF exception, terminating: exception during propertyViolated() notification

java.lang.NullPointerException

at java.util.Hashtable.get(Unknown Source)

at gov.nasa.jpf.util.Source.getSource(Source.java:250)

at gov.nasa.jpf.jvm.Step.getLineString(Step.java:64)

at gov.nasa.jpf.report.ConsolePublisher.publishTrace(ConsolePublisher.java:280)

at gov.nasa.jpf.report.Publisher.publishPropertyViolation(Publisher.java:297)

at gov.nasa.jpf.report.Reporter.publishPropertyViolation(Reporter.java:208)

at gov.nasa.jpf.report.Reporter.propertyViolated(Reporter.java:242)

at gov.nasa.jpf.search.Search.notifyPropertyViolated(Search.java:478)

at gov.nasa.jpf.search.DFSearch.search(DFSearch.java:83)

at gov.nasa.jpf.JPF.run(JPF.java:618)

at gov.nasa.jpf.JPF.start(JPF.java:190)

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:100)

---------------------- JPF error stack trace ---------------------

gov.nasa.jpf.JPFListenerException: exception during propertyViolated() notification

at gov.nasa.jpf.search.Search.notifyPropertyViolated(Search.java:481)

at gov.nasa.jpf.search.DFSearch.search(DFSearch.java:83)

at gov.nasa.jpf.JPF.run(JPF.java:618)

at gov.nasa.jpf.JPF.start(JPF.java:190)

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:100)

Caused by: java.lang.NullPointerException

at java.util.Hashtable.get(Unknown Source)

at gov.nasa.jpf.util.Source.getSource(Source.java:250)

at gov.nasa.jpf.jvm.Step.getLineString(Step.java:64)

at gov.nasa.jpf.report.ConsolePublisher.publishTrace(ConsolePublisher.java:280)

at gov.nasa.jpf.report.Publisher.publishPropertyViolation(Publisher.java:297)

at gov.nasa.jpf.report.Reporter.publishPropertyViolation(Reporter.java:208)

at gov.nasa.jpf.report.Reporter.propertyViolated(Reporter.java:242)

at gov.nasa.jpf.search.Search.notifyPropertyViolated(Search.java:478)

... 9 more

Does anybody have any idea?

--
Tarciana

[Tarciana Dias da Silva]

i have already re-built the jpf-core project but it is still not working... Please, i need some help!

--
Tarciana

[Peter Mehlitz]

this was a missing check for synthetic methods in error traces, which was fixed in r673 (02/24)

-- Peter

On Mar 1, 2012, at 7:43 PM, Tarciana Dias da Silva wrote:

> Hi everybody,
> When i set the line below in my .jpf file:
> report.console.property_violation=error,trace
>
> It shows me the following errors:
> gov.nasa.jpf.jvm.choice.ThreadChoiceFromSet {id:"<root>" ,1/1,isCascaded:false}
> [SEVERE] JPF exception, terminating: exception during propertyViolated() notification
> java.lang.NullPointerException
> at java.util.Hashtable.get(Unknown Source)
> at gov.nasa.jpf.util.Source.getSource(Source.java:250)
> at gov.nasa.jpf.jvm.Step.getLineString(Step.java:64)
> at gov.nasa.jpf.report.ConsolePublisher.publishTrace(ConsolePublisher.java:280)
> at gov.nasa.jpf.report.Publisher.publishPropertyViolation(Publisher.java:297)

...