Hi Cyrille,
Thank you for the response.
> I think it is probably the case that Scala companion objects may not be directly accessible from Java.
Well, the only object I have is MyRCTest in
src/examples/MyRCTest.scala. That's my tester. But, the error speaks
about scaltut.MyRC, which is the listener I (supposedly) implemented
in Scala.
> Try to implement a class with a singleton pattern and a public static getInstance() method. That should be compiled to Java-like bytecode.
I changed my JPF file (src/example/MyRCTest.jpf) to
target = RangeCheckerTest
listener=scaltut.MyRC
rc.field=RangeCheckerTest.data
rc.min=0
rc.max=42
Namely, changed the tester class to the Java one; and, I still get the
same error. For the reference, I am putting my -log -show output in
the P.S. Is that more directive?
> Check the Scala books/documentation and the output of "javap" to find out more.
Sure. I'll send an updated posting if javap turns out to be a game changer.
Cheers,
--Hossein
P.S.
loading property file: C:\Users\Hossein\.jpf\site.properties
loading property file: C:\...\JPF\JPF_HOME\jpf.properties
loading property file: C:\...\JPF\jpf-shell-new\jpf.properties
loading property file: C:\...\JPF\jpf-tut-new\jpf.properties
----------- Config contents
C = /Sources/Scala/eclipse/plugins/org.scala-lang.scala-library.source_2.11.8.v20160304-115712-1706a37eb8.jar
branch_start = 1
cg.boolean.false_first = true
cg.break_single_choice = false
cg.enable_atomic = true
cg.enumerate_random = false
cg.max_processors = 1
cg.randomize_choices = NONE
cg.seed = 42
cg.threads.break_arrays = false
cg.threads.break_sleep = true
cg.threads.break_start = true
cg.threads.break_yield = true
config = C:\...\JPF\jpf-tut-new\jpf.properties
config_path = C:\...\JPF\jpf-tut-new
extensions = ,C:/.../JPF/jpf-shell-new/,C:/.../JPF/jpf-aprop,C:/.../JPF/jpf-numeric,C:/.../JPF/jpf-shell,C:/.../JPF/jpf-awt,C:/.../JPF/jpf-awt-shell
jpf-aprop = C:/.../JPF/jpf-aprop
jpf-awt = C:/.../JPF/jpf-awt
jpf-awt-shell = C:/.../JPF/jpf-awt-shell
jpf-core = C:\...\JPF\JPF_HOME
jpf-core.classpath =
C:\...\JPF\JPF_HOME/build/jpf-classes.jar;C:\...\JPF\JPF_HOME/build/examples
jpf-core.native_classpath =
C:\...\JPF\JPF_HOME/build/jpf.jar;C:\...\JPF\JPF_HOME/build/jpf-annotations.jar
jpf-core.peer_packages = gov.nasa.jpf.vm,<model>,<default>
jpf-core.sourcepath = C:\...\JPF\JPF_HOME/src/examples
jpf-core.test_classpath = C:\...\JPF\JPF_HOME/build/tests
jpf-numeric = C:/.../JPF/jpf-numeric
jpf-shell = C:\...\JPF\jpf-shell-new
jpf-shell.classpath = C:\...\JPF\jpf-shell-new/build/examples
jpf-shell.native_classpath =
C:\...\JPF\jpf-shell-new/build/jpf-shell.jar;C:\...\JPF\jpf-shell-new/lib/collections-generic-4.01.jar;C:\...\JPF\jpf-shell-new/lib/colt-1.2.0.jar;C:\...\JPF\jpf-shell-new/lib/jung-algorithms-2.0.jar;C:\...\JPF\jpf-shell-new/lib/jung-api-2.0.jar;C:\...\JPF\jpf-shell-new/lib/jung-graph-impl-2.0.jar;C:\...\JPF\jpf-shell-new/lib/jung-visualization-2.0.jar
jpf-shell.sourcepath = C:\...\JPF\jpf-shell-new/src/examples
jpf-tutorial = C:\...\JPF\jpf-tut-new
jpf-tutorial.classpath = C:\...\JPF\jpf-tut-new/build/examples
jpf-tutorial.native_classpath =
C:\...\JPF\jpf-tut-new/build/jpf-tutorial.jar;C:\...\JPF\jpf-tut-new/lib/*.jar;
jpf-tutorial.sourcepath = C:\...\JPF\jpf-tut-new/src/examples
jpf-tutorial.test_classpath = C:\...\JPF\jpf-tut-new/build/tests
jpf.home = C:/.../JPF
jpf.print_exception_stack = true
jpf.site = C:\Users\Hossein\.jpf\site.properties
jvm.insn_factory.class = gov.nasa.jpf.jvm.bytecode.InstructionFactory
jvm.nested_init = false
jvm.nested_init.exclude = java.*,javax.*,sun.misc.*
listener.autoload = gov.nasa.jpf.NonNull,gov.nasa.jpf.Const
listener.gov.nasa.jpf.Const = gov.nasa.jpf.tools.ConstChecker
listener.gov.nasa.jpf.NonNull = gov.nasa.jpf.tools.NonNullChecker
log.handler.class = gov.nasa.jpf.util.LogHandler
log.level = warning
race.exclude = java.*,javax.*
report.class = gov.nasa.jpf.report.Reporter
report.console.class = gov.nasa.jpf.report.ConsolePublisher
report.console.constraint = constraint,snapshot
report.console.finished = result,statistics
report.console.probe = statistics
report.console.property_violation = error,snapshot
report.console.show_code = false
report.console.show_method = true
report.console.show_steps = true
report.console.start = jpf,sut
report.console.transition =
report.html.class = gov.nasa.jpf.report.HTMLPublisher
report.html.constraint = constraint
report.html.finished = result,statistics,error,snapshot,output
report.html.property_violation =
report.html.start = jpf,sut,platform,user,dtg,config
report.publisher = console
report.xml.class = gov.nasa.jpf.report.XMLPublisher
search.class = gov.nasa.jpf.search.DFSearch
search.heuristic.branch.count_early = true
search.heuristic.branch.no_branch_return = -1
search.heuristic.queue_limit = -1
search.match_depth = false
search.min_free = 1M
search.multiple_errors = false
search.properties =
gov.nasa.jpf.vm.NotDeadlockedProperty,gov.nasa.jpf.vm.NoUncaughtExceptionsProperty
shell.available_commands = test,verify
shell.available_panels = properties,config,site,report,test,verify,logging
shell.commands = test,verify
shell.commands.test = .shell.commands.TestCommand
shell.commands.verify = .shell.commands.VerifyCommand
shell.panels = properties,config,site,report,test,verify,logging
shell.panels.config = .shell.panels.ConfigPanel
shell.panels.logging = .shell.panels.LoggingPanel
shell.panels.properties = .shell.panels.PropertiesPanel
shell.panels.report = .shell.panels.ReportPanel
shell.panels.script = .shell.panels.ScriptPanel
shell.panels.searchgraph = .shell.panels.SearchGraphPanel
shell.panels.site = .shell.panels.SitePanel
shell.panels.test = .shell.panels.TestConsolePanel
shell.panels.verify = .shell.panels.VerifyConsolePanel
shell.textfont.name = Monospaced
shell.textfont.size = 13
shell.textfont.style = 0
shell.update_interval = 1000
test.report.console.finished = result
vm.backtracker.class = gov.nasa.jpf.vm.DefaultBacktracker
vm.boot_classpath = <system>
vm.class = gov.nasa.jpf.vm.SingleProcessVM
vm.classloader.class = gov.nasa.jpf.jvm.JVMSystemClassLoaderInfo
vm.fields_factory.class = gov.nasa.jpf.vm.DefaultFieldsFactory
vm.finalize = false
vm.gc = true
vm.heap.class = gov.nasa.jpf.vm.OVHeap
vm.ignore_uncaught_handler = false
vm.max_alloc_gc = -1
vm.max_transition_length = 50000
vm.no_orphan_methods = false
vm.pass_uncaught_handler = true
vm.path_output = false
vm.process_finalizers = false
vm.restorer.class = .vm.DefaultMementoRestorer
vm.reuse_tid = false
vm.scheduler.class = gov.nasa.jpf.vm.DelegatingScheduler
vm.scheduler.sharedness.class = gov.nasa.jpf.vm.PathSharednessPolicy
vm.scheduler.sync.class = gov.nasa.jpf.vm.AllRunnablesSyncPolicy
vm.scheduler_factory.class = gov.nasa.jpf.vm.DefaultSchedulerFactory
vm.serializer.class = gov.nasa.jpf.vm.serialize.CFSerializer
vm.shared.break_on_exposure = true
vm.shared.never_break_fields =
java.lang.Thread*.*,java.lang.System.*,java.lang.Runtime.*,java.lang.Boolean.*,java.lang.String.*,java.lang.*.TYPE,java.util.HashMap.EMPTY_TABLE,java.util.HashSet.PRESENT,java.util.concurrent.ThreadPoolExecutor*.*,java.util.concurrent.ThreadPoolExecutor*.*,java.util.concurrent.TimeUnit.*,java.util.concurrent.Exchanger.CANCEL,java.util.concurrent.Exchanger.NULL_ITEM,java.util.concurrent.Executors$DefaultThreadFactory.*,sun.misc.VM.*,sun.misc.SharedSecrets.*,sun.misc.Unsafe.theUnsafe,gov.nasa.jpf.util.test.TestJPF.*
vm.shared.never_break_methods =
java.util.concurrent.ThreadPoolExecutor.processWorkerExit,java.util.concurrent.locks.Abstract*Synchronizer.*,java.util.concurrent.ThreadPoolExecutor.getTask,java.util.concurrent.atomic.Atomic*.*,java.util.concurrent.Exchanger.doExchange,java.util.concurrent.ThreadPoolExecutor.interruptIdleWorkers,java.util.concurrent.TimeUnit.*
vm.shared.never_break_types = java.util.concurrent.TimeUnit
vm.shared.skip_constructed_finals = false
vm.shared.skip_finals = true
vm.shared.skip_static_finals = false
vm.shared.sync_detection = true
vm.statics.class = gov.nasa.jpf.vm.OVStatics
vm.storage.class = gov.nasa.jpf.vm.JenkinsStateSet
vm.store_steps = false
vm.sysprop.source = SELECTED
vm.threadlist.class = gov.nasa.jpf.vm.ThreadList
vm.time.class = gov.nasa.jpf.vm.SystemTime
vm.tree_output = true
vm.untracked = true
vm.verify.ignore_path = true
collected native_classpath=C:\...\JPF\jpf-tut-new/build/jpf-tutorial.jar,C:\...\JPF\jpf-tut-new/lib/*.jar,C:\...\JPF\jpf-shell-new/build/jpf-shell.jar,C:\...\JPF\jpf-shell-new/lib/collections-generic-4.01.jar,C:\...\JPF\jpf-shell-new/lib/colt-1.2.0.jar,C:\...\JPF\jpf-shell-new/lib/jung-algorithms-2.0.jar,C:\...\JPF\jpf-shell-new/lib/jung-api-2.0.jar,C:\...\JPF\jpf-shell-new/lib/jung-graph-impl-2.0.jar,C:\...\JPF\jpf-shell-new/lib/jung-visualization-2.0.jar,C:\...\JPF\JPF_HOME/build/jpf.jar,C:\...\JPF\JPF_HOME/build/jpf-annotations.jar
collected native_libraries=null
[SEVERE] JPF configuration error: main class not a valid class name:
C:\...\JPF\jpf-tut-new\src\examples\MyRCTest.scala
> used within "vm.class" instantiation of class gov.nasa.jpf.vm.SingleProcessVM
[SEVERE] JPF terminated