Skip to content

Bugfix/static function #739

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 4 commits into from
Apr 19, 2017
Merged

Bugfix/static function #739

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
18b33b8
Don't allowing functions called from _Start to be inlined
Nov 29, 2016
96e2a84
Fixed the issue with a single static function in a translation unit s…
NlightNFotis Mar 30, 2017
6509e10
Added two new tests that demonstrate that goto-cc correctly reports a…
NlightNFotis Mar 30, 2017
62995f5
Added a new test that would fail with the wrong logic in the remove_i…
NlightNFotis Mar 31, 2017
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
4 changes: 4 additions & 0 deletions regression/ansi-c/static1/main.c
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,4 @@
static int fun(int a)
{
return a+1;
}
3 changes: 1 addition & 2 deletions regression/ansi-c/static_inline2/test.desc → regression/ansi-c/static1/test.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,8 +1,7 @@
KNOWNBUG
CORE
main.c
--function fun
^EXIT=0$
^SIGNAL=0$
^VERIFICATION SUCCESSFUL$
--
^warning: ignoring
4 changes: 4 additions & 0 deletions regression/ansi-c/static2/main.c
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,4 @@
int foo(int a)
{
return a+1;
}
4 changes: 4 additions & 0 deletions regression/ansi-c/static2/main2.c
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,4 @@
static int foo(int a)
{
return a+1;
}
6 changes: 6 additions & 0 deletions regression/ansi-c/static2/test.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,6 @@
CORE
main.c
main2.c --function foo
^main symbol `foo' is ambiguous$
--
^warning: ignoring
4 changes: 4 additions & 0 deletions regression/ansi-c/static3/main.c
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,4 @@
static int foo(int a)
{
return a+1;
}
4 changes: 4 additions & 0 deletions regression/ansi-c/static3/main2.c
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,4 @@
static int foo(int a)
{
return a+1;
}
6 changes: 6 additions & 0 deletions regression/ansi-c/static3/test.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,6 @@
CORE
main.c
main2.c --function foo
^main symbol `foo' is ambiguous$
--
^warning: ignoring
3 changes: 1 addition & 2 deletions regression/ansi-c/static_inline1/test.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,8 +1,7 @@
KNOWNBUG
CORE
main.c

^EXIT=0$
^SIGNAL=0$
^VERIFICATION SUCCESSFUL$
--
^warning: ignoring
4 changes: 0 additions & 4 deletions regression/ansi-c/static_inline2/main.c
View file
Open in desktop

This file was deleted.

4 changes: 4 additions & 0 deletions regression/cbmc/Static4/main.c
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,4 @@
static int foo(int a)
{
return a+1;
}
7 changes: 7 additions & 0 deletions regression/cbmc/Static4/test.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,7 @@
CORE
main.c
--show-symbol-table
^EXIT=0$
^SIGNAL=0$
--
^Symbol......: foo
7 changes: 6 additions & 1 deletion src/goto-programs/goto_inline.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -213,7 +213,12 @@ void goto_partial_inline(
// called function
const goto_functiont &goto_function=f_it->second;

if(!goto_function.body_available())
// We can't take functions without bodies to find functions
// inside them to be inlined.
// We also don't allow for the _start function to have any of its
// function calls to be inlined
if(!goto_function.body_available() ||
f_it->first==goto_functions.entry_point())
continue;

const goto_programt &goto_program=goto_function.body;
Expand Down
4 changes: 3 additions & 1 deletion src/linking/remove_internal_symbols.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -11,6 +11,7 @@ Author: Daniel Kroening
#include <util/find_symbols.h>
#include <util/std_types.h>
#include <util/cprover_prefix.h>
#include <util/config.h>

#include "remove_internal_symbols.h"

Expand Down Expand Up @@ -149,7 +150,8 @@ void remove_internal_symbols(
else if(is_function)
{
// body? not local (i.e., "static")?
if(has_body && !is_file_local)
if(has_body &&
(!is_file_local || (config.main==symbol.name.c_str())))
get_symbols_rec(ns, symbol, exported);
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

What's the .c_str() doing?

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

@kroening It's returning a const char * that we can compare to the std::string that is config.main. Without it, we get the following error message:

remove_internal_symbols.cpp: In function 'void remove_internal_symbols(symbol_tablet&)':
remove_internal_symbols.cpp:153:54: error: no match for 'operator==' (operand types are 'std::__cxx11::string {aka std::__cxx11::basic_string<char>}' and 'const irep_idt {aka const dstringt}')
       if(has_body || (!is_file_local && (config.main == symbol.name)))

If we need to change it, I can change the c_str() call to as_string(), but they appear to do exactly the same thing, with the difference that c_str() returns a C string whereas as_string() returns a c++ string.

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

@kroening @NlightNFotis I'm wondering why config.main is a string. I can't see a good reason for it not to be an irep_idt.

}
else
Expand Down