Fix the typing implication in the bi-abduction for non Java types

Reviewed By: jvillard

Differential Revision: D2927341

fb-gh-sync-id: abe1140
shipit-source-id: abe1140

infer/src/backend/prover.ml

@@ -1636,8 +1636,8 @@ let texp_imply tenv subs texp1 texp2 e1 calc_missing =
     | Sil.Sizeof (Sil.Tstruct _, _), Sil.Sizeof (Sil.Tstruct _, _)
     | Sil.Sizeof (Sil.Tarray _, _), Sil.Sizeof (Sil.Tarray _, _)
     | Sil.Sizeof (Sil.Tarray _, _), Sil.Sizeof (Sil.Tstruct _, _)
-    | Sil.Sizeof (Sil.Tstruct _, _), Sil.Sizeof (Sil.Tarray _, _) ->
-        !Config.curr_language = Config.Java
+    | Sil.Sizeof (Sil.Tstruct _, _), Sil.Sizeof (Sil.Tarray _, _)
+      when !Config.curr_language = Config.Java -> true
 
     | Sil.Sizeof (typ1, _), Sil.Sizeof (typ2, _) ->
         (Sil.is_cpp_class typ1 && Sil.is_cpp_class typ2) ||

infer/tests/codetoanalyze/cpp/errors/subtyping/dynamic_cast.cpp

@@ -33,7 +33,6 @@ int wrongCastOfArgumentPointer(){
     return 1/castOfArgumentPointer(&pdd);
 }
 
-//This should give a CLASS_CAST_EXCEPTION error but doesn't yet.
 int wrongCastOfArgumentReference(){
     Base pdd;
     return castOfArgumentReference(pdd);

infer/tests/endtoend/cpp/DynamicCastTest.java

@@ -107,4 +107,14 @@ public class DynamicCastTest {
         contains(CLASS_CAST_EXCEPTION, FILE, "wrongReferenceCastNotAssigned"));
   }
 
+  @Test
+  public void whenInferRunsOnWrongCastOfArgumentReferenceThenClassCastExceptionIsFound()
+      throws InterruptedException, IOException, InferException {
+    InferResults inferResults = InferRunner.runInferCPP(inferCmd);
+    assertThat(
+        "Results should contain class cast exception",
+        inferResults,
+        contains(CLASS_CAST_EXCEPTION, FILE, "wrongCastOfArgumentReference"));
+  }
+
 }