From 10615a72467247a82fa68bdec60e7ece0377fe22 Mon Sep 17 00:00:00 2001
From: Basile Desloges <basile.desloges@cea.fr>
Date: Tue, 28 Jan 2025 16:00:01 +0100
Subject: [PATCH] [kernel] Add test for __builtin_types_compatible_p

---
 tests/syntax/builtin_types_compatible.i                |  6 ++++++
 .../syntax/oracle/builtin_types_compatible.res.oracle  | 10 ++++++++++
 2 files changed, 16 insertions(+)
 create mode 100644 tests/syntax/builtin_types_compatible.i
 create mode 100644 tests/syntax/oracle/builtin_types_compatible.res.oracle

diff --git a/tests/syntax/builtin_types_compatible.i b/tests/syntax/builtin_types_compatible.i
new file mode 100644
index 0000000000..891cb5e7e4
--- /dev/null
+++ b/tests/syntax/builtin_types_compatible.i
@@ -0,0 +1,6 @@
+/* run.config
+   OPT: -machdep gcc_x86_64 -print
+*/
+int main() {
+  return __builtin_types_compatible_p(int, int[]);
+}
diff --git a/tests/syntax/oracle/builtin_types_compatible.res.oracle b/tests/syntax/oracle/builtin_types_compatible.res.oracle
new file mode 100644
index 0000000000..139913b6d0
--- /dev/null
+++ b/tests/syntax/oracle/builtin_types_compatible.res.oracle
@@ -0,0 +1,10 @@
+[kernel] Parsing builtin_types_compatible.i (no preprocessing)
+/* Generated by Frama-C */
+int main(void)
+{
+  int __retres;
+  __retres = 0;
+  return __retres;
+}
+
+
-- 
GitLab