Scala PropertyListenerAdapter

160 views
Skip to first unread message

hossei...@gmail.com

unread,
May 31, 2017, 2:37:27 PM5/31/17
to Java™ Pathfinder
Dear all,

I am trying to teach myself some JPF by following the ASE 2011 Tutorial of Rungta, Mehlitz, and Visser. Given that I am going to use JPF from Scala, I thought I'd implement the same RangeChecker in Scala. I have added a RangeChecker.scala under src/main/scaltut, which I am attaching to this posting. I also have a MyRCTest.scala under src/example:

object MyRCTest {
  var data: Int = ???

  def setData(d: Int) {data = d}

  def main(args: Array[String]) {
    setData( 42)
    setData(-42)
  }
}

Finally, here is my JPF file (src/examples/MyRCTest.jpf):

target = MyRCTest

listener=scaltut.MyRC

rc.field=MyRCTest.data
rc.min=0
rc.max=42

When I try to verify that under Eclipse, I get the exception trace in the P.S. Does anyone know what's going wrong?

TIA,
--Hossein

P.S.

Executing command: java -jar ...\JPF_HOME\build\RunJPF.jar +shell.port=4242 ...\jpf-tutorial\src\examples\MyRCTest.jpf 
java.lang.NoClassDefFoundError: scala/runtime/Nothing$
at java.lang.Class.getDeclaredConstructors0(Native Method)
at java.lang.Class.privateGetDeclaredConstructors(Unknown Source)
at java.lang.Class.getConstructor0(Unknown Source)
at java.lang.Class.getConstructor(Unknown Source)
at gov.nasa.jpf.Config.getInstance(Config.java:1984)
at gov.nasa.jpf.Config.getInstances(Config.java:1839)
at gov.nasa.jpf.JPF.addListeners(JPF.java:448)
at gov.nasa.jpf.JPF.initialize(JPF.java:286)
at gov.nasa.jpf.JPF.<init>(JPF.java:251)
at gov.nasa.jpf.JPF.start(JPF.java:188)
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:80)
at gov.nasa.jpf.tool.RunJPF.main(RunJPF.java:116)
Caused by: java.lang.ClassNotFoundException: scala.runtime.Nothing$
at java.net.URLClassLoader.findClass(Unknown Source)
at java.lang.ClassLoader.loadClass(Unknown Source)
at java.lang.ClassLoader.loadClass(Unknown Source)
... 16 more
 
RangeChecker.scala

Cyrille Artho

unread,
Jun 2, 2017, 5:41:04 AM6/2/17
to Java™ Pathfinder
You need to include Scala's runtime libraries in your classpath.

Seyed H. HAERI (Hossein)

unread,
Jun 2, 2017, 5:25:14 PM6/2/17
to java-pa...@googlegroups.com
Hi Cyrille,

> You need to include Scala's runtime libraries in your classpath.

I see. And, how do I do that?

Cheers,
--Hossein

Seyed H. HAERI (Hossein)

unread,
Jun 7, 2017, 12:08:45 PM6/7/17
to java-pa...@googlegroups.com
Dear all,

Having no response from Cyrille (or others) on how to include Scala in
my classpath, I added the following line to my site.properties:

jpf-core.classpath+=C:/.../org.scala-lang.scala-library.source_2.11.8.v20160304-115712-1706a37eb8.jar

But, then, I get the following error:

Executing command: java -jar C:\My Documents\My
Programs\JPF\JPF_HOME\build\RunJPF.jar +shell.port=4242 C:\My
Documents\Research\UCL\LVL\SeCloud\JPF\jpf-tut-new\src\examples\MyRCTest.jpf
[SEVERE] JPF configuration error: error instantiating class
scaltut.MyRC for entry "listener":no suitable ctor found
[SEVERE] JPF terminated

What's wrong now?

TIA,
--Hossein

On 2 June 2017 at 23:25, Seyed H. HAERI (Hossein)
--
--------------------------------------------------------------------------------------------------------------

Seyed H. HAERI (Hossein), Dr.

Post-Doctoral Research Fellow
Department of Computing Science and Engineering
Catholic University of Louvain
Louvain-la-Neuve, Belgium

