Fix class loading order to support any extension

[Mahmoud-Khawaja]

No description provided.

[Mahmoud-Khawaja]

Hi @cyrille-artho ,

This is more elegant solution that adding a new config in init in ClassLoaderInfo. I was thinking first about adding vm.model_class_priority but to be honest it sounded like adding stuff rather than fixing the main issue. I think this is a good solution so far. the main issue was when we tried to override a model class that already existed in jpf core (such as java.lang.Math or java.lang.String) it wouldn't work because the order of search

jpf was searching for classes in the following order:
1 classpath (application classes)
2 vm.boot_classpath (jpf-core model classes)
3 jrt classes

so here is the thing
in the old code we had

// loading class path first
pathElements = getPathElements(conf, "classpath", appId); 


// then load vm.boot_classpath (jpf-core)
pathElements = getPathElements(conf, "vm.boot_classpath", appId);

but in the new code we are looking for all properties named *.boot_classpath if it found something like our test ext
jpf-test.boot_classpath it will load it first before anythingelse and add it to the class path.

I've tested that on my machine and it works good now

in jpf-test ext in Math.java model class

i have a function abs that should that should return 999 regardless the parameter

    public static int abs(int a) {
        return 999;  // wrong on purpose
    }

when i test that

java -jar ../jpf-core/build/RunJPF.jar TestMath.jpf

public class TestMath {
    public static void main(String[] args) {
        int absVal = Math.abs(-42);

        System.out.println(absVal); // should be 99
    }
}

it will result

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

====================================================== search started: 1/11/26, 7:23 AM
999

====================================================== results
no errors detected

====================================================== statistics
elapsed time:       00:00:00
states:             new=1,visited=0,backtracked=1,end=1
search:             maxDepth=1,constraints=0
choice generators:  thread=1 (signal=0,lock=1,sharedRef=0,threadApi=0,reschedule=0), data=0
heap:               new=496,released=24,maxLive=0,gcCycles=1
instructions:       9160
max memory:         250MB
loaded code:        classes=80,methods=1658

====================================================== search finished: 1/11/26, 7:23 AM

which means that its using the function in my model class. same thing for string model class. Now, I think this will be helpful to fix the same issue we had with jpf-nas months ago. Please Let me know what you think about that

[Mahmoud-Khawaja]

Hi Cyrille,

Cleaned this up to just the classpath ordering change. It now loads extension *.boot_classpath entries before the normal classpath and vm.boot_classpath, so extensions like jpf-nas can override the core model classes without touching vm.boot_classpath.

Also dropped the <s> token I'd added (nothing else uses it) and reverted the unrelated whitespace in the header and createClassInfo.

Tested with jpf-nas on Java 11, SocketTest passes.