Additional regression tests for always_inline

tautschnig · tautschnig · commit e501317b53d8 · 2018-07-07T10:02:57.000Z
The previous attempt of implementing support for always_inline broke each of
those in different ways.
diff --git a/regression/ansi-c/always_inline2/main.c b/regression/ansi-c/always_inline2/main.c
@@ -0,0 +1,16 @@
+static inline __attribute__((__always_inline__)) int func(int val)
+{
+  return val;
+}
+
+static inline int func2(int *p)
+{
+  // the typecast, although redundant, is essential to show the problem
+  return func(*(int*)p);
+}
+
+int main()
+{
+  int x;
+  return func2(&x);
+}
diff --git a/regression/ansi-c/always_inline2/test.desc b/regression/ansi-c/always_inline2/test.desc
@@ -0,0 +1,8 @@
+CORE gcc-only
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+^CONVERSION ERROR$
diff --git a/regression/ansi-c/always_inline3/main.c b/regression/ansi-c/always_inline3/main.c
@@ -0,0 +1,12 @@
+static inline __attribute__((__always_inline__)) int func(int val)
+{
+  if(val > 0)
+    return func(val - 1);
+  return 0;
+}
+
+int main()
+{
+  int x;
+  return func(x);
+}
diff --git a/regression/ansi-c/always_inline3/test.desc b/regression/ansi-c/always_inline3/test.desc
@@ -0,0 +1,8 @@
+CORE gcc-only
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+^CONVERSION ERROR$
diff --git a/regression/ansi-c/always_inline4/main.c b/regression/ansi-c/always_inline4/main.c
@@ -0,0 +1,14 @@
+extern int func_alias(int val) __asm__("" "func");
+
+static inline __attribute__((__always_inline__)) int func(int val)
+{
+  if(val > 0)
+    return func_alias(val - 1);
+  return 0;
+}
+
+int main()
+{
+  int x;
+  return func(x);
+}
diff --git a/regression/ansi-c/always_inline4/test.desc b/regression/ansi-c/always_inline4/test.desc
@@ -0,0 +1,8 @@
+CORE gcc-only
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+^CONVERSION ERROR$
diff --git a/regression/ansi-c/always_inline5/main.c b/regression/ansi-c/always_inline5/main.c
@@ -0,0 +1,12 @@
+static inline
+__attribute__((__section__(".init"))) __attribute__((__always_inline__))
+int func(int val)
+{
+  return val + 1;
+}
+
+int main()
+{
+  int x;
+  return func(x);
+}
diff --git a/regression/ansi-c/always_inline5/test.desc b/regression/ansi-c/always_inline5/test.desc
@@ -0,0 +1,8 @@
+CORE gcc-only
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+^CONVERSION ERROR$
diff --git a/regression/ansi-c/always_inline6/main.c b/regression/ansi-c/always_inline6/main.c
@@ -0,0 +1,10 @@
+static inline __attribute__((__always_inline__)) int func(int val, ...)
+{
+  return val + 1;
+}
+
+int main()
+{
+  int x;
+  return func(x, x);
+}
diff --git a/regression/ansi-c/always_inline6/test.desc b/regression/ansi-c/always_inline6/test.desc
@@ -0,0 +1,8 @@
+CORE gcc-only
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+^CONVERSION ERROR$
diff --git a/regression/ansi-c/always_inline7/main.c b/regression/ansi-c/always_inline7/main.c
@@ -0,0 +1,11 @@
+static inline __attribute__((__always_inline__)) int func(int val)
+{
+  int local = val;
+  return local;
+}
+
+int main()
+{
+  int x;
+  return func(x);
+}
diff --git a/regression/ansi-c/always_inline7/test.desc b/regression/ansi-c/always_inline7/test.desc
@@ -0,0 +1,8 @@
+CORE gcc-only
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+^CONVERSION ERROR$
diff --git a/regression/ansi-c/always_inline8/main.c b/regression/ansi-c/always_inline8/main.c
@@ -0,0 +1,10 @@
+static inline __attribute__((__always_inline__)) int func(int val)
+{
+  return (__typeof__(val))42;
+}
+
+int main()
+{
+  int x;
+  return func(x);
+}
diff --git a/regression/ansi-c/always_inline8/test.desc b/regression/ansi-c/always_inline8/test.desc
@@ -0,0 +1,8 @@
+CORE gcc-only
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+^CONVERSION ERROR$
diff --git a/regression/ansi-c/always_inline9/main.c b/regression/ansi-c/always_inline9/main.c
@@ -0,0 +1,11 @@
+static inline __attribute__((__always_inline__)) int func(int val)
+{
+  val = val + 1;
+  return val;
+}
+
+int main()
+{
+  int x;
+  return func(x);
+}
diff --git a/regression/ansi-c/always_inline9/test.desc b/regression/ansi-c/always_inline9/test.desc
@@ -0,0 +1,8 @@
+CORE gcc-only
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+^CONVERSION ERROR$
diff --git a/regression/cbmc/always_inline1/main.c b/regression/cbmc/always_inline1/main.c
@@ -0,0 +1,24 @@
+#include <assert.h>
+
+#ifndef __GNUC__
+#define __attribute__(x)
+#endif
+
+static inline __attribute__((__always_inline__)) void func(int *val)
+{
+  *val = 1;
+  return;
+}
+
+static inline int func2(int *p)
+{
+  func(p);
+  return *p;
+}
+
+int main()
+{
+  int x;
+  assert(func2(&x) == 1);
+  return 0;
+}
diff --git a/regression/cbmc/always_inline1/test.desc b/regression/cbmc/always_inline1/test.desc
@@ -0,0 +1,8 @@
+CORE
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
diff --git a/regression/cbmc/always_inline2/main.c b/regression/cbmc/always_inline2/main.c
@@ -0,0 +1,30 @@
+#include <assert.h>
+
+#ifndef __GNUC__
+#define __attribute__(x)
+#endif
+
+static inline __attribute__((__always_inline__)) int func(int *val)
+{
+  switch(*val)
+  {
+    case 1:
+      return *val + 1;
+    case 2:
+      return *val + 2;
+  }
+
+  return *val;
+}
+
+static inline int func2(int *p)
+{
+  return func(p);
+}
+
+int main()
+{
+  int x = 1;
+  assert(func2(&x) == 2);
+  return 0;
+}
diff --git a/regression/cbmc/always_inline2/test.desc b/regression/cbmc/always_inline2/test.desc
@@ -0,0 +1,8 @@
+CORE
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
diff --git a/regression/cbmc/always_inline3/main.c b/regression/cbmc/always_inline3/main.c
@@ -0,0 +1,32 @@
+#include <assert.h>
+
+#ifndef __GNUC__
+#define __attribute__(x)
+#endif
+
+static inline __attribute__((__always_inline__)) void func(int *val)
+{
+  if(*val < 0)
+  {
+    *val = 1;
+    return;
+  }
+  else
+  {
+    *val = 1;
+    return;
+  }
+}
+
+static inline int func2(int *p)
+{
+  func(p);
+  return *p;
+}
+
+int main()
+{
+  int x;
+  assert(func2(&x) == 1);
+  return 0;
+}
diff --git a/regression/cbmc/always_inline3/test.desc b/regression/cbmc/always_inline3/test.desc
@@ -0,0 +1,8 @@
+CORE
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
