Ignore x86 __seg_fs/__seg_gs named-address-space qualifiers

regression/cbmc/gcc_named_address_space/main.c

@@ -0,0 +1,23 @@
+// The x86 named-address-space (segment) qualifiers __seg_fs / __seg_gs,
+// used by the Linux kernel's per-CPU accessors as BARE type qualifiers
+// when the compiler supports named address spaces
+// (CONFIG_CC_HAS_NAMED_ADDRESS_SPACES) -- e.g. `typeof(x) __seg_gs *`.
+// They denote %fs/%gs segment-relative addressing, irrelevant to
+// functional verification, so CBMC ignores the qualifier (the pointed-to
+// object is unchanged).
+struct s
+{
+  int x;
+};
+
+int main(void)
+{
+  struct s obj = {.x = 42};
+  struct s __seg_gs *p = (struct s __seg_gs *)&obj;
+  struct s __seg_fs *q = (struct s __seg_fs *)&obj;
+  __typeof__(struct s __seg_gs) *r = &obj;
+  __CPROVER_assert(p->x == 42, "seg-gs-qualified pointer reads the object");
+  __CPROVER_assert(q->x == 42, "seg-fs-qualified pointer reads the object");
+  __CPROVER_assert(r->x == 42, "typeof with seg qualifier");
+  return 0;
+}

regression/cbmc/gcc_named_address_space/test.desc

@@ -0,0 +1,7 @@
+CORE
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--

src/ansi-c/scanner.l

@@ -1023,6 +1023,17 @@ enable_or_disable ("enable"|"disable")
 
 "__extension__" { /* ignore */ }
 
+  /* x86 named-address-space (segment) qualifiers used by the kernel's
+     per-CPU accessors (arch/x86/include/asm/percpu.h) when the compiler
+     supports named address spaces (CONFIG_CC_HAS_NAMED_ADDRESS_SPACES).
+     They denote %fs/%gs segment-relative addressing, which is irrelevant
+     to functional verification, so we ignore the qualifier (the pointed-to
+     object is unchanged).  When the compiler lacks the feature these are
+     instead macros expanding to __attribute__((address_space(...))), which
+     the GCC_ATTRIBUTE states already discard. */
+"__seg_fs"      { /* ignore: segment address-space qualifier */ }
+"__seg_gs"      { /* ignore: segment address-space qualifier */ }
+
 "__restrict"    { loc(); return TOK_RESTRICT; }
 "__restrict__"  { loc(); return TOK_RESTRICT; }