From 8116086be1f11cc4efd5fe1baecf9a630405f6ca Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Thu, 25 Jul 2024 12:48:31 +0300
Subject: [PATCH 01/24] Add some CHANGES for 2.0.4

---
 CHANGES.md | 5 +++++
 1 file changed, 5 insertions(+)

diff --git a/CHANGES.md b/CHANGES.md
index 1122f4fd0..8aca1ea7c 100644
--- a/CHANGES.md
+++ b/CHANGES.md
@@ -1,3 +1,8 @@
+## 2.0.4 (unreleased)
+* Add `Return` statement expression location (#167).
+* Remove unused `Libmaincil` module (#165).
+* Fix some synthetic locations (#166, #167).
+
 ## 2.0.3
 * Add `asm inline` parsing (#151).
 * Ignore top level qualifiers in `__builtin_types_compatible_p` (#157).

From 7a522fc74d1704cc54044abc0e498bbfa5a8a75f Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Thu, 25 Jul 2024 13:28:47 +0300
Subject: [PATCH 02/24] Add test for assign in attribute (issue #168)

---
 test/small1/attr-assign.c | 7 +++++++
 test/testcil.pl           | 1 +
 2 files changed, 8 insertions(+)
 create mode 100755 test/small1/attr-assign.c

diff --git a/test/small1/attr-assign.c b/test/small1/attr-assign.c
new file mode 100755
index 000000000..8b83facc0
--- /dev/null
+++ b/test/small1/attr-assign.c
@@ -0,0 +1,7 @@
+// From some new MacOS headers: https://github.com/goblint/cil/issues/168
+
+void foo(void) __attribute__((availability(macos,introduced=10.15)));
+
+void foo(void) {
+    return;
+}
diff --git a/test/testcil.pl b/test/testcil.pl
index a33e9af7a..c8bcd082f 100644
--- a/test/testcil.pl
+++ b/test/testcil.pl
@@ -222,6 +222,7 @@ sub addToGroup {
 addTest("test/attr11 _GNUCC=1");
 addTest("test/attr12 _GNUCC=1");
 addTest("test/attr13 _GNUCC=1");
+addTest("test/attr-assign");
 addTest("testrun/packed _GNUCC=1 WARNINGS_ARE_ERRORS=1");
 addTest("test/packed2 _GNUCC=1");
 addTest("test/bitfield");

From 659e310f5e3e8859ba79681ec13bcdc2b08aad32 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Thu, 25 Jul 2024 14:07:14 +0300
Subject: [PATCH 03/24] Add attribute assignment to parser

---
 src/frontc/cparser.mly | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

diff --git a/src/frontc/cparser.mly b/src/frontc/cparser.mly
index db8431cdc..51e813264 100644
--- a/src/frontc/cparser.mly
+++ b/src/frontc/cparser.mly
@@ -1619,8 +1619,12 @@ conditional_attr:
 |   logical_or_attr QUEST conditional_attr COLON conditional_attr
                                           { QUESTION($1, $3, $5) }
 
+assignment_attr:
+    conditional_attr              { $1 }
+|   unary_attr EQ assignment_attr { BINARY(ASSIGN, $1, $3) }
 
-attr: conditional_attr                    { $1 }
+
+attr: assignment_attr                    { $1 }
 ;
 
 attr_list_ne:

From bfb5f545da291a112c051a74b53c517adb64c10e Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Thu, 25 Jul 2024 14:07:25 +0300
Subject: [PATCH 04/24] Add attribute float to parser

---
 src/frontc/cparser.mly | 1 +
 1 file changed, 1 insertion(+)

diff --git a/src/frontc/cparser.mly b/src/frontc/cparser.mly
index 51e813264..9c010cd80 100644
--- a/src/frontc/cparser.mly
+++ b/src/frontc/cparser.mly
@@ -1494,6 +1494,7 @@ primary_attr:
 |   LPAREN attr RPAREN                  { $2 }
 |   IDENT IDENT                          { CALL(VARIABLE (fst $1), [VARIABLE (fst $2)]) }
 |   CST_INT                              { CONSTANT(CONST_INT (fst $1)) }
+|   CST_FLOAT                            { CONSTANT(CONST_FLOAT (fst $1)) }
 |   const_string_or_wstring                 { CONSTANT(fst $1) }
                                            /*(* Const when it appears in
                                               attribute lists, is translated

From 551e46066885f8f6dfb7eccbd4e712c2c09c371a Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Thu, 25 Jul 2024 13:40:47 +0300
Subject: [PATCH 05/24] Add AAssign

---
 src/cil.ml  | 10 ++++++++++
 src/cil.mli |  1 +
 2 files changed, 11 insertions(+)

diff --git a/src/cil.ml b/src/cil.ml
index 4bec87a9c..53bed82eb 100755
--- a/src/cil.ml
+++ b/src/cil.ml
@@ -344,6 +344,7 @@ and attrparam =
   | AAddrOf of attrparam                 (** & a **)
   | AIndex of attrparam * attrparam      (** a1[a2] *)
   | AQuestion of attrparam * attrparam * attrparam (** a1 ? a2 : a3 **)
+  | AAssign of attrparam * attrparam     (** a1 = a2 *)
 
 
 (** Information about a composite type (a struct or a union). Use
@@ -1874,6 +1875,7 @@ let additiveLevel = 60
 let comparativeLevel = 70
 let bitwiseLevel = 75
 let questionLevel = 100
+let assignLevel = 110
 let getParenthLevel (e: exp) =
   match e with
   | Question _ -> questionLevel
@@ -1924,6 +1926,7 @@ let getParenthLevelAttrParam (a: attrparam) =
   | AAddrOf _ -> 30
   | ADot _ | AIndex _ | AStar _ -> 20
   | AQuestion _ -> questionLevel
+  | AAssign _ -> assignLevel
 
 
 let isIntegralType t =
@@ -4423,6 +4426,9 @@ class defaultCilPrinterClass : cilPrinter = object (self)
           self#pAttrParam () a1 ++ text " ? " ++
           self#pAttrParam () a2 ++ text " : " ++
           self#pAttrParam () a3
+    | AAssign (a1, a2) ->
+          self#pAttrParam () a1 ++ text "=" ++
+          self#pAttrParam () a2
 
 
   (* A general way of printing lists of attributes *)
@@ -5561,6 +5567,10 @@ and childrenAttrparam (vis: cilVisitor) (aa: attrparam) : attrparam =
         let e3' = fAttrP e3 in
         if e1' != e1 || e2' != e2 || e3' != e3
         then AQuestion (e1', e2', e3') else aa
+    | AAssign (e1, e2) ->
+      let e1' = fAttrP e1 in
+      let e2' = fAttrP e2 in
+      if e1' != e1 || e2' != e2 then AAssign (e1', e2') else aa
 
 
 let rec visitCilFunction (vis : cilVisitor) (f : fundec) : fundec =
diff --git a/src/cil.mli b/src/cil.mli
index 099b6e8ea..4464d4c20 100644
--- a/src/cil.mli
+++ b/src/cil.mli
@@ -338,6 +338,7 @@ and attrparam =
   | AAddrOf of attrparam                 (** & a **)
   | AIndex of attrparam * attrparam      (** a1[a2] *)
   | AQuestion of attrparam * attrparam * attrparam (** a1 ? a2 : a3 **)
+  | AAssign of attrparam * attrparam     (** a1 = a2 *)
 
 (** {b Structures.} The {!compinfo} describes the definition of a
    structure or union type. Each such {!compinfo} must be defined at the

From e684426a965a7b069de9bae4c8d7ddfc885194a3 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Thu, 25 Jul 2024 14:06:47 +0300
Subject: [PATCH 06/24] Add AAssign to Cabs2cil

---
 src/frontc/cabs2cil.ml | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/src/frontc/cabs2cil.ml b/src/frontc/cabs2cil.ml
index 83d135ac8..b3f6c9173 100644
--- a/src/frontc/cabs2cil.ml
+++ b/src/frontc/cabs2cil.ml
@@ -2940,6 +2940,8 @@ and doAttr (a: A.attribute) : attribute list =
             ABinOp(LAnd, ae aa1, ae aa2)
         | A.BINARY(A.OR, aa1, aa2) ->
             ABinOp(LOr, ae aa1, ae aa2)
+        | A.BINARY(A.ASSIGN, aa1, aa2) ->
+            AAssign(ae aa1, ae aa2)
         | A.BINARY(abop, aa1, aa2) ->
             ABinOp (convBinOp abop, ae aa1, ae aa2)
         | A.UNARY(A.PLUS, aa) -> ae aa

From ce1c7f7f6f1db90061ac6ff7caaf4e5fb2d71028 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Fri, 26 Jul 2024 10:50:43 +0300
Subject: [PATCH 07/24] Add float attributes to Cabs2cil

---
 src/frontc/cabs2cil.ml | 1 +
 1 file changed, 1 insertion(+)

diff --git a/src/frontc/cabs2cil.ml b/src/frontc/cabs2cil.ml
index b3f6c9173..85dd9c092 100644
--- a/src/frontc/cabs2cil.ml
+++ b/src/frontc/cabs2cil.ml
@@ -2927,6 +2927,7 @@ and doAttr (a: A.attribute) : attribute list =
             | _ ->
                 E.s (error "Invalid attribute constant: %s")
           end
+        | A.CONSTANT (A.CONST_FLOAT str) -> ACons (str, [])
         | A.CALL(A.VARIABLE n, args) -> begin
             let n' = if strip then stripUnderscore n else n in
             let ae' = Util.list_map ae args in

From a1b28f2b696e1ad74b2bf9c81db8f979a0fd444f Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Thu, 25 Jul 2024 14:21:16 +0300
Subject: [PATCH 08/24] Comment out attr-assign test

---
 test/testcil.pl | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/test/testcil.pl b/test/testcil.pl
index c8bcd082f..be107b9d7 100644
--- a/test/testcil.pl
+++ b/test/testcil.pl
@@ -222,7 +222,7 @@ sub addToGroup {
 addTest("test/attr11 _GNUCC=1");
 addTest("test/attr12 _GNUCC=1");
 addTest("test/attr13 _GNUCC=1");
-addTest("test/attr-assign");
+# addTest("test/attr-assign"); # TODO: only on OSX, Linux GCC errors on introduced
 addTest("testrun/packed _GNUCC=1 WARNINGS_ARE_ERRORS=1");
 addTest("test/packed2 _GNUCC=1");
 addTest("test/bitfield");

From 70a430312f6e93acf4f59af08ac65a225dc62852 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Thu, 25 Jul 2024 17:46:45 +0300
Subject: [PATCH 09/24] Disable some GCC 14 errors in tests

---
 test/Makefile | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/test/Makefile b/test/Makefile
index 27f09f2b8..189d391b8 100644
--- a/test/Makefile
+++ b/test/Makefile
@@ -127,6 +127,9 @@ ifdef SEPARATE
   CILLY+= --nomerge
 endif
 
+# Disable GCC 14 new warnings as errors because some tests contain them
+CFLAGS += -Wno-error=implicit-int -Wno-error=implicit-function-declaration -Wno-error=int-conversion -Wno-error=incompatible-pointer-types
+
 # sm: this will make gcc warnings into errors; it's almost never
 # what we want, but for a particular testcase (combine_copyptrs)
 # I need it to show the difference between something which works

From 453a777040c7c1aee8a4b1d511d73491a249d03f Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Fri, 26 Jul 2024 10:45:42 +0300
Subject: [PATCH 10/24] Add availability attribute with multiple dots to test

---
 test/small1/attr-assign.c | 7 +++++++
 1 file changed, 7 insertions(+)

diff --git a/test/small1/attr-assign.c b/test/small1/attr-assign.c
index 8b83facc0..ae7712d98 100755
--- a/test/small1/attr-assign.c
+++ b/test/small1/attr-assign.c
@@ -5,3 +5,10 @@ void foo(void) __attribute__((availability(macos,introduced=10.15)));
 void foo(void) {
     return;
 }
+
+// Version numbers may have multiple dots: https://github.com/goblint/cil/pull/171#issuecomment-2250670652
+void bar(void) __attribute__((availability(macos,introduced=10.13.4)));
+
+void bar(void) {
+    return;
+}

From f441f5496b41d249bbe848c9d90a459c9dcf9255 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Fri, 26 Jul 2024 10:52:13 +0300
Subject: [PATCH 11/24] Add hack for parsing version numbers with multiple dots

---
 src/frontc/cparser.mly | 1 +
 1 file changed, 1 insertion(+)

diff --git a/src/frontc/cparser.mly b/src/frontc/cparser.mly
index 9c010cd80..4983a3c37 100644
--- a/src/frontc/cparser.mly
+++ b/src/frontc/cparser.mly
@@ -1495,6 +1495,7 @@ primary_attr:
 |   IDENT IDENT                          { CALL(VARIABLE (fst $1), [VARIABLE (fst $2)]) }
 |   CST_INT                              { CONSTANT(CONST_INT (fst $1)) }
 |   CST_FLOAT                            { CONSTANT(CONST_FLOAT (fst $1)) }
+|   CST_FLOAT CST_FLOAT                  { CONSTANT(CONST_FLOAT (fst $1 ^ fst $2)) } /* Clang-like hack to parse version numbers like "10.13.4" (https://github.com/goblint/cil/pull/171#issuecomment-2250670652). We lex them as "10.13" and ".4". */
 |   const_string_or_wstring                 { CONSTANT(fst $1) }
                                            /*(* Const when it appears in
                                               attribute lists, is translated

From ac3a40a5dbafd3e12d080526f0ed44061cf52548 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Fri, 26 Jul 2024 11:25:02 +0300
Subject: [PATCH 12/24] Exclude nonsense kernel1 test

---
 test/small2/kernel1.c | 2 +-
 test/testcil.pl       | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/test/small2/kernel1.c b/test/small2/kernel1.c
index 46c2673f7..05f8814d2 100644
--- a/test/small2/kernel1.c
+++ b/test/small2/kernel1.c
@@ -1,4 +1,4 @@
-
+// This test is nonsense: DECLARE_WAIT_QUEUE_HEAD is a macro in Linux kernel
 DECLARE_WAIT_QUEUE_HEAD(log_wait);
 
 
diff --git a/test/testcil.pl b/test/testcil.pl
index be107b9d7..64c8c1a97 100644
--- a/test/testcil.pl
+++ b/test/testcil.pl
@@ -658,7 +658,7 @@ sub addToGroup {
 addBadComment("scott/globalprob", "Notbug. Not a bug if fails on a non-Linux machine ;-)");
 addTest("scott/bisonerror $gcc");
 addTest("scott/cmpzero");
-addTest("scott/kernel1 $gcc");
+# addTest("scott/kernel1 $gcc");
 addTest("scott/kernel2 $gcc");
 addTest("scott/xcheckers $gcc");
 addTest("scott/memberofptr $gcc");

From 8f9b0c660a020308b12e15276ad9a82cc9a64c9f Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Fri, 26 Jul 2024 11:04:12 +0300
Subject: [PATCH 13/24] Make available on arm64

---
 goblint-cil.opam          | 2 +-
 goblint-cil.opam.template | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/goblint-cil.opam b/goblint-cil.opam
index cf5377505..2cac855a5 100644
--- a/goblint-cil.opam
+++ b/goblint-cil.opam
@@ -64,4 +64,4 @@ depexts: [
   ["perl-FindBin"] {os-distribution = "fedora"}
   ["build-base"] {os-distribution = "alpine"}
 ]
-available: arch = "x86_64"
+available: arch = "x86_64" | arch = "arm64"
diff --git a/goblint-cil.opam.template b/goblint-cil.opam.template
index e98127179..f48259706 100644
--- a/goblint-cil.opam.template
+++ b/goblint-cil.opam.template
@@ -3,4 +3,4 @@ depexts: [
   ["perl-FindBin"] {os-distribution = "fedora"}
   ["build-base"] {os-distribution = "alpine"}
 ]
-available: arch = "x86_64"
+available: arch = "x86_64" | arch = "arm64"

From 8dd4983910013a117596e9fa34a9803decf0c4f0 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Tue, 30 Jul 2024 10:41:04 +0300
Subject: [PATCH 14/24] Add availability attribute to CHANGES for 2.0.4

---
 CHANGES.md | 1 +
 1 file changed, 1 insertion(+)

diff --git a/CHANGES.md b/CHANGES.md
index 8aca1ea7c..12b21c399 100644
--- a/CHANGES.md
+++ b/CHANGES.md
@@ -1,5 +1,6 @@
 ## 2.0.4 (unreleased)
 * Add `Return` statement expression location (#167).
+* Add `availability` attribute support (#168, #171).
 * Remove unused `Libmaincil` module (#165).
 * Fix some synthetic locations (#166, #167).
 

From 317e26d48b06d5cdc4acff3df1a6824587052b53 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Tue, 30 Jul 2024 10:42:22 +0300
Subject: [PATCH 15/24] Bump version to 2.0.4

---
 CHANGES.md                | 2 +-
 META.goblint-cil.template | 4 ++--
 README.md                 | 2 +-
 dune-project              | 2 +-
 goblint-cil.opam          | 2 +-
 5 files changed, 6 insertions(+), 6 deletions(-)

diff --git a/CHANGES.md b/CHANGES.md
index 12b21c399..e0b9d1d51 100644
--- a/CHANGES.md
+++ b/CHANGES.md
@@ -1,4 +1,4 @@
-## 2.0.4 (unreleased)
+## 2.0.4
 * Add `Return` statement expression location (#167).
 * Add `availability` attribute support (#168, #171).
 * Remove unused `Libmaincil` module (#165).
diff --git a/META.goblint-cil.template b/META.goblint-cil.template
index e5aba4bb2..cf051e8fe 100644
--- a/META.goblint-cil.template
+++ b/META.goblint-cil.template
@@ -2,10 +2,10 @@
 
 package "default-features" (
 requires="goblint-cil.dataslicing goblint-cil.liveness goblint-cil.pta goblint-cil.makecfg goblint-cil.syntacticsearch"
-version = "2.0.3"
+version = "2.0.4"
 )
 
 package "all-features" (
 requires="goblint-cil.dataslicing goblint-cil.liveness goblint-cil.pta goblint-cil.makecfg goblint-cil.zrapp goblint-cil.syntacticsearch"
-version = "2.0.3"
+version = "2.0.4"
 )
diff --git a/README.md b/README.md
index 2fc45c67f..049e27287 100644
--- a/README.md
+++ b/README.md
@@ -84,7 +84,7 @@ instance in the OCaml toplevel using [Findlib][findlib]:
     # #require "goblint-cil";;
     [...]
     # GoblintCil.cilVersion;;
-    - : string = "2.0.3"
+    - : string = "2.0.4"
 
 [findlib]: http://projects.camlcity.org/projects/findlib.html
 
diff --git a/dune-project b/dune-project
index b6e92840b..e0929b4e5 100644
--- a/dune-project
+++ b/dune-project
@@ -2,7 +2,7 @@
 (name goblint-cil)
 (implicit_transitive_deps false)
 (generate_opam_files true)
-(version 2.0.3)
+(version 2.0.4)
 (source (github goblint/cil))
 ; (documentation "https://goblint.github.io/cil")
 (authors "George Necula" "Scott McPeak" "Westley Weimer" "Gabriel Kerneis" "Ralf Vogler" "Michael Schwarz" "Simmo Saan")
diff --git a/goblint-cil.opam b/goblint-cil.opam
index 2cac855a5..17e39f5a1 100644
--- a/goblint-cil.opam
+++ b/goblint-cil.opam
@@ -1,6 +1,6 @@
 # This file is generated by dune, edit dune-project instead
 opam-version: "2.0"
-version: "2.0.3"
+version: "2.0.4"
 synopsis:
   "A front-end for the C programming language that facilitates program analysis and transformation"
 description: """

From f3f2177c936dd4d6136ebe9c2ed5fce3ad3c7855 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Fri, 2 Aug 2024 16:44:14 +0300
Subject: [PATCH 16/24] Add test for enumerator attributes

---
 test/small1/attr-enumerator.c | 8 ++++++++
 test/testcil.pl               | 1 +
 2 files changed, 9 insertions(+)
 create mode 100755 test/small1/attr-enumerator.c

diff --git a/test/small1/attr-enumerator.c b/test/small1/attr-enumerator.c
new file mode 100755
index 000000000..2c8f55ecd
--- /dev/null
+++ b/test/small1/attr-enumerator.c
@@ -0,0 +1,8 @@
+// From some new MacOS headers
+
+enum {
+    A,
+    B __attribute__((availability(macos,introduced=10.15))),
+    C = 5,
+    D __attribute__((availability(macos,introduced=10.15))) = 7
+} E;
diff --git a/test/testcil.pl b/test/testcil.pl
index 64c8c1a97..db75b5b4c 100644
--- a/test/testcil.pl
+++ b/test/testcil.pl
@@ -223,6 +223,7 @@ sub addToGroup {
 addTest("test/attr12 _GNUCC=1");
 addTest("test/attr13 _GNUCC=1");
 # addTest("test/attr-assign"); # TODO: only on OSX, Linux GCC errors on introduced
+# addTest("test/attr-enumerator"); # TODO: only on OSX, Linux GCC errors on introduced
 addTest("testrun/packed _GNUCC=1 WARNINGS_ARE_ERRORS=1");
 addTest("test/packed2 _GNUCC=1");
 addTest("test/bitfield");

From 53872de30467909c5e8c57c9f91e8b59e1f5ae4e Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Fri, 2 Aug 2024 16:52:17 +0300
Subject: [PATCH 17/24] Add enumerator attributes to parser and Cabs

---
 src/frontc/cabs.ml      | 2 +-
 src/frontc/cabs2cil.ml  | 6 +++---
 src/frontc/cabsvisit.ml | 4 ++--
 src/frontc/cparser.mly  | 4 ++--
 src/frontc/cprint.ml    | 3 ++-
 5 files changed, 10 insertions(+), 9 deletions(-)

diff --git a/src/frontc/cabs.ml b/src/frontc/cabs.ml
index 7a9db7b14..4ac432e04 100644
--- a/src/frontc/cabs.ml
+++ b/src/frontc/cabs.ml
@@ -168,7 +168,7 @@ and init_name = name * init_expression
 and single_name = specifier * name
 
 
-and enum_item = string * expression * cabsloc
+and enum_item = string * attribute list * expression * cabsloc
 
 (*
 ** Declaration definition (at toplevel)
diff --git a/src/frontc/cabs2cil.ml b/src/frontc/cabs2cil.ml
index 85dd9c092..686acb5e4 100644
--- a/src/frontc/cabs2cil.ml
+++ b/src/frontc/cabs2cil.ml
@@ -2675,7 +2675,7 @@ let rec doSpecList (suggestedAnonName: string) (* This string will be part of
     | [A.Tenum (n, Some eil, extraAttrs)] -> (* A definition of an enum *)
         let rec justNames eil = match eil with
             [] -> []
-          | (str, expr, loc) :: eis -> str :: justNames eis
+          | (str, attrs, expr, loc) :: eis -> str :: justNames eis (* TODO: use attrs *)
         in
         let names = justNames eil in
         let n' =
@@ -2736,11 +2736,11 @@ let rec doSpecList (suggestedAnonName: string) (* This string will be part of
 
         and loop i = function
             [] -> []
-          | (kname, A.NOTHING, cloc) :: rest ->
+          | (kname, attrs, A.NOTHING, cloc) :: rest -> (* TODO: use attrs *)
               (* use the passed-in 'i' as the value, since none specified *)
               processName kname i (convLoc cloc) rest
 
-          | (kname, e, cloc) :: rest ->
+          | (kname, attrs, e, cloc) :: rest -> (* TODO: use attrs *)
               (* constant-eval 'e' to determine tag value *)
               let e' = getIntConstExp e in
               let e'' =
diff --git a/src/frontc/cabsvisit.ml b/src/frontc/cabsvisit.ml
index 85d44f933..6fc8dce74 100644
--- a/src/frontc/cabsvisit.ml
+++ b/src/frontc/cabsvisit.ml
@@ -198,9 +198,9 @@ and childrenTypeSpecifier vis ts =
       let fg' = mapNoCopy childrenFieldGroup fg in
       if fg' != fg then Tunion( n, Some fg', extraAttrs) else ts
   | Tenum (n, Some ei, extraAttrs) ->
-      let doOneEnumItem ((s, e, loc) as ei) =
+      let doOneEnumItem ((s, attrs, e, loc) as ei) =
         let e' = visitCabsExpression vis e in
-        if e' != e then (s, e', loc) else ei
+        if e' != e then (s, attrs, e', loc) else ei (* TODO: visit attrs? *)
       in
       vis#vEnterScope ();
       let ei' = mapNoCopy doOneEnumItem ei in
diff --git a/src/frontc/cparser.mly b/src/frontc/cparser.mly
index 4983a3c37..039162895 100644
--- a/src/frontc/cparser.mly
+++ b/src/frontc/cparser.mly
@@ -1188,8 +1188,8 @@ enum_list: /* (* ISO 6.7.2.2 *) */
 |   enum_list COMMA error               { $1 }
 ;
 enumerator:
-    IDENT			{(fst $1, NOTHING, snd $1)}
-|   IDENT EQ expression		{(fst $1, fst $3, snd $1)}
+    IDENT attributes			{(fst $1, $2, NOTHING, snd $1)}
+|   IDENT attributes EQ expression		{(fst $1, $2, fst $4, snd $1)}
 ;
 
 
diff --git a/src/frontc/cprint.ml b/src/frontc/cprint.ml
index 2ea32fce6..4194cb051 100644
--- a/src/frontc/cprint.ml
+++ b/src/frontc/cprint.ml
@@ -262,10 +262,11 @@ and print_enum_items items =
     indent ();
     print_commas
       true
-      (fun (id, exp, loc) -> print id;
+      (fun (id, attrs, exp, loc) -> print id;
 	if exp = NOTHING then ()
 	else begin
 	  space ();
+    print_attributes attrs;
 	  print "= ";
 	  print_expression exp
 	end)

From ead4987b9f873b5c9da99b181e20a235b63e93af Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Fri, 2 Aug 2024 17:04:14 +0300
Subject: [PATCH 18/24] Add enumerator attributes to CIL

---
 src/check.ml           |  2 +-
 src/cil.ml             | 10 ++++++----
 src/cil.mli            |  2 +-
 src/ext/zrapp/zrapp.ml |  6 ++++--
 src/frontc/cabs2cil.ml | 14 +++++++-------
 src/mergecil.ml        |  6 +++---
 6 files changed, 22 insertions(+), 18 deletions(-)

diff --git a/src/check.ml b/src/check.ml
index 06a030223..1fc37396f 100644
--- a/src/check.ml
+++ b/src/check.ml
@@ -390,7 +390,7 @@ and checkEnumInfo (isadef: defuse) enum =
     (* Add it to the map before we go on *)
     H.add enumUsed enum.ename (enum, ref isadef);
     checkAttributes enum.eattr;
-    List.iter (fun (tn, _, _) -> defineName tn) enum.eitems;
+    List.iter (fun (tn, attrs, _, _) -> defineName tn; checkAttributes attrs) enum.eitems;
   end
 
 and checkTypeInfo (isadef: defuse) ti =
diff --git a/src/cil.ml b/src/cil.ml
index 53bed82eb..b40466fe8 100755
--- a/src/cil.ml
+++ b/src/cil.ml
@@ -399,7 +399,7 @@ and fieldinfo = {
     enumeration. Make sure you have a [GEnumTag] for each of of these.   *)
 and enuminfo = {
     mutable ename: string;              (** The name. Always non-empty *)
-    mutable eitems: (string * exp * location) list; (** Items with names
+    mutable eitems: (string * attributes * exp * location) list; (** Items with names
                                                       and values. This list
                                                       should be
                                                       non-empty. The item
@@ -4014,8 +4014,10 @@ class defaultCilPrinterClass : cilPrinter = object (self)
           text "enum" ++ align ++ text (" " ^ enum.ename) ++
           text " {" ++ line
           ++ (docList ~sep:(chr ',' ++ line)
-                (fun (n,i, loc) ->
-                  text (n ^ " = ")
+                (fun (n, attrs, i, loc) ->
+                  text n
+                    ++ self#pAttrs () attrs
+                    ++ text (n ^ " = ")
                     ++ self#pExp () i)
                 () enum.eitems)
           ++ unalign ++ line ++ text "} "
@@ -5622,7 +5624,7 @@ and childrenGlobal (vis: cilVisitor) (g: global) : global =
   | GEnumTag (enum, _) ->
       (* (trace "visit" (dprintf "visiting global enum %s\n" enum.ename)); *)
       (* Do the values and attributes of the enumerated items *)
-      let itemVisit (name, exp, loc) = (name, visitCilExpr vis exp, loc) in
+      let itemVisit (name, attrs, exp, loc) = (name, visitCilAttributes vis attrs, visitCilExpr vis exp, loc) in
       enum.eitems <- mapNoCopy itemVisit enum.eitems;
       enum.eattr <- visitCilAttributes vis enum.eattr;
       g
diff --git a/src/cil.mli b/src/cil.mli
index 4464d4c20..d63e5535f 100644
--- a/src/cil.mli
+++ b/src/cil.mli
@@ -423,7 +423,7 @@ and fieldinfo = {
 and enuminfo = {
     mutable ename: string;
     (** The name. Always non-empty. *)
-    mutable eitems: (string * exp * location) list;
+    mutable eitems: (string * attributes * exp * location) list;
     (** Items with names and values. This list should be non-empty. The item
        values must be compile-time constants. *)
     mutable eattr: attributes;
diff --git a/src/ext/zrapp/zrapp.ml b/src/ext/zrapp/zrapp.ml
index a1fd7e498..bd3fef444 100644
--- a/src/ext/zrapp/zrapp.ml
+++ b/src/ext/zrapp/zrapp.ml
@@ -412,8 +412,10 @@ class zraCilPrinterClass : cilPrinter = object (self)
           text "enum" ++ align ++ text (" " ^ enum.ename) ++
           self#pAttrs () enum.eattr ++ text " {" ++ line
           ++ (docList ~sep:(chr ',' ++ line)
-                (fun (n,i, loc) ->
-                  text (n ^ " = ")
+                (fun (n, attrs, i, loc) ->
+                  text n
+                    ++ self#pAttrs () attrs
+                    ++ text (n ^ " = ")
                     ++ self#pExp () i)
                 () enum.eitems)
           ++ unalign ++ line ++ text "};\n"
diff --git a/src/frontc/cabs2cil.ml b/src/frontc/cabs2cil.ml
index 686acb5e4..707612f6b 100644
--- a/src/frontc/cabs2cil.ml
+++ b/src/frontc/cabs2cil.ml
@@ -2675,7 +2675,7 @@ let rec doSpecList (suggestedAnonName: string) (* This string will be part of
     | [A.Tenum (n, Some eil, extraAttrs)] -> (* A definition of an enum *)
         let rec justNames eil = match eil with
             [] -> []
-          | (str, attrs, expr, loc) :: eis -> str :: justNames eis (* TODO: use attrs *)
+          | (str, attrs, expr, loc) :: eis -> str :: justNames eis
         in
         let names = justNames eil in
         let n' =
@@ -2721,7 +2721,7 @@ let rec doSpecList (suggestedAnonName: string) (* This string will be part of
           else IULongLong (* assume there can be not enum constants that don't fit in long long since there can only be 128bit constants if long long is also 128bit *)
         in
         (* as each name,value pair is determined, this is called *)
-        let rec processName kname (i: exp) loc rest = begin
+        let rec processName kname attrs (i: exp) loc rest = begin
           (* add the name to the environment, but with a faked 'typ' field;
              we don't know the full type yet (since that includes all of the
              tag values), but we won't need them in here  *)
@@ -2731,16 +2731,16 @@ let rec doSpecList (suggestedAnonName: string) (* This string will be part of
             environment when we're finished  *)
           let newname, _  = newAlphaName true "" kname in
 
-          (kname, (newname, i, loc)) :: loop (increm i 1) rest
+          (kname, (newname, doAttributes attrs, i, loc)) :: loop (increm i 1) rest
         end
 
         and loop i = function
             [] -> []
-          | (kname, attrs, A.NOTHING, cloc) :: rest -> (* TODO: use attrs *)
+          | (kname, attrs, A.NOTHING, cloc) :: rest ->
               (* use the passed-in 'i' as the value, since none specified *)
-              processName kname i (convLoc cloc) rest
+              processName kname attrs i (convLoc cloc) rest
 
-          | (kname, attrs, e, cloc) :: rest -> (* TODO: use attrs *)
+          | (kname, attrs, e, cloc) :: rest ->
               (* constant-eval 'e' to determine tag value *)
               let e' = getIntConstExp e in
               let e'' =
@@ -2750,7 +2750,7 @@ let rec doSpecList (suggestedAnonName: string) (* This string will be part of
 		                if !lowerConstants then kintegerCilint ik n else e'
                 | _ -> E.s (error "Constant initializer %a not an integer" d_exp e')
               in
-              processName kname e'' (convLoc cloc) rest
+              processName kname attrs e'' (convLoc cloc) rest
         in
 
         let fields = loop zero eil in
diff --git a/src/mergecil.ml b/src/mergecil.ml
index 028649c7b..04801c0f9 100644
--- a/src/mergecil.ml
+++ b/src/mergecil.ml
@@ -701,7 +701,7 @@
        (* We check that they are defined in the same way. This is a fairly
             conservative check. *)
        List.iter2
-         (fun (old_iname, old_iv, _) (iname, iv, _) ->
+         (fun (old_iname, old_attrs, old_iv, _) (iname, attrs, iv, _) -> (* TODO: combine attributes somewhere? *)
            if old_iname <> iname then
              raise (Failure "(different names for enumeration items)");
            let samev =
@@ -1545,12 +1545,12 @@
                     as the variables *)
                  ei.eitems <-
                    Util.list_map
-                     (fun (n, i, loc) ->
+                     (fun (n, attrs, i, loc) ->
                        let newname, _ =
                          A.newAlphaName ~alphaTable:vtAlpha ~undolist:None
                            ~lookupname:n ~data:!currentLoc
                        in
-                       (newname, i, loc))
+                       (newname, attrs, i, loc))
                      ei.eitems;
                  mergePushGlobals (visitCilGlobal renameVisitor g)
              | Some (ei', _) ->

From 0d21b3479f1416417d667ad9a6cec8c5ded1fe9b Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Fri, 2 Aug 2024 17:17:36 +0300
Subject: [PATCH 19/24] Fix enumerator attribute merging like fieldinfo merging

---
 src/mergecil.ml | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/src/mergecil.ml b/src/mergecil.ml
index 04801c0f9..6de3abc4a 100644
--- a/src/mergecil.ml
+++ b/src/mergecil.ml
@@ -701,9 +701,11 @@
        (* We check that they are defined in the same way. This is a fairly
             conservative check. *)
        List.iter2
-         (fun (old_iname, old_attrs, old_iv, _) (iname, attrs, iv, _) -> (* TODO: combine attributes somewhere? *)
+         (fun (old_iname, old_attrs, old_iv, _) (iname, attrs, iv, _) ->
            if old_iname <> iname then
              raise (Failure "(different names for enumeration items)");
+           if old_attrs <> attrs then
+             raise (Failure "(different enumerator attributes)");
            let samev =
              match (constFold true old_iv, constFold true iv) with
              | Const (CInt (oldi, _, _)), Const (CInt (i, _, _)) ->

From 04b8a45a7d20425c7b6c8abe1ad094abc063922b Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Fri, 2 Aug 2024 17:28:36 +0300
Subject: [PATCH 20/24] Visit enumerator attributes in Cabsvisit

---
 src/frontc/cabsvisit.ml | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/src/frontc/cabsvisit.ml b/src/frontc/cabsvisit.ml
index 6fc8dce74..444392e58 100644
--- a/src/frontc/cabsvisit.ml
+++ b/src/frontc/cabsvisit.ml
@@ -199,8 +199,9 @@ and childrenTypeSpecifier vis ts =
       if fg' != fg then Tunion( n, Some fg', extraAttrs) else ts
   | Tenum (n, Some ei, extraAttrs) ->
       let doOneEnumItem ((s, attrs, e, loc) as ei) =
+        let attrs' = visitCabsAttributes vis attrs in
         let e' = visitCabsExpression vis e in
-        if e' != e then (s, attrs, e', loc) else ei (* TODO: visit attrs? *)
+        if attrs' != attrs || e' != e then (s, attrs', e', loc) else ei
       in
       vis#vEnterScope ();
       let ei' = mapNoCopy doOneEnumItem ei in

From 73d02511a0366816d428853634fb939bd2f0a1b7 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Tue, 24 Sep 2024 11:05:15 +0300
Subject: [PATCH 21/24] Generate 32bit and 64bit Machdep if possible

The -m32 and -m64 arguments are x86-only, so these have to be optional.
---
 src/dune                    | 18 +++++++++++++++++-
 src/machdep.cppo.ml         |  7 +++++++
 src/machdepArchConfigure.ml | 20 ++++++++++++++++++++
 3 files changed, 44 insertions(+), 1 deletion(-)
 create mode 100644 src/machdepArchConfigure.ml

diff --git a/src/dune b/src/dune
index 6b3766013..09b365c02 100644
--- a/src/dune
+++ b/src/dune
@@ -4,7 +4,7 @@
   (public_name goblint-cil)
   (name goblintCil)
   (libraries zarith findlib dynlink unix str stdlib-shims)
-  (modules (:standard \ main ciloptions machdepConfigure modelConfigure))
+  (modules (:standard \ main ciloptions machdepConfigure machdepArchConfigure modelConfigure))
 )
 
 (executable
@@ -21,6 +21,21 @@
  (target machdep-ml.exe)
  (action (run %{read-lines:../bin/real-gcc} -D_GNUCC machdep-ml.c -o %{target})))
 
+(executable
+ (name machdepArchConfigure)
+ (modules machdepArchConfigure)
+ (libraries dune-configurator))
+
+(rule
+ (deps machdep-config.h machdep-ml.c)
+ (target machdep32)
+ (action (with-stdout-to %{target} (run ./machdepArchConfigure.exe --real-gcc %{read-lines:../bin/real-gcc} -m 32))))
+
+(rule
+ (deps machdep-config.h machdep-ml.c)
+ (target machdep64)
+ (action (with-stdout-to %{target} (run ./machdepArchConfigure.exe --real-gcc %{read-lines:../bin/real-gcc} -m 64))))
+
 ; for Cilly.pm
 (executable
  (name modelConfigure)
@@ -40,6 +55,7 @@
  (action (with-stdout-to %{target} (run ./modelConfigure.exe --real-gcc %{read-lines:../bin/real-gcc} -m 64))))
 
 (rule
+ (deps machdep32 machdep64)
  (target machdep.ml)
  (action (run %{bin:cppo} -V OCAML:%{ocaml_version}
               %{dep:machdep.cppo.ml} -x machdep:./%{dep:machdep-ml.exe}
diff --git a/src/machdep.cppo.ml b/src/machdep.cppo.ml
index 45d734e93..b00ef8cfc 100644
--- a/src/machdep.cppo.ml
+++ b/src/machdep.cppo.ml
@@ -56,4 +56,11 @@ let gcc = {
 #ext machdep
 #endext
 }
+
+let gcc32 =
+#include "machdep32"
+
+let gcc64 =
+#include "machdep64"
+
 let theMachine : mach ref = ref gcc
diff --git a/src/machdepArchConfigure.ml b/src/machdepArchConfigure.ml
new file mode 100644
index 000000000..ebf4ee0e7
--- /dev/null
+++ b/src/machdepArchConfigure.ml
@@ -0,0 +1,20 @@
+module C = Configurator.V1
+
+let () =
+  let real_gcc = ref "" in
+  let m = ref "" in
+  let args = Arg.[
+      ("--real-gcc", Set_string real_gcc, "");
+      ("-m", Set_string m, "");
+    ]
+  in
+  C.main ~name:"model" ~args (fun c ->
+      let exe = "./machdep-ml" ^ !m ^ ".exe" in
+      let {C.Process.exit_code; stdout; stderr} = C.Process.run c !real_gcc ["-D_GNUCC"; "-m" ^ !m; "machdep-ml.c"; "-o"; exe] in
+      if exit_code = 0 then (
+        let {C.Process.stdout; stderr; exit_code} = C.Process.run c exe [] in
+        Printf.printf "Some {%s}" stdout
+      )
+      else 
+        Printf.printf "None"
+    )

From 72829a316bd35a1317dd715c6fc412d49c5873e5 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Wed, 25 Sep 2024 15:32:40 +0300
Subject: [PATCH 22/24] Change machdepArchConfigure compiled output name to
 avoid potential conflict with modelConfigure

---
 src/machdepArchConfigure.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/machdepArchConfigure.ml b/src/machdepArchConfigure.ml
index ebf4ee0e7..95ed6a22e 100644
--- a/src/machdepArchConfigure.ml
+++ b/src/machdepArchConfigure.ml
@@ -9,7 +9,7 @@ let () =
     ]
   in
   C.main ~name:"model" ~args (fun c ->
-      let exe = "./machdep-ml" ^ !m ^ ".exe" in
+      let exe = "./machdep" ^ !m ^ "-ml.exe" in
       let {C.Process.exit_code; stdout; stderr} = C.Process.run c !real_gcc ["-D_GNUCC"; "-m" ^ !m; "machdep-ml.c"; "-o"; exe] in
       if exit_code = 0 then (
         let {C.Process.stdout; stderr; exit_code} = C.Process.run c exe [] in

From 9f4fac450c02bc61a13717784515056b185794cd Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Wed, 25 Sep 2024 15:33:12 +0300
Subject: [PATCH 23/24] Assert machdep-ml exit code to be 0

---
 src/machdepArchConfigure.ml | 1 +
 src/modelConfigure.ml       | 1 +
 2 files changed, 2 insertions(+)

diff --git a/src/machdepArchConfigure.ml b/src/machdepArchConfigure.ml
index 95ed6a22e..29a249cd0 100644
--- a/src/machdepArchConfigure.ml
+++ b/src/machdepArchConfigure.ml
@@ -13,6 +13,7 @@ let () =
       let {C.Process.exit_code; stdout; stderr} = C.Process.run c !real_gcc ["-D_GNUCC"; "-m" ^ !m; "machdep-ml.c"; "-o"; exe] in
       if exit_code = 0 then (
         let {C.Process.stdout; stderr; exit_code} = C.Process.run c exe [] in
+        assert (exit_code = 0);
         Printf.printf "Some {%s}" stdout
       )
       else 
diff --git a/src/modelConfigure.ml b/src/modelConfigure.ml
index 5b0e8a4ac..a161e703a 100644
--- a/src/modelConfigure.ml
+++ b/src/modelConfigure.ml
@@ -13,6 +13,7 @@ let () =
       let {C.Process.exit_code; stdout; stderr} = C.Process.run c !real_gcc ["-D_GNUCC"; "-m" ^ !m; "machdep-ml.c"; "-o"; exe] in
       if exit_code = 0 then (
         let {C.Process.stdout; stderr; exit_code} = C.Process.run c exe ["--env"] in
+        assert (exit_code = 0);
         print_string stdout;
       )
       else 

From 460d4d3444a602f5597d5b71c9e68ba1a9b86637 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Mon, 25 Nov 2024 10:17:16 +0200
Subject: [PATCH 24/24] Allow manual CI execution

---
 .github/workflows/tests.yml | 1 +
 1 file changed, 1 insertion(+)

diff --git a/.github/workflows/tests.yml b/.github/workflows/tests.yml
index e8284c4df..6c9b42d3b 100644
--- a/.github/workflows/tests.yml
+++ b/.github/workflows/tests.yml
@@ -4,6 +4,7 @@ name: build and run tests
 on:
   - push
   - pull_request
+  - workflow_dispatch
 
 jobs:
   tests: