From c79f9662791e3a99bccee6c61777c1d5bf69b7da Mon Sep 17 00:00:00 2001 From: Jules Villard Date: Mon, 11 Feb 2019 06:48:18 -0800 Subject: [PATCH] [java] model `Double` like `Integer` Summary: Get rid of false positive as in the test by modelling `Double`. Longer term we should probably prevent biabduction from blocking the angelic analysis on `Nullable` fields but that seems harder. Reviewed By: jeremydubreil Differential Revision: D14005228 fbshipit-source-id: 59ef2ed66 --- infer/models/java/src/java/lang/Double.java | 31 +++++++++++++++++++ .../java/infer/DoubleExample.java | 24 ++++++++++++++ .../tests/codetoanalyze/java/infer/issues.exp | 1 + 3 files changed, 56 insertions(+) create mode 100644 infer/models/java/src/java/lang/Double.java create mode 100644 infer/tests/codetoanalyze/java/infer/DoubleExample.java diff --git a/infer/models/java/src/java/lang/Double.java b/infer/models/java/src/java/lang/Double.java new file mode 100644 index 000000000..ae304cfb7 --- /dev/null +++ b/infer/models/java/src/java/lang/Double.java @@ -0,0 +1,31 @@ +/* + * Copyright (c) 2019-present, Facebook, Inc. + * + * This source code is licensed under the MIT license found in the + * LICENSE file in the root directory of this source tree. + */ + +package java.lang; + +public final class Double { + + protected final double value; + + public Double(double i) { + this.value = i; + } + + public static Double valueOf(double i) { + return new Double(i); + } + + public boolean equals(Object anObject) { + return anObject != null + && anObject instanceof Double + && this.value == ((Double) anObject).value; + } + + public double doubleValue() { + return this.value; + } +} diff --git a/infer/tests/codetoanalyze/java/infer/DoubleExample.java b/infer/tests/codetoanalyze/java/infer/DoubleExample.java new file mode 100644 index 000000000..536d33d8a --- /dev/null +++ b/infer/tests/codetoanalyze/java/infer/DoubleExample.java @@ -0,0 +1,24 @@ +/* + * Copyright (c) 2019-present, Facebook, Inc. + * + * This source code is licensed under the MIT license found in the + * LICENSE file in the root directory of this source tree. + */ + +package codetoanalyze.java.infer; + +import javax.annotation.Nullable; + +public class DoubleExample { + + @Nullable Double x; + + private Double testAssignNonNullOk() { + x = 1.0; + return x + 1.0; + } + + private Double testdReadNullableBad() { + return x + 1.0; + } +} diff --git a/infer/tests/codetoanalyze/java/infer/issues.exp b/infer/tests/codetoanalyze/java/infer/issues.exp index c39404ffb..bf680a9b7 100644 --- a/infer/tests/codetoanalyze/java/infer/issues.exp +++ b/infer/tests/codetoanalyze/java/infer/issues.exp @@ -42,6 +42,7 @@ codetoanalyze/java/infer/CursorNPEs.java, codetoanalyze.java.infer.CursorNPEs.cu codetoanalyze/java/infer/DivideByZero.java, codetoanalyze.java.infer.DivideByZero.callDivideByZeroInterProc():int, 1, DIVIDE_BY_ZERO, no_bucket, ERROR, [start of procedure callDivideByZeroInterProc(),start of procedure divideByZeroInterProc(...)] codetoanalyze/java/infer/DivideByZero.java, codetoanalyze.java.infer.DivideByZero.divByZeroLocal(java.lang.String):int, 3, DIVIDE_BY_ZERO, no_bucket, ERROR, [start of procedure divByZeroLocal(...)] codetoanalyze/java/infer/DivideByZero.java, codetoanalyze.java.infer.DivideByZero.divideByZeroWithStaticField():int, 2, DIVIDE_BY_ZERO, no_bucket, ERROR, [start of procedure divideByZeroWithStaticField(),start of procedure setXToZero(),return from a call to void DivideByZero.setXToZero(),start of procedure divideByZeroInterProc(...)] +codetoanalyze/java/infer/DoubleExample.java, codetoanalyze.java.infer.DoubleExample.testdReadNullableBad():java.lang.Double, 1, NULL_DEREFERENCE, B1, ERROR, [start of procedure testdReadNullableBad()] codetoanalyze/java/infer/DynamicDispatch.java, codetoanalyze.java.infer.DynamicDispatch$WithField.dispatchOnFieldBad():void, 3, NULL_DEREFERENCE, B1, ERROR, [start of procedure dispatchOnFieldBad(),start of procedure DynamicDispatch$Subtype(),start of procedure DynamicDispatch$Supertype(),return from a call to DynamicDispatch$Supertype.(),return from a call to DynamicDispatch$Subtype.(),start of procedure DynamicDispatch$WithField(...),return from a call to DynamicDispatch$WithField.(DynamicDispatch$Subtype),start of procedure foo(),return from a call to Object DynamicDispatch$Subtype.foo()] codetoanalyze/java/infer/DynamicDispatch.java, codetoanalyze.java.infer.DynamicDispatch.dynamicDispatchCallsWrapperWithSubtypeBad():void, 3, NULL_DEREFERENCE, B1, ERROR, [start of procedure dynamicDispatchCallsWrapperWithSubtypeBad(),start of procedure DynamicDispatch$Subtype(),start of procedure DynamicDispatch$Supertype(),return from a call to DynamicDispatch$Supertype.(),return from a call to DynamicDispatch$Subtype.(),start of procedure dynamicDispatchWrapperFoo(...),start of procedure foo(),return from a call to Object DynamicDispatch$Subtype.foo(),return from a call to Object DynamicDispatch.dynamicDispatchWrapperFoo(DynamicDispatch$Subtype)] codetoanalyze/java/infer/DynamicDispatch.java, codetoanalyze.java.infer.DynamicDispatch.dynamicDispatchCallsWrapperWithSupertypeBad():void, 3, NULL_DEREFERENCE, B1, ERROR, [start of procedure dynamicDispatchCallsWrapperWithSupertypeBad(),start of procedure DynamicDispatch$Supertype(),return from a call to DynamicDispatch$Supertype.(),start of procedure dynamicDispatchWrapperBar(...),start of procedure bar(),return from a call to Object DynamicDispatch$Supertype.bar(),return from a call to Object DynamicDispatch.dynamicDispatchWrapperBar(DynamicDispatch$Supertype)]