A false positive and false negative

[Linhao87]

Nice tool! I played the demo a little bit and found two cases where the analysis does not work very well.

False positive example:

void mayLeakResource() throws IOException {
    OutputStream stream = Resources.allocateResource();
    if (stream == null) {
      return;
    }

    try {
      stream.write(12); // false positive, warns about unclosed stream
    } finally {
        mayClose(stream, -10);
    }
}
  
void mayClose(OutputStream stream, double value) {
      if (value < 0) { // remove this condition, however, the warning goes away
          try {
            stream.close();  
          } catch (Exception ex) {}
      }
}

It seems that in the analysis, the stream argument flows into the mayClose function. And it is reasonable to infer that -10 also flows into the value argument. The analyzer should be able to learn that value < 0 is true, and reports no warning.

Another example of false negative, this is probably due to the lack of symbolic summary of built-in functions.

False negative example:

void mayLeakResource() throws IOException {
    OutputStream stream = Resources.allocateResource();
    if (stream == null) {
      return;
    }

    try {
      stream.write(12); // the analyzer should report warning here, but it didn't
    } finally {
        mayClose(stream);
    }
}
  
void mayClose(OutputStream stream) {
      if (Math.random() > 100) {
          try {
            stream.close();  // false negative
          } catch (Exception ex) {}
      }
}

[cristianoc]

@Linhao87 thanks for the report!
For the first example, do you get the expected behavior using integers instead of doubles?

[Linhao87]

@cristianoc Yes, I got the expected behavior using integers. The first one looks more like a bug now.

[cristianoc]

@Linhao87 yes looks there is a bug in the treatment of non-integer constants.