ACCU - Professionalism in programming - http://www.accu.org/
--------------------------------------------------------------------------------------------------------------

Cyrille Artho

unread,
Jun 12, 2017, 3:11:18 AM6/12/17
to Java™ Pathfinder
Hi,
I think it is probably the case that Scala companion objects may not be directly accessible from Java.
Try to implement a class with a singleton pattern and a public static getInstance() method. That should be compiled to Java-like bytecode.
Check the Scala books/documentation and the output of "javap" to find out more.

Seyed H. HAERI (Hossein)

unread,
Jun 12, 2017, 8:51:07 AM6/12/17
to java-pa...@googlegroups.com
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

Seyed H. HAERI (Hossein)

unread,
Jun 19, 2017, 10:47:38 AM6/19/17
to java-pa...@googlegroups.com
Hi again Cyrille (and the rest),

> Sure. I'll send an updated posting if javap turns out to be a game changer.

So, here is the update I promised:

I compiled my Scala object using scalac and then used javap to see the
contents. (I have put a copy at the P.S. here.) Then, I even changed
the listener to the out-of-box Java one:

#src/examples/MyRCTest.jpf

target = RC2

listener=tutorial.RangeChecker

rc.field=RC2.data
rc.min=0
rc.max=42

(I also tried it with RC2$, BTW.) I even copied the scalac class files
in my build/main/scaltut and src/classes directories. And, I get the
following error when trying to verify (the above) MyRCTest.jpf:

Executing command: java -jar C:\...\JPF\JPF_HOME\build\RunJPF.jar
+shell.port=4242 C:\...\JPF\jpf-tut-new\src\examples\MyRCTest.jpf
[SEVERE] cannot load application class RC2

What am I missing now? In case you'd like, I can also send you my -log -show.

TIA,
--Hossein

P.S.

$ javap RC2$.class
Compiled from "RC2.scala"
public final class RC2$ {
public static final RC2$ MODULE$;
public static {};
public int data();
public void data_$eq(int);
public void setData(int);
public void main(java.lang.String[]);
}

$ javap RC2.class
Compiled from "RC2.scala"
public final class RC2 {
public static void main(java.lang.String[]);
public static void setData(int);
public static void data_$eq(int);
public static int data();
}

Cyrille Artho

unread,
Jun 29, 2017, 4:24:18 AM6/29/17
to Java™ Pathfinder
Hi Seyed,
I was on vacation so I apologize for the delay.

As you can see from the output of javap, Scala fields (var or val) are not compiled into fields as bytecode. Instead, they are represented as methods.

The RangeChecker is therefore not directly applicable. You'd have to rewrite it to accommodate to Scala's bytecode as well.

Scala's bytecode may change from 2.11 (still most widely used) to 2.12 (the latest stable version), so if you want to try this, be aware which Scala compiler you are using.

hossei...@gmail.com

unread,
Jul 5, 2017, 8:41:05 AM7/5/17
to Java™ Pathfinder, java-pa...@googlegroups.com
Hi Cyrille,

> I was on vacation so I apologize for the delay.

No problem. Hope you had a good one. :)

> As you can see from the output of javap, Scala fields (var or val) are not compiled into fields as bytecode. Instead, they are represented as methods.

Nothing for me to notice on my own as a JVM unfamiliar person. Thank you for bringing that up. 

> The RangeChecker is therefore not directly applicable. You'd have to rewrite it to accommodate to Scala's bytecode as well.

How do you do that? Having posted a similar query to the Scala list, apparently, there is no way to instruct scalac to compile `var`s and `val`s into bytecode fields unless they are `private[this]`. Are such attributed fields essentially accessible to (JPF) listeners?

> Scala's bytecode may change from 2.11 (still most widely used) to 2.12 (the latest stable version), so if you want to try this, be aware which Scala compiler you are using.

Good to know.

Thanks,
--Hossein

Cyrille Artho

unread,
Jul 7, 2017, 3:47:08 AM7/7/17
to Java™ Pathfinder
I think you'd have to reverse engineer which fields are used (internally) for storing val and var types in Scala.

