From 4d344db8f2f2ef5c1e5939460267423ff56a17cd Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Sat, 29 Nov 2025 12:13:16 +0100
Subject: [PATCH] C front-end: support GCC attributes before contract clauses

Add a rule to also permit GCC attributes (C23 attributes already worked)
before contract clauses attached to functions. This is at the expense of
creating additional shift/reduce conflicts in our parser.

Fixes: #8685
---
 .../gcc_attribute_before_contract/main.c      | 47 +++++++++++++++++++
 .../gcc_attribute_before_contract/test.desc   |  7 +++
 src/ansi-c/parser.y                           | 19 +++++++-
 3 files changed, 72 insertions(+), 1 deletion(-)
 create mode 100644 regression/ansi-c/gcc_attribute_before_contract/main.c
 create mode 100644 regression/ansi-c/gcc_attribute_before_contract/test.desc

diff --git a/regression/ansi-c/gcc_attribute_before_contract/main.c b/regression/ansi-c/gcc_attribute_before_contract/main.c
new file mode 100644
index 00000000000..b242c78bf01
--- /dev/null
+++ b/regression/ansi-c/gcc_attribute_before_contract/main.c
@@ -0,0 +1,47 @@
+// Test for issue #8685: GCC attributes before contract clauses
+// This test verifies that GCC __attribute__ syntax can appear before
+// __CPROVER_* contract clauses, just like C23 [[...]] attributes.
+
+#include <limits.h>
+
+// Test 1: GCC attribute before __CPROVER_requires (declaration)
+int test_decl1(int a) __attribute__((const)) __CPROVER_requires(a != 0);
+
+// Test 2: GCC attribute before __CPROVER_ensures (declaration)
+int test_decl2(int a) __attribute__((pure))
+__CPROVER_ensures(__CPROVER_return_value > 0);
+
+// Test 3: Multiple GCC attributes before __CPROVER_requires
+int test_decl3(int a) __attribute__((const)) __attribute__((nonnull))
+__CPROVER_requires(a != 0);
+
+// Test 4: GCC attribute before multiple contract clauses
+int test_decl4(int a) __attribute__((const)) __CPROVER_requires(a > 0)
+  __CPROVER_ensures(__CPROVER_return_value == a + 1);
+
+// Test 5: Function with no parameters, GCC attribute before contract
+int test_decl5(void) __attribute__((const))
+__CPROVER_ensures(__CPROVER_return_value == 42);
+
+// Test 6: C23 attribute style (should still work as before)
+int test_decl6(int a) [[gnu::const]] __CPROVER_requires(a != 0);
+
+// Test 7: Function definition with GCC attribute and contract
+int test_def1(int a) __attribute__((const)) __CPROVER_requires(a < INT_MAX)
+{
+  return a + 1;
+}
+
+// Test 8: No attribute (baseline - should still work)
+int test_decl7(int a) __CPROVER_requires(a != 0);
+
+// Test 9: Attribute without contract (should still work)
+int test_decl8(int a) __attribute__((const));
+
+int main(void)
+{
+  int x = 5;
+  int result = test_def1(x);
+  __CPROVER_assert(result == 6, "test_def1 should return 6");
+  return 0;
+}
diff --git a/regression/ansi-c/gcc_attribute_before_contract/test.desc b/regression/ansi-c/gcc_attribute_before_contract/test.desc
new file mode 100644
index 00000000000..932cbf87ce3
--- /dev/null
+++ b/regression/ansi-c/gcc_attribute_before_contract/test.desc
@@ -0,0 +1,7 @@
+CORE
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
diff --git a/src/ansi-c/parser.y b/src/ansi-c/parser.y
index 91526b2b8e6..52ea992eb96 100644
--- a/src/ansi-c/parser.y
+++ b/src/ansi-c/parser.y
@@ -286,7 +286,8 @@ int yyansi_cerror(const std::string &error);
 
 %start grammar
 
-%expect 2 /* the famous "dangling `else'" ambiguity */
+%expect 8 /* the famous "dangling `else'" ambiguity, and ambiguities from allowing
+              GCC attributes before contract clauses (resolved by preferring shift) */
           /* results in one shift/reduce conflict   */
           /* that we don't want to be reported      */
 
@@ -3515,6 +3516,22 @@ cprover_function_contract_sequence:
 cprover_function_contract_sequence_opt:
           /* nothing */
           { init($$); }
+        | post_declarator_attributes cprover_function_contract_sequence
+        {
+          // Function contracts should either be attached to a
+          // top-level function declaration or top-level function
+          // definition.  Any embedded function pointer scopes should
+          // be disallowed.
+          int contract_in_global_scope = (PARSER.scopes.size() == 1);
+          int contract_in_top_level_function_scope = (PARSER.scopes.size() == 2);
+          if(!contract_in_global_scope && !contract_in_top_level_function_scope)
+          {
+            yyansi_cerror("Function contracts allowed only at top-level declarations.");
+            YYABORT;
+          }
+          // Merge attributes with contracts
+          $$ = merge($1, $2);
+        }
         | cprover_function_contract_sequence
         {
           // Function contracts should either be attached to a