Confirm programs with null pointer exception that are labelled with "No issues found"

[mdlnhurmuz]

Hi,

I am generating benchmarks with null pointer exception and on these benchmarks I am currently running Infer to see whether the NPE issue is found by Infer. It seems that my benchmarks are labelled with "No issues found", i.e. Infer does not find the NPE.

I was wondering if you could confirm the two attached examples of benchmarks.

Thank you, Madalina

Relevant information:

• Infer version v1.1.0
• MacOS Big Sur, version 11.6.2. No Docker.
• Command I ran: infer run -- javac Program.java

RootProgram1Mnpeiancm.java.txt RootProgram4DtmcIfwono.java.txt

[jvillard]

Hi @mdlnhurmuz, thank you for your report! For your first example, infer does report an issue, is that not the one you wanted?

$ ./infer-linux64-v1.1.0/bin/infer -- javac RootProgram1Mnpeiancm.java
[...]
RootProgram1Mnpeiancm.java:50: error: Null Dereference
  object `box` last assigned on line 48 could be null and is dereferenced by call to `test(...)` at line 50.
  48.           Box<Integer> box = null;
  49.           Hello h = new Hello();
  50. >         h.test(box);
  51.       }
  52.   }

The second one is indeed a false negative. It seems that we don't take the implicit zero-initialisation in Java constructors into account, we should fix that! Here's a more minimal example that shows the problem:

class Box {
  public Object g;
  public Box() { } // the summary of the constructor does not say that g = null
}

class NullInitDeref {
  void FN_null_init_deref_bad()
    Box b = new Box();
    b.g.toString(); // missing NPE report here
  }
}

[jvillard]

Actually, infer does find the NPE in the second example as well, but filters it out by default so you need to pass -F to see it:

$ ./infer-linux64-v1.1.0/bin/infer -F -- javac RootProgram4DtmcIfwono.java
RootProgram4DtmcIfwono.java:60: error: Null Dereference
  object `o` last assigned on line 59 could be null and is dereferenced by call to `print(...)` at line 60.
  58.           Box<Integer> b = new Box<Integer>().bvits();
  59.           Object o = b.g;
  60. >         print(o);
  61.       }
  62.   }

[mdlnhurmuz]

Hey @jvillard,

Thank you so much for your quick reply.

I can indeed replicate the command and behaviour on the second example and it shows me the NPE, but on the first one I still do not get the NPE issue.

I followed the instructions here to install Infer and running only the command I mentioned.

Is there something else I could check to fix running Infer on my computer?

Many thanks, Madalina

[jvillard]

What version of Java do you have on your machine? javac -version and java -version. You may need to force the Java version with --java-version.

[mdlnhurmuz]

I was using Java 15.0.2 and downgraded now to 1.8.0 and it seems to be working. Thanks a lot for the prompt answers. Closing this issue now.

[mdlnhurmuz]

Hi,

Reopening this bug with some minor questions.

1) Could you confirm this program as false negative?

public class RootProgram5 {
    public static void main(String[] args) {
        String[] array = new String[3];
        String s = array[0];
        System.out.println(s.toString());
    }
}

2) I was wondering what are the current java versions that Infer supports on MacOS. Is it documented up to which java version Infer works as expected?

Many thanks, Madalina

[MazizEsa]

@jvillard so this only supports jdk 1.8? > 1.8 it doesn't?