Fix unsoundness on unknown function call with tid as argument

goblint · Oct 27, 2023 · 2df7882 · 2df7882
1 parent 1221860
commit 2df7882
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/src/cdomains/valueDomain.ml b/src/cdomains/valueDomain.ml
@@ -708,7 +708,7 @@ struct
       let v = invalidate_value ask voidType (CArrays.get ask n (array_idx_top)) in
       Array (CArrays.set ask n (array_idx_top) v)
     |                 t , Blob n       -> Blob (Blobs.invalidate_value ask t n)
-    |                 _ , Thread _     -> state (* TODO: no top thread ID set! *)
+    |                 _ , Thread tid   -> Thread (Threads.join (Threads.top ()) tid)
     |                 _ , JmpBuf _     -> state (* TODO: no top jmpbuf *)
     | _, Bot -> Bot (* Leave uninitialized value (from malloc) alone in free to avoid trashing everything. TODO: sound? *)
     |                 t , _             -> top_value t