mode!=ID_java is trivially true in this branch

This is part of the else { ... } in if(mode==ID_java) { ... } else { ... }

Author: tautschnig

src/analyses/goto_check.cpp

@@ -1029,26 +1029,23 @@ void goto_checkt::pointer_validity_check(
         expr,
         guard);
 
-    if(mode != ID_java)
-    {
-      if(flags.is_unknown() || flags.is_dynamic_heap())
-        add_guarded_claim(
-          not_exprt(deallocated(pointer, ns)),
-          "dereference failure: deallocated dynamic object",
-          "pointer dereference",
-          expr.find_source_location(),
-          expr,
-          guard);
+    if(flags.is_unknown() || flags.is_dynamic_heap())
+      add_guarded_claim(
+        not_exprt(deallocated(pointer, ns)),
+        "dereference failure: deallocated dynamic object",
+        "pointer dereference",
+        expr.find_source_location(),
+        expr,
+        guard);
 
-      if(flags.is_unknown() || flags.is_dynamic_local())
-        add_guarded_claim(
-          not_exprt(dead_object(pointer, ns)),
-          "dereference failure: dead object",
-          "pointer dereference",
-          expr.find_source_location(),
-          expr,
-          guard);
-    }
+    if(flags.is_unknown() || flags.is_dynamic_local())
+      add_guarded_claim(
+        not_exprt(dead_object(pointer, ns)),
+        "dereference failure: dead object",
+        "pointer dereference",
+        expr.find_source_location(),
+        expr,
+        guard);
 
     if(enable_bounds_check)
     {