Implement widen for threads with int and address similarly to the Add…

…ress and Int case
goblint · Oct 29, 2023 · ae7a406 · ae7a406
1 parent 4cb8c97
commit ae7a406
Showing 1 changed file with 2 additions and 4 deletions.
diff --git a/src/cdomains/valueDomain.ml b/src/cdomains/valueDomain.ml
@@ -583,11 +583,9 @@ struct
     | (Blob x, Blob y) -> Blob (Blobs.widen x y) (* TODO: why no blob special cases like in join? *)
     | (Thread x, Thread y) -> Thread (Threads.widen x y)
     | (Int x, Thread y)
-    | (Thread y, Int x) ->
-      Thread y (* TODO: ignores int! *)
+    | (Thread y, Int x) -> Thread (Threads.widen y (Threads.join y (Threads.top ())))
     | (Address x, Thread y)
-    | (Thread y, Address x) ->
-      Thread y (* TODO: ignores address! *)
+    | (Thread y, Address x) -> Thread (Threads.widen y (Threads.join y (Threads.top ())))
     | (Mutex, Mutex) -> Mutex
     | (JmpBuf x, JmpBuf y) -> JmpBuf (JmpBufs.widen x y)
     | (MutexAttr x, MutexAttr y) -> MutexAttr (MutexAttr.widen x y)