Skip to content

Commit 717b6a8

Browse files
committed
Add pthread_join_N to Klever library
1 parent edf7e6f commit 717b6a8

File tree

1 file changed

+1
-0
lines changed

1 file changed

+1
-0
lines changed

src/analyses/libraryFunctions.ml

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1008,6 +1008,7 @@ let rtnl_lock = AddrOf (Cil.var (Cilfacade.create_var (makeGlobalVar "[rtnl_lock
10081008
(** LDV Klever functions. *)
10091009
let klever_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[
10101010
("pthread_create_N", special [__ "thread" [w]; drop "attr" [r]; __ "start_routine" [s]; __ "arg" []] @@ fun thread start_routine arg -> ThreadCreate { thread; start_routine; arg }); (* TODO: add multiple flag to ThreadCreate *)
1011+
("pthread_join_N", special [__ "thread" []; __ "retval" [w]] @@ fun thread retval -> ThreadJoin {thread; ret_var = retval});
10111012
("ldv_mutex_model_lock", special [__ "lock" []; drop "sign" []] @@ fun lock -> Lock { lock; try_ = get_bool "sem.lock.fail"; write = true; return_on_success = true });
10121013
("ldv_mutex_model_unlock", special [__ "lock" []; drop "sign" []] @@ fun lock -> Unlock lock);
10131014
("ldv_spin_model_lock", unknown [drop "sign" []]);

0 commit comments

Comments
 (0)