Skip to content

Commit 0d6d3a8

Browse files
committed
Pin CIL with attr-enumerator fix for MacOS
1 parent b9caf63 commit 0d6d3a8

File tree

6 files changed

+7
-7
lines changed

6 files changed

+7
-7
lines changed

goblint.opam

+1-1
Original file line numberDiff line numberDiff line change
@@ -96,7 +96,7 @@ dev-repo: "git+https://github.com/goblint/analyzer.git"
9696
# also remember to generate/adjust goblint.opam.locked!
9797
available: os-family != "bsd" & os-distribution != "alpine" & (arch != "arm64" | os = "macos")
9898
pin-depends: [
99-
[ "goblint-cil.2.0.4" "git+https://github.com/goblint/cil.git#317e26d48b06d5cdc4acff3df1a6824587052b53" ]
99+
[ "goblint-cil.2.0.4" "git+https://github.com/goblint/cil.git#04b8a45a7d20425c7b6c8abe1ad094abc063922b" ]
100100
]
101101
depexts: [
102102
["libgraph-easy-perl"] {os-distribution = "ubuntu" & with-test}

goblint.opam.locked

+1-1
Original file line numberDiff line numberDiff line change
@@ -139,7 +139,7 @@ post-messages: [
139139
pin-depends: [
140140
[
141141
"goblint-cil.2.0.4"
142-
"git+https://github.com/goblint/cil.git#317e26d48b06d5cdc4acff3df1a6824587052b53"
142+
"git+https://github.com/goblint/cil.git#04b8a45a7d20425c7b6c8abe1ad094abc063922b"
143143
]
144144
]
145145
depexts: ["libgraph-easy-perl"] {os-distribution = "ubuntu" & with-test}

goblint.opam.template

+1-1
Original file line numberDiff line numberDiff line change
@@ -2,7 +2,7 @@
22
# also remember to generate/adjust goblint.opam.locked!
33
available: os-family != "bsd" & os-distribution != "alpine" & (arch != "arm64" | os = "macos")
44
pin-depends: [
5-
[ "goblint-cil.2.0.4" "git+https://github.com/goblint/cil.git#317e26d48b06d5cdc4acff3df1a6824587052b53" ]
5+
[ "goblint-cil.2.0.4" "git+https://github.com/goblint/cil.git#04b8a45a7d20425c7b6c8abe1ad094abc063922b" ]
66
]
77
depexts: [
88
["libgraph-easy-perl"] {os-distribution = "ubuntu" & with-test}

src/cdomain/value/cdomains/mutexAttrDomain.ml

+1-1
Original file line numberDiff line numberDiff line change
@@ -25,7 +25,7 @@ let recursive_int = lazy (
2525
let res = ref (Z.of_int 2) in (* Use OS X as the default, it doesn't have the enum *)
2626
GoblintCil.iterGlobals !Cilfacade.current_file (function
2727
| GEnumTag (einfo, _) ->
28-
List.iter (fun (name, exp, _) ->
28+
List.iter (fun (name, _, exp, _) ->
2929
if name = "PTHREAD_MUTEX_RECURSIVE" then
3030
res := Option.get @@ GoblintCil.getInteger exp
3131
) einfo.eitems

src/incremental/compareAST.ml

+2-2
Original file line numberDiff line numberDiff line change
@@ -178,8 +178,8 @@ and eq_typ_acc ?(fun_parameter_name_comparison_enabled: bool = true) (a: typ) (b
178178
if Messages.tracing then Messages.traceu "compareast" "eq_typ_acc %a vs %a" d_type a d_type b;
179179
(r, updated_rename_mapping)
180180

181-
and eq_eitems (a: string * exp * location) (b: string * exp * location) ~(rename_mapping: rename_mapping) ~(acc: (typ * typ) list) = match a, b with
182-
(name1, exp1, _l1), (name2, exp2, _l2) -> (name1 = name2, rename_mapping) &&>> eq_exp exp1 exp2 ~acc
181+
and eq_eitems (a: string * attributes * exp * location) (b: string * attributes * exp * location) ~(rename_mapping: rename_mapping) ~(acc: (typ * typ) list) = match a, b with
182+
(name1, attr1, exp1, _l1), (name2, attr2, exp2, _l2) -> (name1 = name2, rename_mapping) &&>> forward_list_equal (eq_attribute ~acc) attr1 attr2 &&>> eq_exp exp1 exp2 ~acc
183183
(* Ignore location *)
184184

185185
and eq_enuminfo (a: enuminfo) (b: enuminfo) ~(rename_mapping: rename_mapping) ~(acc: (typ * typ) list) =

src/witness/witnessUtil.ml

+1-1
Original file line numberDiff line numberDiff line change
@@ -209,7 +209,7 @@ struct
209209
let typ = TEnum (e, []) in
210210
let name = "enum " ^ ename in
211211
Hashtbl.replace genv name (Cabs2cil.EnvTyp typ, loc);
212-
List.iter (fun (name, exp, loc) ->
212+
List.iter (fun (name, _, exp, loc) ->
213213
Hashtbl.replace genv name (Cabs2cil.EnvEnum (exp, typ), loc)
214214
) eitems
215215
| Cil.GVar (v, _, loc)

0 commit comments

Comments
 (0)