Merge pull request #2553 from tautschnig/always-inline-partial-revert

Daniel Kroening · web-flow · commit c6f92318e9ca · 2018-07-08T08:12:36.000+01:00
Partial revert of #1898 (always_inline support, second attempt)
diff --git a/regression/ansi-c/always_inline1/test.desc b/regression/ansi-c/always_inline1/test.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 
 ^EXIT=0$
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
diff --git a/src/ansi-c/ansi_c_convert_type.cpp b/src/ansi-c/ansi_c_convert_type.cpp
@@ -171,8 +171,6 @@ void ansi_c_convert_typet::read_rec(const typet &type)
     c_storage_spec.is_weak=true;
   else if(type.id() == ID_used)
     c_storage_spec.is_used = true;
-  else if(type.id() == ID_always_inline)
-    c_storage_spec.is_always_inline = true;
   else if(type.id()==ID_auto)
   {
     // ignore
diff --git a/src/ansi-c/ansi_c_declaration.cpp b/src/ansi-c/ansi_c_declaration.cpp
@@ -81,8 +81,6 @@ void ansi_c_declarationt::output(std::ostream &out) const
     out << " is_extern";
   if(get_is_static_assert())
     out << " is_static_assert";
-  if(get_is_always_inline())
-    out << " is_always_inline";
   out << "\n";
 
   out << "Type: " << type().pretty() << "\n";
@@ -166,9 +164,6 @@ void ansi_c_declarationt::to_symbol(
           symbol.is_extern=false;
         else  if(get_is_extern()) // traditional GCC
           symbol.is_file_local=true;
-
-        if(get_is_always_inline())
-          symbol.is_macro = true;
       }
 
       // GCC __attribute__((__used__)) - do not treat those as file-local
diff --git a/src/ansi-c/ansi_c_declaration.h b/src/ansi-c/ansi_c_declaration.h
@@ -205,16 +205,6 @@ class ansi_c_declarationt:public exprt
     set(ID_is_used, is_used);
   }
 
-  bool get_is_always_inline() const
-  {
-    return get_bool(ID_is_always_inline);
-  }
-
-  void set_is_always_inline(bool is_always_inline)
-  {
-    set(ID_is_always_inline, is_always_inline);
-  }
-
   void to_symbol(
     const ansi_c_declaratort &,
     symbolt &symbol) const;
diff --git a/src/ansi-c/c_storage_spec.cpp b/src/ansi-c/c_storage_spec.cpp
@@ -34,8 +34,6 @@ void c_storage_spect::read(const typet &type)
     is_weak=true;
   else if(type.id() == ID_used)
     is_used = true;
-  else if(type.id() == ID_always_inline)
-    is_always_inline = true;
   else if(type.id()==ID_auto)
   {
     // ignore
diff --git a/src/ansi-c/c_storage_spec.h b/src/ansi-c/c_storage_spec.h
@@ -36,14 +36,13 @@ class c_storage_spect
     is_inline=false;
     is_weak=false;
     is_used = false;
-    is_always_inline = false;
     alias.clear();
     asm_label.clear();
     section.clear();
   }
 
-  bool is_typedef, is_extern, is_static, is_register, is_inline,
-    is_thread_local, is_weak, is_used, is_always_inline;
+  bool is_typedef, is_extern, is_static, is_register,
+       is_inline, is_thread_local, is_weak, is_used;
 
   // __attribute__((alias("foo")))
   irep_idt alias;
@@ -54,7 +53,6 @@ class c_storage_spect
 
   bool operator==(const c_storage_spect &other) const
   {
-    // clang-format off
     return is_typedef==other.is_typedef &&
            is_extern==other.is_extern &&
            is_static==other.is_static &&
@@ -63,11 +61,9 @@ class c_storage_spect
            is_inline==other.is_inline &&
            is_weak==other.is_weak &&
            is_used == other.is_used &&
-           is_always_inline == other.is_always_inline &&
            alias==other.alias &&
            asm_label==other.asm_label &&
            section==other.section;
-    // clang-format on
   }
 
   bool operator!=(const c_storage_spect &other) const
@@ -85,7 +81,6 @@ class c_storage_spect
     is_thread_local |=other.is_thread_local;
     is_weak         |=other.is_weak;
     is_used         |=other.is_used;
-    is_always_inline |= other.is_always_inline;
     if(alias.empty())
       alias=other.alias;
     if(asm_label.empty())
diff --git a/src/ansi-c/c_typecheck_base.cpp b/src/ansi-c/c_typecheck_base.cpp
diff --git a/src/ansi-c/c_typecheck_expr.cpp b/src/ansi-c/c_typecheck_expr.cpp
diff --git a/src/ansi-c/parser.y b/src/ansi-c/parser.y
diff --git a/src/ansi-c/scanner.l b/src/ansi-c/scanner.l
diff --git a/src/util/irep_ids.def b/src/util/irep_ids.def
diff --git a/src/util/replace_symbol.cpp b/src/util/replace_symbol.cpp

Original file line number	Diff line number	Diff line change
`@@ -1,4 +1,4 @@`
`1`		`-CORE`
	`1`	`+KNOWNBUG`
`2`	`2`	`main.c`
`3`	`3`
`4`	`4`	`^EXIT=0$`