This may change between 2.11 and 2.12, as the compiler back-end has changed.

Most likely, the private field that is used when calling the public methods that represent get/set methods for val/var fields, are very similar to the actual names, just "mangled" with $ signs or such.


On Wednesday, May 31, 2017 at 8:37:27 PM UTC+2, hossei...@gmail.com wrote:

hossei...@gmail.com

unread,
Jul 7, 2017, 11:19:48 AM7/7/17
to Java™ Pathfinder, java-pa...@googlegroups.com
Hi Cyrille,

> I think you'd have to reverse engineer which fields are used (internally) for storing val and var types in Scala.

Sorry, but, I'm not following.


> This may change between 2.11 and 2.12, as the compiler back-end has changed.

Would you mind explaining please?


> Most likely, the private field that is used when calling the public methods that represent get/set methods for val/var fields, are very similar to the actual names, just "mangled" with $ signs or such.

For what it's worth, as shown in the P.S., I added a `private[this]` field (called `predate`) to a Scala object I'd like to be listened (called `MyRCTest4`). I tried javap on `MyRCTest4` and `MyRCTest4$`. The results has no hit for my `predate` or any $-mangled dialect of that. Am I missing anything?

TIA,
--Hossein

P.S.
object MyRCTest4 extends App {
 
var data: Int = 0

 
private[this] var predate: String = "Blah"

 
override def main(args: Array[String]) {

hossei...@gmail.com

unread,
Jul 7, 2017, 2:13:51 PM7/7/17
to Java™ Pathfinder, java-pa...@googlegroups.com
Hi Cyrille,

> As you can see from the output of javap, Scala fields (var or val) are not compiled into fields as bytecode. Instead, they are represented as methods.

Here is an update from the Scala list (copyright Jasper-M):

"A public val gets a public accessor, and a public var gets a public accessor and public mutator. But they're both backed by a private field. Private vals and vars also get the methods but then they're private as well. Private[this] is the exception, those only get a private field."

I am putting the output of javap -p in the P.S. so this also gets demonstrated in action for my case. Now, would you mind elaborating on your words above? In particular, is JPF still missing anything for accessing fields of a Scala object?

TIA,
--Hossein

P.S.

$ javap -p MyRCTest4$.class
Compiled from "MyRCTest.scala"

public final class MyRCTest4$ implements scala.App {
 
public static final MyRCTest4$ MODULE$;
 
private int data;
 
private java.lang.String predate;
 
private final long executionStart;
 
private java.lang.String[] scala$App$$_args;
 
private final scala.collection.mutable.ListBuffer<scala.Function0<scala.runtime.BoxedUnit>> scala$App$$initCode;
 
public static {};
 
public long executionStart();
 
public java.lang.String[] scala$App$$_args();
 
public void scala$App$$_args_$eq(java.lang.String[]);
 
public scala.collection.mutable.ListBuffer<scala.Function0<scala.runtime.BoxedUnit>> scala$App$$initCode();
 
public void scala$App$_setter_$executionStart_$eq(long);
 
public void scala$App$_setter_$scala$App$$initCode_$eq(scala.collection.mutable.ListBuffer);
 
public java.lang.String[] args();
 
public void delayedInit(scala.Function0<scala.runtime.BoxedUnit>);

 
public int data();
 
public void data_$eq(int);

 
public void main(java.lang.String[]);
 
public void setData(int);
 
public final void delayedEndpoint$MyRCTest4$1();
 
private MyRCTest4$();
}


Cyrille Artho

unread,
Jul 11, 2017, 11:25:43 AM7/11/17
to Java™ Pathfinder
Hi,
The output of javap is helpful to explain what I mean.

We have a getter and a setter method:

  public int data();
 
public void data_$eq(int);

These are the methods that are really called behind the scenes, when someone accesses a val or var in Scala.

They update field MyRCTest4$.data internally.

This is a normal field, so perhaps it is enough to set the JPF listener to the intended class name with a "$" appended. Try that and see if it works.

hossei...@gmail.com

unread,
Jul 11, 2017, 1:07:53 PM7/11/17
to Java™ Pathfinder, java-pa...@googlegroups.com
Hi Cyrille,

This finally gets the Scala tester accessible to the Java listener I got out of the box from the tutorial. I highly appreciate all that advice.

Nevertheless, the Scala listener that I had implemented to be the equivalent to the Java listener doesn't still work. Here is the error:

Executing command: java -jar C:\...\build\RunJPF.jar +shell.port=4242 C:\...\src\examples\MyRCTest.jpf 

[SEVERE] JPF configuration error: error instantiating class scaltut.MyRC for entry "listener":no suitable ctor found
[SEVERE] JPF terminated

In case that helps, I am putting the javap output in the P.S. Any idea what's going wrong?

Cheers,
--Hossein

P.S.

$ javap -p MyRC.class
Compiled from "MyRC.scala"
class scaltut.MyRC {
 
var error;
 scaltut
.MyRC();
 
protected def isRelevantField();
 
protected def isValueOutOfRange();
 
protected def storeError();
}


Cyrille Artho

unread,
Jul 17, 2017, 10:08:04 AM7/17/17
to Java™ Pathfinder
Hi,
"ctor" in the error message means "constructor". In your case, you have a zero-argument constructor available. I'm not sure why this is not "suitable" for the listener; maybe it expects a constructor with one argument?
Maybe you can look at the bytecode of a Java class that works, to see what constructors it uses?



On Wednesday, May 31, 2017 at 8:37:27 PM UTC+2, hossei...@gmail.com wrote:

hossei...@gmail.com

unread,
Jul 18, 2017, 2:57:16 PM7/18/17
to Java™ Pathfinder, java-pa...@googlegroups.com
Hi  Cyrille,

> In your case, you have a zero-argument constructor available. I'm not sure why this is not "suitable" for the listener; maybe it expects a constructor with one argument?

As a matter of fact, the Scala code does also have a unary constructor. I realised that constructor, however, is not present in javap's output.

> Maybe you can look at the bytecode of a Java class that works, to see what constructors it uses? 

Very good recommendation. With that intention, I javap'ed the out-of-box Java listener with the -verbose switch. It turns out that there are 9 "Unresolved compilation problems" in there -- which, is a shame because the same JPF projects builds "successfully" in Eclipse!!! Using information from other threads on this list, I resolved 4 of them that pertained to the JPF version updates requiring
gov.nasa.jpf.jvm
to be replaced by
gov.nasa.jpf.vm.

The 5 remaining compile errors are on the inability of resolving the following types:
JVM, ThreadInfo

and
FieldInfo.
Would you mind pointing me to where these creatures currently are?

Once I manage to get the Java listener behave, I'll move on to the Scala one. (Using javap -verbose, I found out that the project build compiles the file for Java rather than Scala!)

Cheers,
--Hossein

Cyrille Artho

unread,
Jul 20, 2017, 3:05:55 PM7/20/17
to Java™ Pathfinder
Hi,
I assume these are other instances where a package changes from "jvm" to "vm". This change was from JPF 7 to JPF 8. Are you sure you have the most recent version of JPF? Either your version is not a fully updated version 8, or parts of the source (such as this listener) still need updating.

hossei...@gmail.com

unread,
Jul 21, 2017, 12:47:31 PM7/21/17
to Java™ Pathfinder, java-pa...@googlegroups.com
Hi Cyrille,
 
> I assume these are other instances where a package changes from "jvm" to "vm". This change was from JPF 7 to JPF 8.

Good to know. Where can I find the list of such updates?

> Are you sure you have the most recent version of JPF?

Well, TortoiseHg says it's 5 months old. And, apparently, that's the most up-to-date TortoiseHg can fetch from the repository.

> Either your version is not a fully updated version 8, or parts of the source (such as this listener) still need updating.

The listener, I know from other threads on the list to be old. It comes from the ASE 2011 tutorial of JPF. Alas, I don't know of a more up-to-date listener that I can use for training myself. I asked on the same other thread for anything newer a month ago and nothing back yet. Is there any such thing you can kindly point me to?

TIA,
--Hossein
Reply all
Reply to author
Forward
0 new messages