Caused by: gov.nasa.jpf.JPFException: not a int field: value

[Alexander Pelepeychenko]

Where is bug tracker of jpf?

When i try to run analize of my test app, internal exeception occur.

May be, exception thrown, because class JPF_java_util_concurrent_atomic_AtomicLong have copy&paste-driven errors: threre is getIntField call instead of getLongField in methods getAndAdd__J__J, incrementAndGet____J, decrementAndGet____J, addAndGet__J__J

import java.util.Map;
import java.util.concurrent.ConcurrentSkipListMap;

public class MyApp {

    static class Th extends Thread {
        int a, b;
        Map<Integer, Integer> map;

        public Th(int a, int b, Map<Integer, Integer> map) {
            this.a = a;
            this.b = b;
            this.map = map;
        }

        @Override
        public void run() {
            map.compute(a, (k, v) -> {
                map.remove(b);
                return b;
            });
        }
    }

    public static void main(String[] args) {
        Map<Integer, Integer> m = new ConcurrentSkipListMap<>();

        new Th(1, 2, m).start();
        new Th(2, 1, m).start();
    }

}

---------------------- JPF error stack trace ---------------------
gov.nasa.jpf.JPFException: not a int field: value
    at gov.nasa.jpf.vm.ElementInfo.getIntField(ElementInfo.java:1130)
    at gov.nasa.jpf.vm.ElementInfo.getIntField(ElementInfo.java:1004)
    at gov.nasa.jpf.vm.MJIEnv.getIntField(MJIEnv.java:459)
    at gov.nasa.jpf.vm.JPF_java_util_concurrent_atomic_AtomicLong.getAndAdd__J__J(JPF_java_util_concurrent_atomic_AtomicLong.java:61)
    at sun.reflect.NativeMethodAccessorImpl.invoke0(Native Method)
    at sun.reflect.NativeMethodAccessorImpl.invoke(NativeMethodAccessorImpl.java:62)
    at sun.reflect.DelegatingMethodAccessorImpl.invoke(DelegatingMethodAccessorImpl.java:43)
    at java.lang.reflect.Method.invoke(Method.java:498)
    at gov.nasa.jpf.vm.NativeMethodInfo.executeNative(NativeMethodInfo.java:125)
    at gov.nasa.jpf.jvm.bytecode.EXECUTENATIVE.execute(EXECUTENATIVE.java:73)
    at gov.nasa.jpf.vm.ThreadInfo.executeInstruction(ThreadInfo.java:1908)
    at gov.nasa.jpf.vm.ThreadInfo.executeTransition(ThreadInfo.java:1859)
    at gov.nasa.jpf.vm.SystemState.executeNextTransition(SystemState.java:765)
    at gov.nasa.jpf.vm.VM.forward(VM.java:1722)
    at gov.nasa.jpf.search.Search.forward(Search.java:579)
    at gov.nasa.jpf.search.DFSearch.search(DFSearch.java:79)
    at gov.nasa.jpf.JPF.run(JPF.java:613)
    at gov.nasa.jpf.JPF.start(JPF.java:189)
    at gov.nasa.jpf.JPF.main(JPF.java:156)
    at sun.reflect.NativeMethodAccessorImpl.invoke0(Native Method)
    at sun.reflect.NativeMethodAccessorImpl.invoke(NativeMethodAccessorImpl.java:62)
    at sun.reflect.DelegatingMethodAccessorImpl.invoke(DelegatingMethodAccessorImpl.java:43)
    at java.lang.reflect.Method.invoke(Method.java:498)
    at com.intellij.rt.execution.application.AppMain.main(AppMain.java:144)
Exception in thread "main" ---------------------- JPF error stack trace ---------------------
gov.nasa.jpf.JPFNativePeerException: exception in native method java.util.concurrent.atomic.AtomicLong.getAndAdd
    at gov.nasa.jpf.vm.NativeMethodInfo.executeNative(NativeMethodInfo.java:186)
    at gov.nasa.jpf.jvm.bytecode.EXECUTENATIVE.execute(EXECUTENATIVE.java:73)
    at gov.nasa.jpf.vm.ThreadInfo.executeInstruction(ThreadInfo.java:1908)
    at gov.nasa.jpf.vm.ThreadInfo.executeTransition(ThreadInfo.java:1859)
    at gov.nasa.jpf.vm.SystemState.executeNextTransition(SystemState.java:765)
    at gov.nasa.jpf.vm.VM.forward(VM.java:1722)
    at gov.nasa.jpf.search.Search.forward(Search.java:579)
    at gov.nasa.jpf.search.DFSearch.search(DFSearch.java:79)
    at gov.nasa.jpf.JPF.run(JPF.java:613)
    at gov.nasa.jpf.JPF.start(JPF.java:189)
    at gov.nasa.jpf.JPF.main(JPF.java:156)
    at sun.reflect.NativeMethodAccessorImpl.invoke0(Native Method)
    at sun.reflect.NativeMethodAccessorImpl.invoke(NativeMethodAccessorImpl.java:62)
    at sun.reflect.DelegatingMethodAccessorImpl.invoke(DelegatingMethodAccessorImpl.java:43)
    at java.lang.reflect.Method.invoke(Method.java:498)
    at com.intellij.rt.execution.application.AppMain.main(AppMain.java:144)
Caused by: gov.nasa.jpf.JPFException: not a int field: value
    at gov.nasa.jpf.vm.ElementInfo.getIntField(ElementInfo.java:1130)
    at gov.nasa.jpf.vm.ElementInfo.getIntField(ElementInfo.java:1004)
    at gov.nasa.jpf.vm.MJIEnv.getIntField(MJIEnv.java:459)
    at gov.nasa.jpf.vm.JPF_java_util_concurrent_atomic_AtomicLong.getAndAdd__J__J(JPF_java_util_concurrent_atomic_AtomicLong.java:61)
    at sun.reflect.NativeMethodAccessorImpl.invoke0(Native Method)
    at sun.reflect.NativeMethodAccessorImpl.invoke(NativeMethodAccessorImpl.java:62)
    at sun.reflect.DelegatingMethodAccessorImpl.invoke(DelegatingMethodAccessorImpl.java:43)
    at java.lang.reflect.Method.invoke(Method.java:498)
    at gov.nasa.jpf.vm.NativeMethodInfo.executeNative(NativeMethodInfo.java:125)
    ... 15 more

[Alexander Pelepeychenko]

path for fix it attached

[Nastaran Shafiei]

Thanks for reporting the bug. I am going to fix it.

Nastaran

--

---
You received this message because you are subscribed to the Google Groups "Java™ Pathfinder" group.
To unsubscribe from this group and stop receiving emails from it, send an email to java-pathfind...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.