From 0d6d3a8e5911476875464b7b6c402908453d8323 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Fri, 16 Aug 2024 10:19:51 +0300 Subject: [PATCH] Pin CIL with attr-enumerator fix for MacOS --- goblint.opam | 2 +- goblint.opam.locked | 2 +- goblint.opam.template | 2 +- src/cdomain/value/cdomains/mutexAttrDomain.ml | 2 +- src/incremental/compareAST.ml | 4 ++-- src/witness/witnessUtil.ml | 2 +- 6 files changed, 7 insertions(+), 7 deletions(-) diff --git a/goblint.opam b/goblint.opam index b73d2c0329..2ed13448f5 100644 --- a/goblint.opam +++ b/goblint.opam @@ -96,7 +96,7 @@ dev-repo: "git+https://github.com/goblint/analyzer.git" # also remember to generate/adjust goblint.opam.locked! available: os-family != "bsd" & os-distribution != "alpine" & (arch != "arm64" | os = "macos") pin-depends: [ - [ "goblint-cil.2.0.4" "git+https://github.com/goblint/cil.git#317e26d48b06d5cdc4acff3df1a6824587052b53" ] + [ "goblint-cil.2.0.4" "git+https://github.com/goblint/cil.git#04b8a45a7d20425c7b6c8abe1ad094abc063922b" ] ] depexts: [ ["libgraph-easy-perl"] {os-distribution = "ubuntu" & with-test} diff --git a/goblint.opam.locked b/goblint.opam.locked index c629aa6755..a4b9cf6677 100644 --- a/goblint.opam.locked +++ b/goblint.opam.locked @@ -139,7 +139,7 @@ post-messages: [ pin-depends: [ [ "goblint-cil.2.0.4" - "git+https://github.com/goblint/cil.git#317e26d48b06d5cdc4acff3df1a6824587052b53" + "git+https://github.com/goblint/cil.git#04b8a45a7d20425c7b6c8abe1ad094abc063922b" ] ] depexts: ["libgraph-easy-perl"] {os-distribution = "ubuntu" & with-test} diff --git a/goblint.opam.template b/goblint.opam.template index bb70aa29e7..9f29ceb7a5 100644 --- a/goblint.opam.template +++ b/goblint.opam.template @@ -2,7 +2,7 @@ # also remember to generate/adjust goblint.opam.locked! available: os-family != "bsd" & os-distribution != "alpine" & (arch != "arm64" | os = "macos") pin-depends: [ - [ "goblint-cil.2.0.4" "git+https://github.com/goblint/cil.git#317e26d48b06d5cdc4acff3df1a6824587052b53" ] + [ "goblint-cil.2.0.4" "git+https://github.com/goblint/cil.git#04b8a45a7d20425c7b6c8abe1ad094abc063922b" ] ] depexts: [ ["libgraph-easy-perl"] {os-distribution = "ubuntu" & with-test} diff --git a/src/cdomain/value/cdomains/mutexAttrDomain.ml b/src/cdomain/value/cdomains/mutexAttrDomain.ml index ea9696d26f..e12818c2c1 100644 --- a/src/cdomain/value/cdomains/mutexAttrDomain.ml +++ b/src/cdomain/value/cdomains/mutexAttrDomain.ml @@ -25,7 +25,7 @@ let recursive_int = lazy ( let res = ref (Z.of_int 2) in (* Use OS X as the default, it doesn't have the enum *) GoblintCil.iterGlobals !Cilfacade.current_file (function | GEnumTag (einfo, _) -> - List.iter (fun (name, exp, _) -> + List.iter (fun (name, _, exp, _) -> if name = "PTHREAD_MUTEX_RECURSIVE" then res := Option.get @@ GoblintCil.getInteger exp ) einfo.eitems diff --git a/src/incremental/compareAST.ml b/src/incremental/compareAST.ml index 2449cdac47..b62cf28f2f 100644 --- a/src/incremental/compareAST.ml +++ b/src/incremental/compareAST.ml @@ -178,8 +178,8 @@ and eq_typ_acc ?(fun_parameter_name_comparison_enabled: bool = true) (a: typ) (b if Messages.tracing then Messages.traceu "compareast" "eq_typ_acc %a vs %a" d_type a d_type b; (r, updated_rename_mapping) -and eq_eitems (a: string * exp * location) (b: string * exp * location) ~(rename_mapping: rename_mapping) ~(acc: (typ * typ) list) = match a, b with - (name1, exp1, _l1), (name2, exp2, _l2) -> (name1 = name2, rename_mapping) &&>> eq_exp exp1 exp2 ~acc +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 + (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 (* Ignore location *) and eq_enuminfo (a: enuminfo) (b: enuminfo) ~(rename_mapping: rename_mapping) ~(acc: (typ * typ) list) = diff --git a/src/witness/witnessUtil.ml b/src/witness/witnessUtil.ml index 5d22fd1e83..ffadaf14e5 100644 --- a/src/witness/witnessUtil.ml +++ b/src/witness/witnessUtil.ml @@ -209,7 +209,7 @@ struct let typ = TEnum (e, []) in let name = "enum " ^ ename in Hashtbl.replace genv name (Cabs2cil.EnvTyp typ, loc); - List.iter (fun (name, exp, loc) -> + List.iter (fun (name, _, exp, loc) -> Hashtbl.replace genv name (Cabs2cil.EnvEnum (exp, typ), loc) ) eitems | Cil.GVar (v, _, loc)