NullPointerException is expected as a result of the correct test

[EgorkaKulikov]

Generate tests in the following configuration:

timeLimit=60
methodFilter = "org.usvm.samples.primitives.IntExamples.*"
projectFilter = listOf("samples")

There are two tests for the function isInteger. They have the same input. One of them is incorrect.

///region Test suites for executable org.usvm.samples.primitives.IntExamples.isInteger
    
    
    /**
     * @utbot.classUnderTest {@link org.usvm.samples.primitives.IntExamples}
     * @utbot.methodUnderTest {@link org.usvm.samples.primitives.IntExamples#isInteger(java.lang.String)}
     */
    @Test
    public void testIsIntegerReturnsFalse() {
        boolean actual = IntExamples.isInteger(null);
        
        assertFalse(actual);
    }
    
    /**
     * @utbot.classUnderTest {@link org.usvm.samples.primitives.IntExamples}
     * @utbot.methodUnderTest {@link org.usvm.samples.primitives.IntExamples#isInteger(java.lang.String)}
     */
    @Test(expected = NullPointerException.class)
    public void testIsIntegerThrowsNPE() {
        IntExamples.isInteger(null);
    }
    
    ///endregion

It seems that erronous NPE comes from the JcState

[EgorkaKulikov]

Another example, here failing test is correct, while non-failing is not

/**
     * @utbot.classUnderTest {@link org.usvm.samples.controlflow.Switch}
     * @utbot.methodUnderTest {@link org.usvm.samples.controlflow.Switch#stringSwitch(java.lang.String)}
     */
    @Test
    public void testStringSwitch() {
        Switch switch1 = new Switch();
        
        int actual = switch1.stringSwitch(null);
        
        assertEquals(-1, actual);
    }
    
    /**
     * @utbot.classUnderTest {@link org.usvm.samples.controlflow.Switch}
     * @utbot.methodUnderTest {@link org.usvm.samples.controlflow.Switch#stringSwitch(java.lang.String)}
     */
    @Test(expected = NullPointerException.class)
    public void testStringSwitchThrowsNPE() {
        Switch switch1 = new Switch();
        
        switch1.stringSwitch(null);
    }

[Damtev]

Briefly, the reason for this incorrect NPE is the lack of approximation for java.lang.String.

In more detail, the JcMachine has no information that the value field of any correct String instance is always not null. So, the machine considers the value of the input string as a common input field that may be null, and retrieving its length may lead to NPE. There are no more executions than 2 because of the default steps limit 3500, but there are still no meaningful executions even with increased steps limit and/or timeout.

As java.lang.Integer#parseInt(java.lang.String, int) is quite complex, I suppose approximations are the only way to fix this problem.