[Infer][Java] Handling assert keyword by adding a special case for the $assertionsDisabled field during translation

infer/src/java/jTrans.ml

@@ -577,10 +577,16 @@ let rec expression context pc expr =
         let field_type = (JTransType.get_class_type program tenv (JBasics.make_cn JConfig.string_cl)) in
         JTransStaticField.translate_instr_static_field context callee_procdesc fs field_type loc
       else
-        let sil_expr = Sil.Lfield (sil_expr, field_name, sil_type) in
+        if JTransType.is_autogenerated_assert_field field_name
-        let tmp_id = Ident.create_fresh Ident.knormal in
+        then
-        let lderef_instr = Sil.Letderef (tmp_id, sil_expr, sil_type, loc) in
+          (* assume that reading from C.$assertionsDisabled always yields "false". this allows *)
-        (idl @ [tmp_id], instrs @ [lderef_instr], Sil.Var tmp_id)
+          (* Infer to understand the assert keyword in the expected way *)
+          (idl, instrs, Sil.exp_zero)
+        else
+          let sil_expr = Sil.Lfield (sil_expr, field_name, sil_type) in
+          let tmp_id = Ident.create_fresh Ident.knormal in
+          let lderef_instr = Sil.Letderef (tmp_id, sil_expr, sil_type, loc) in
+          (idl @ [tmp_id], instrs @ [lderef_instr], Sil.Var tmp_id)
 
 let method_invocation context loc pc var_opt cn ms sil_obj_opt expr_list invoke_code is_static =
   let cfg = JContext.get_cfg context in

infer/src/java/jTransType.ml

@@ -342,6 +342,9 @@ let get_class_type program tenv cn =
   let t = get_class_type_no_pointer program tenv cn in
   Sil.Tptr (t, Sil.Pk_pointer)
 
+(** return true if [field_name] is the autogenerated C.$assertionsDisabled field for class C *)
+let is_autogenerated_assert_field field_name =
+  string_equal (Ident.java_fieldname_get_field field_name) "$assertionsDisabled"
 
 (** translate an object type *)
 let rec object_type program tenv ot =

infer/src/java/jTransType.mli

@@ -19,6 +19,9 @@ val get_class_type_no_pointer: JClasspath.program -> Sil.tenv -> JBasics.class_n
 (** [get_class_type tenv cn] returns the sil type representation of the class  *)
 val get_class_type : JClasspath.program -> Sil.tenv -> JBasics.class_name -> Sil.typ
 
+(** return true if [field_name] is the autogenerated C.$assertionsDisabled field for class C *)
+val is_autogenerated_assert_field : Ident.fieldname -> bool
+
 (** transforms a Java object type to a Sil type *)
 val object_type : JClasspath.program -> Sil.tenv -> JBasics.object_type -> Sil.typ