From f0502d24e759833160b7604f29b263dd83f1cd8b Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Wed, 6 Apr 2022 14:40:11 +0000 Subject: [PATCH] Set base_name member for __CPROVER_start The (un)reachable functions output uses the base_name in the output, which previously resulted in the surprising behaviour that an empty function name was printed. While falling back to the symbol's name may be possible, there could well be other places that try to use the `base_name`. --- jbmc/src/java_bytecode/java_entry_point.cpp | 1 + .../goto-analyzer/reachable-functions-basic-json/test.desc | 1 + .../goto-analyzer/reachable-functions-basic-text/test.desc | 1 + src/ansi-c/ansi_c_entry_point.cpp | 1 + src/jsil/jsil_entry_point.cpp | 1 + src/statement-list/statement_list_entry_point.cpp | 1 + unit/analyses/ai/ai.cpp | 1 + 7 files changed, 7 insertions(+) diff --git a/jbmc/src/java_bytecode/java_entry_point.cpp b/jbmc/src/java_bytecode/java_entry_point.cpp index 58c5d1160bd..05e37b1c535 100644 --- a/jbmc/src/java_bytecode/java_entry_point.cpp +++ b/jbmc/src/java_bytecode/java_entry_point.cpp @@ -767,6 +767,7 @@ bool generate_java_start_function( symbolt new_symbol; new_symbol.name=goto_functionst::entry_point(); + new_symbol.base_name = goto_functionst::entry_point(); new_symbol.type = java_method_typet({}, java_void_type()); new_symbol.value.swap(init_code); new_symbol.mode=ID_java; diff --git a/regression/goto-analyzer/reachable-functions-basic-json/test.desc b/regression/goto-analyzer/reachable-functions-basic-json/test.desc index 78060f012c4..2ed573690ac 100644 --- a/regression/goto-analyzer/reachable-functions-basic-json/test.desc +++ b/regression/goto-analyzer/reachable-functions-basic-json/test.desc @@ -10,3 +10,4 @@ CORE -- "last line":[[:space:]]*$ ^warning: ignoring +"function": "" diff --git a/regression/goto-analyzer/reachable-functions-basic-text/test.desc b/regression/goto-analyzer/reachable-functions-basic-text/test.desc index 2ef6e1898c8..f97803107a8 100644 --- a/regression/goto-analyzer/reachable-functions-basic-text/test.desc +++ b/regression/goto-analyzer/reachable-functions-basic-text/test.desc @@ -9,3 +9,4 @@ unreachable.c not_obviously_dead 25 31$ ^SIGNAL=0$ -- ^warning: ignoring +^ 35$ diff --git a/src/ansi-c/ansi_c_entry_point.cpp b/src/ansi-c/ansi_c_entry_point.cpp index 6c10396e08e..1988a20dfd1 100644 --- a/src/ansi-c/ansi_c_entry_point.cpp +++ b/src/ansi-c/ansi_c_entry_point.cpp @@ -535,6 +535,7 @@ bool generate_ansi_c_start_function( symbolt new_symbol; new_symbol.name=goto_functionst::entry_point(); + new_symbol.base_name = goto_functionst::entry_point(); new_symbol.type = code_typet({}, void_type()); new_symbol.value.swap(init_code); new_symbol.mode=symbol.mode; diff --git a/src/jsil/jsil_entry_point.cpp b/src/jsil/jsil_entry_point.cpp index 422805948c3..57456145877 100644 --- a/src/jsil/jsil_entry_point.cpp +++ b/src/jsil/jsil_entry_point.cpp @@ -152,6 +152,7 @@ bool jsil_entry_point( symbolt new_symbol; new_symbol.name=goto_functionst::entry_point(); + new_symbol.base_name = goto_functionst::entry_point(); new_symbol.type = code_typet({}, empty_typet()); new_symbol.value.swap(init_code); diff --git a/src/statement-list/statement_list_entry_point.cpp b/src/statement-list/statement_list_entry_point.cpp index 47e95bf3210..66da25f41ab 100644 --- a/src/statement-list/statement_list_entry_point.cpp +++ b/src/statement-list/statement_list_entry_point.cpp @@ -180,6 +180,7 @@ bool generate_statement_list_start_function( // Add the start symbol. symbolt start_symbol; start_symbol.name = goto_functionst::entry_point(); + start_symbol.base_name = goto_functionst::entry_point(); start_symbol.type = code_typet({}, empty_typet{}); start_symbol.value.swap(start_function_body); start_symbol.mode = main.mode; diff --git a/unit/analyses/ai/ai.cpp b/unit/analyses/ai/ai.cpp index 905ee2aa206..bdec4ae5cfb 100644 --- a/unit/analyses/ai/ai.cpp +++ b/unit/analyses/ai/ai.cpp @@ -233,6 +233,7 @@ SCENARIO( symbolt start; start.name = goto_functionst::entry_point(); + start.base_name = goto_functionst::entry_point(); start.mode = ID_C; start.type = code_typet({}, empty_typet()); start.value = make_void_call(f.symbol_expr());