Fix exceptions due to ID ops

goblint · Oct 5, 2023 · 22e4df5 · 22e4df5
1 parent d683281
commit 22e4df5
Show file tree

Hide file tree

Showing 2 changed files with 12 additions and 3 deletions.
diff --git a/src/analyses/base.ml b/src/analyses/base.ml
@@ -2144,7 +2144,11 @@ struct
         | `Lifted ds, `Lifted n ->
           let casted_ds = ID.cast_to (Cilfacade.ptrdiff_ikind ()) ds in
           let casted_n = ID.cast_to (Cilfacade.ptrdiff_ikind ()) n in
-          let ds_eq_n = ID.eq casted_ds casted_n in
+          let ds_eq_n =
+            begin try ID.eq casted_ds casted_n
+              with IntDomain.ArithmeticOnIntegerBot _ -> ID.bot_of @@ Cilfacade.ptrdiff_ikind ()
+            end
+          in
           begin match ID.to_bool ds_eq_n with
             | Some b -> b
             | None -> false

diff --git a/src/analyses/memOutOfBounds.ml b/src/analyses/memOutOfBounds.ml
@@ -184,7 +184,8 @@ struct
             | `Bot -> ID.bot_of @@ Cilfacade.ptrdiff_ikind ()
             | `Lifted eval_x ->
               let typ_size_in_bytes = size_of_type_in_bytes typ in
-              let bytes_offset = ID.mul typ_size_in_bytes eval_x in
+              let casted_eval_x = ID.cast_to (Cilfacade.ptrdiff_ikind ()) eval_x in
+              let bytes_offset = ID.mul typ_size_in_bytes casted_eval_x in
               let remaining_offset = cil_offs_to_idx ctx typ o in
               ID.add bytes_offset remaining_offset
           end
@@ -290,7 +291,11 @@ struct
             let one = intdom_of_int 1 in
             let casted_es = ID.sub casted_es one in
             let casted_offs = ID.cast_to (Cilfacade.ptrdiff_ikind ()) offs_intdom in
-            let ptr_size_lt_offs = ID.lt casted_es casted_offs in
+            let ptr_size_lt_offs =
+              begin try ID.lt casted_es casted_offs
+                with IntDomain.ArithmeticOnIntegerBot _ -> ID.bot_of @@ Cilfacade.ptrdiff_ikind ()
+              end
+            in
             let behavior = Undefined MemoryOutOfBoundsAccess in
             let cwe_number = 823 in
             begin match ID.to_bool ptr_size_lt_offs with