Merge pull request #6816 from tautschnig/bugfixes/crangler-static

Crangler: also apply remove-static to declarations

Author: kroening

regression/crangler/remove-static/remove_static1.c

@@ -5,6 +5,8 @@ int foo()
 
 int bar();
 
+static void foobar2();
+
 static void foobar1()
 {
 }

regression/crangler/remove-static/remove_static1.desc

@@ -6,3 +6,4 @@ remove_static1.json
 ^EXIT=0$
 ^SIGNAL=0$
 --
+static\s+(void\s+)?foobar[12]\(\)$

src/crangler/c_wrangler.cpp

@@ -368,7 +368,7 @@ static void mangle_function(
   const c_wranglert::functiont &function_config,
   std::ostream &out)
 {
-  if(function_config.stub.has_value())
+  if(function_config.stub.has_value() && declaration.has_body())
   {
     // replace by stub
     out << function_config.stub.value();
@@ -399,6 +399,13 @@ static void mangle_function(
     for(auto &t : declaration.post_declarator)
       out << t.text;
 
+    if(!declaration.has_body())
+    {
+      for(auto &t : declaration.initializer)
+        out << t.text;
+      return;
+    }
+
     for(const auto &entry : function_config.contract)
       out << ' ' << CPROVER_PREFIX << entry.clause << '('
           << defines(entry.content) << ')';
@@ -498,8 +505,7 @@ static void mangle(
   std::ostream &out)
 {
   auto name_opt = declaration.declared_identifier();
-  if(
-    declaration.is_function() && name_opt.has_value() && declaration.has_body())
+  if(declaration.is_function() && name_opt.has_value())
   {
     for(const auto &entry : config.functions)
     {