Replaced type comparison with CilType.Typ.equal

goblint · Sep 16, 2023 · a0a501c · a0a501c
1 parent 1aaec46
commit a0a501c
Showing 1 changed file with 5 additions and 6 deletions.
diff --git a/src/analyses/base.ml b/src/analyses/base.ml
@@ -2075,8 +2075,7 @@ struct
       let s2_a = address_from_value s2_v in
       let s2_typ = AD.type_of s2_a in
       (* compute value in string literals domain if s1 and s2 are both string literals *)
-      (* TODO: comparing types structurally should not be done (use typSig instead!) *)
-      if s1_typ = charPtrType && s2_typ = charPtrType then
+      if CilType.Typ.equal s1_typ charPtrType && CilType.Typ.equal s2_typ charPtrType then
         begin match lv, op_addr with
           | Some lv_val, Some f ->
           (* when whished types coincide, compute result of operation op_addr, otherwise use top *)
@@ -2100,7 +2099,7 @@ struct
           | None -> s1_a, s1_typ in
         begin match (get (Analyses.ask_of_ctx ctx) gs st s1_a None), get (Analyses.ask_of_ctx ctx) gs st s2_a None with
           | Array array_s1, Array array_s2 -> set ~ctx ~blob_destructive:true (Analyses.ask_of_ctx ctx) gs st lv_a lv_typ (op_array array_s1 array_s2)
-          | Array array_s1, _ when s2_typ = charPtrType ->
+          | Array array_s1, _ when CilType.Typ.equal s2_typ charPtrType ->
             let s2_null_bytes = List.map CArrays.to_null_byte_domain (AD.to_string s2_a) in
             let array_s2 = List.fold_left CArrays.join (CArrays.bot ()) s2_null_bytes in
             set ~ctx ~blob_destructive:true (Analyses.ask_of_ctx ctx) gs st lv_a lv_typ (op_array array_s1 array_s2)
@@ -2110,15 +2109,15 @@ struct
             let s_id = ValueDomainQueries.ID.unlift (Fun.id) size in
             let empty_array = CArrays.make (ID.cast_to (Cilfacade.ptrdiff_ikind ()) s_id) (Int (ID.top_of IChar)) in
             set ~ctx (Analyses.ask_of_ctx ctx) gs st lv_a lv_typ (op_array empty_array array_s2)
-          | Bot , _ when s2_typ = charPtrType ->
+          | Bot , _ when CilType.Typ.equal s2_typ charPtrType ->
             (* If we have bot inside here, we assume the blob is used as a char array and create one inside *)
             let size = ctx.ask (Q.BlobSize s1) in
             let s_id = ValueDomainQueries.ID.unlift (Fun.id) size in
             let empty_array = CArrays.make (ID.cast_to (Cilfacade.ptrdiff_ikind ()) s_id) (Int (ID.top_of IChar)) in
             let s2_null_bytes = List.map CArrays.to_null_byte_domain (AD.to_string s2_a) in
             let array_s2 = List.fold_left CArrays.join (CArrays.bot ()) s2_null_bytes in
             set ~ctx (Analyses.ask_of_ctx ctx) gs st lv_a lv_typ (op_array empty_array array_s2)
-          | _, Array array_s2 when s1_typ = charPtrType ->
+          | _, Array array_s2 when CilType.Typ.equal s1_typ charPtrType ->
             (* if s1 is string literal, str(n)cpy and str(n)cat are undefined *)
             if op_addr = None then
               (* triggers warning, function only evaluated for side-effects *)
@@ -2128,7 +2127,7 @@ struct
               let s1_null_bytes = List.map CArrays.to_null_byte_domain (AD.to_string s1_a) in
               let array_s1 = List.fold_left CArrays.join (CArrays.bot ()) s1_null_bytes in
               set ~ctx (Analyses.ask_of_ctx ctx) gs st lv_a lv_typ (op_array array_s1 array_s2)
-          | vals1, _ ->
+          | _ ->
             set ~ctx (Analyses.ask_of_ctx ctx) gs st lv_a lv_typ (VD.top_value (unrollType lv_typ))
         end
     in