Can't find bundle for base name org.apache.xerces.impl.msg.SAXMessages, locale en_US.

[edilton-santos]

Hi folks,

I'm trying to use JPF to analyze a running simulator called Adasim implemented in Java 8. I added all dependencies in jpf-core.classpath, but when I run JPF, I get this error message:

gov.nasa.jpf.vm.NoUncaughtExceptionsProperty
java.util.MissingResourceException: Can't find bundle for base name org.apache.xerces.impl.msg.SAXMessages, locale en_US.

Do you have some idea about this problem? Because the xercesImpl.jar is available in the JPF classpath, and the locale is en_US.
Below you can find the JPF log. Thank you.

parallels@ubuntu-linux-20-04-desktop:~/eclipse-workspace/adasim/src$ java -jar /home/parallels/eclipse-workspace/jpf/jpf-core/build/RunJPF.jar TrafficMain.jpf
JavaPathfinder core system v8.0 (rev 121f364) - (C) 2005-2014 United States Government. All rights reserved.

====================================================== system under test
TrafficMainRun.main()

====================================================== search started: 4/28/22 11:01 AM
Country: - Lang: en
Country: - Lang: pt
Country: - Lang: fr
Country: - Lang: de
Country: - Lang: it
Country: - Lang: ja
Country: - Lang: ko
Country: - Lang: zh
Country: CN - Lang: zh
Country: TW - Lang: zh
Country: FR - Lang: fr
Country: DE - Lang: de
Country: IT - Lang: it
Country: JP - Lang: ja
Country: KR - Lang: ko
Country: GB - Lang: en
Country: US - Lang: en
Country: BR - Lang: pt
Country: PT - Lang: pt
Country: CA - Lang: en
Country: CA - Lang: fr
Country: - Lang:
[WARNING] orphan NativePeer method: java.util.ResourceBundle.getClassContext()[Ljava/lang/Class;

====================================================== error 1
gov.nasa.jpf.vm.NoUncaughtExceptionsProperty
java.util.MissingResourceException: Can't find bundle for base name org.apache.xerces.impl.msg.SAXMessages, locale en_US
at java.util.ResourceBundle.throwMissingResourceException(ResourceBundle.java:1581)
at java.util.ResourceBundle.getBundleImpl(ResourceBundle.java:1396)
at java.util.ResourceBundle.getBundle(ResourceBundle.java:854)
at org.apache.xerces.util.SAXMessageFormatter.formatMessage
at org.apache.xerces.parsers.AbstractSAXParser.setProperty
at org.jdom.input.SAXBuilder.configureParser(SAXBuilder.java:701)
at org.jdom.input.SAXBuilder.build(SAXBuilder.java:505)
at org.jdom.input.SAXBuilder.build(SAXBuilder.java:905)
at org.jdom.input.SAXBuilder.build(SAXBuilder.java:884)
at adasim.model.internal.SimulationXMLReader.(SimulationXMLReader.java:85)
at adasim.model.internal.SimulationXMLReader.buildSimulator(SimulationXMLReader.java:105)
at adasim.TrafficMain.run(TrafficMain.java:86)
at TrafficMainRun.main(TrafficMainRun.java:8)
Caused by: java.lang.ClassCastException: java.lang.NoSuchMethodException cannot be cast to java.io.IOException
at java.util.ResourceBundle$Control.newBundle(ResourceBundle.java:2700)
at java.util.ResourceBundle.loadBundle(ResourceBundle.java:1518)
at java.util.ResourceBundle.findBundle(ResourceBundle.java:1482)
at java.util.ResourceBundle.findBundle(ResourceBundle.java:1436)
at java.util.ResourceBundle.findBundle(ResourceBundle.java:1436)
at java.util.ResourceBundle.getBundleImpl(ResourceBundle.java:1370)
at java.util.ResourceBundle.getBundle(ResourceBundle.java:854)
at org.apache.xerces.util.SAXMessageFormatter.formatMessage
at org.apache.xerces.parsers.AbstractSAXParser.setProperty
at org.jdom.input.SAXBuilder.configureParser(SAXBuilder.java:701)
at org.jdom.input.SAXBuilder.build(SAXBuilder.java:505)
at org.jdom.input.SAXBuilder.build(SAXBuilder.java:905)
at org.jdom.input.SAXBuilder.build(SAXBuilder.java:884)
at adasim.model.internal.SimulationXMLReader.(SimulationXMLReader.java:85)
at adasim.model.internal.SimulationXMLReader.buildSimulator(SimulationXMLReader.java:105)
at adasim.TrafficMain.run(TrafficMain.java:86)
at TrafficMainRun.main(TrafficMainRun.java:8)

====================================================== snapshot #1
thread java.lang.Thread:{id:0,name:main,status:RUNNING,priority:5,isDaemon:false,lockCount:0,suspendCount:0}
call stack:
at org.jdom.input.SAXBuilder.build(SAXBuilder.java:545)
at org.jdom.input.SAXBuilder.build(SAXBuilder.java:905)
at org.jdom.input.SAXBuilder.build(SAXBuilder.java:884)
at adasim.model.internal.SimulationXMLReader.(SimulationXMLReader.java:85)
at adasim.model.internal.SimulationXMLReader.buildSimulator(SimulationXMLReader.java:105)
at adasim.TrafficMain.run(TrafficMain.java:86)
at TrafficMainRun.main(TrafficMainRun.java:8)

====================================================== results
error #1: gov.nasa.jpf.vm.NoUncaughtExceptionsProperty "java.util.MissingResourceException: Can't find bun..."

====================================================== statistics
elapsed time: 00:00:00
states: new=3,visited=0,backtracked=3,end=0
search: maxDepth=3,constraints=0
choice generators: thread=3 (signal=0,lock=1,sharedRef=0,threadApi=0,reschedule=2), data=0
heap: new=4031,released=504,maxLive=1731,gcCycles=2
instructions: 137081
max memory: 75MB
loaded code: classes=409,methods=5850

====================================================== search finished: 4/28/22 11:01 AM

[cyrille-artho]

There are many methods that JPF does not support. You have to write so-called "model classes" for them; check the JPF wiki and research papers in that area for more information.