Skip to content

Commit c5f0f36

Browse files
committed
Crangler: also apply remove-static to declarations
Taking functions out of file-local scope requires removing the "static" keyword from both definitions as well as declarations.
1 parent abc4e01 commit c5f0f36

File tree

3 files changed

+12
-3
lines changed

3 files changed

+12
-3
lines changed

regression/crangler/remove-static/remove_static1.c

+2
Original file line numberDiff line numberDiff line change
@@ -5,6 +5,8 @@ int foo()
55

66
int bar();
77

8+
static void foobar2();
9+
810
static void foobar1()
911
{
1012
}

regression/crangler/remove-static/remove_static1.desc

+1
Original file line numberDiff line numberDiff line change
@@ -6,3 +6,4 @@ remove_static1.json
66
^EXIT=0$
77
^SIGNAL=0$
88
--
9+
static\s+(void\s+)?foobar[12]\(\)$

src/crangler/c_wrangler.cpp

+9-3
Original file line numberDiff line numberDiff line change
@@ -368,7 +368,7 @@ static void mangle_function(
368368
const c_wranglert::functiont &function_config,
369369
std::ostream &out)
370370
{
371-
if(function_config.stub.has_value())
371+
if(function_config.stub.has_value() && declaration.has_body())
372372
{
373373
// replace by stub
374374
out << function_config.stub.value();
@@ -399,6 +399,13 @@ static void mangle_function(
399399
for(auto &t : declaration.post_declarator)
400400
out << t.text;
401401

402+
if(!declaration.has_body())
403+
{
404+
for(auto &t : declaration.initializer)
405+
out << t.text;
406+
return;
407+
}
408+
402409
for(const auto &entry : function_config.contract)
403410
out << ' ' << CPROVER_PREFIX << entry.clause << '('
404411
<< defines(entry.content) << ')';
@@ -498,8 +505,7 @@ static void mangle(
498505
std::ostream &out)
499506
{
500507
auto name_opt = declaration.declared_identifier();
501-
if(
502-
declaration.is_function() && name_opt.has_value() && declaration.has_body())
508+
if(declaration.is_function() && name_opt.has_value())
503509
{
504510
for(const auto &entry : config.functions)
505511
{

0 commit comments

Comments
 (0)