ansi-c library: model __builtin_assume_aligned

regression/cbmc-library/__builtin_assume_aligned/main.c

@@ -0,0 +1,12 @@
+#include <assert.h>
+
+int main()
+{
+  int x = 5;
+  // Per the GCC documentation __builtin_assume_aligned returns its
+  // first argument (and asserts nothing at run time).
+  void *p = __builtin_assume_aligned(&x, 4);
+  assert(p == &x);
+  assert(*(int *)p == 5);
+  return 0;
+}

regression/cbmc-library/__builtin_assume_aligned/test.desc

@@ -0,0 +1,8 @@
+CORE gcc-only
+main.c
+--pointer-check --bounds-check
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

src/ansi-c/library/gcc.c

@@ -1,3 +1,18 @@
+/* FUNCTION: __builtin_assume_aligned */
+
+void *__builtin_assume_aligned(const void *exp, __CPROVER_size_t align, ...)
+{
+  // Per the GCC documentation, this returns `exp` and allows the
+  // compiler to assume the returned pointer is at least `align`-byte
+  // aligned (with an optional run-time misalignment offset in the
+  // variadic part).  The alignment claim is an optimisation hint; for
+  // verification we model the identity value flow and do not prune
+  // (assume) or check (assert) the alignment, which keeps the model
+  // conservative.
+  (void)align;
+  return (void *)exp;
+}
+
 /* FUNCTION: __builtin_ia32_sfence */
 
 #if defined(__i386__) || defined(__x86_64__)