Skip to content

Commit 8268b1d

Browse files
committed
Parallelism: Apply thread-safe Lazy on mutexAttrDomain
Possibly, this could be needed elsewhere, where state is involved
1 parent d1967d5 commit 8268b1d

File tree

2 files changed

+4
-2
lines changed

2 files changed

+4
-2
lines changed

src/cdomain/value/cdomains/mutexAttrDomain.ml

Lines changed: 3 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,5 @@
11
(** Mutex attribute type domain. *)
2+
open Goblint_parallel
23

34
module MutexKind =
45
struct
@@ -21,7 +22,7 @@ end
2122
include Lattice.FlatConf (struct include Printable.DefaultConf let bot_name = "Uninitialized" let top_name = "Top" end) (MutexKind)
2223

2324
(* Needed because OS X is weird and assigns different constants than normal systems... :( *)
24-
let recursive_int = lazy (
25+
let recursive_int = DomainsafeLazy.from_fun (fun () ->
2526
let res = ref (Z.of_int 2) in (* Use OS X as the default, it doesn't have the enum *)
2627
GoblintCil.iterGlobals !Cilfacade.current_file (function
2728
| GEnumTag (einfo, _) ->
@@ -39,7 +40,7 @@ let of_int z =
3940
if Z.equal z Z.zero then
4041
`Lifted MutexKind.NonRec
4142
else
42-
let recursive_int = Lazy.force recursive_int in
43+
let recursive_int = DomainsafeLazy.force recursive_int in
4344
if Z.equal z recursive_int then
4445
`Lifted MutexKind.Recursive
4546
else

src/cdomain/value/dune

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -13,6 +13,7 @@
1313
goblint_library
1414
goblint_domain
1515
goblint_incremental
16+
goblint_parallel
1617
goblint-cil)
1718
(flags :standard -open Goblint_std -open Goblint_logs)
1819
(preprocess

0 commit comments

Comments
 (0)