Skip to content

Commit f0502d2

Browse files
committed
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`.
1 parent 1a4c66e commit f0502d2

File tree

7 files changed

+7
-0
lines changed

7 files changed

+7
-0
lines changed

jbmc/src/java_bytecode/java_entry_point.cpp

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -767,6 +767,7 @@ bool generate_java_start_function(
767767
symbolt new_symbol;
768768

769769
new_symbol.name=goto_functionst::entry_point();
770+
new_symbol.base_name = goto_functionst::entry_point();
770771
new_symbol.type = java_method_typet({}, java_void_type());
771772
new_symbol.value.swap(init_code);
772773
new_symbol.mode=ID_java;

regression/goto-analyzer/reachable-functions-basic-json/test.desc

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -10,3 +10,4 @@ CORE
1010
--
1111
"last line":[[:space:]]*$
1212
^warning: ignoring
13+
"function": ""

regression/goto-analyzer/reachable-functions-basic-text/test.desc

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -9,3 +9,4 @@ unreachable.c not_obviously_dead 25 31$
99
^SIGNAL=0$
1010
--
1111
^warning: ignoring
12+
^ 35$

src/ansi-c/ansi_c_entry_point.cpp

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -535,6 +535,7 @@ bool generate_ansi_c_start_function(
535535
symbolt new_symbol;
536536

537537
new_symbol.name=goto_functionst::entry_point();
538+
new_symbol.base_name = goto_functionst::entry_point();
538539
new_symbol.type = code_typet({}, void_type());
539540
new_symbol.value.swap(init_code);
540541
new_symbol.mode=symbol.mode;

src/jsil/jsil_entry_point.cpp

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -152,6 +152,7 @@ bool jsil_entry_point(
152152
symbolt new_symbol;
153153

154154
new_symbol.name=goto_functionst::entry_point();
155+
new_symbol.base_name = goto_functionst::entry_point();
155156
new_symbol.type = code_typet({}, empty_typet());
156157
new_symbol.value.swap(init_code);
157158

src/statement-list/statement_list_entry_point.cpp

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -180,6 +180,7 @@ bool generate_statement_list_start_function(
180180
// Add the start symbol.
181181
symbolt start_symbol;
182182
start_symbol.name = goto_functionst::entry_point();
183+
start_symbol.base_name = goto_functionst::entry_point();
183184
start_symbol.type = code_typet({}, empty_typet{});
184185
start_symbol.value.swap(start_function_body);
185186
start_symbol.mode = main.mode;

unit/analyses/ai/ai.cpp

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -233,6 +233,7 @@ SCENARIO(
233233

234234
symbolt start;
235235
start.name = goto_functionst::entry_point();
236+
start.base_name = goto_functionst::entry_point();
236237
start.mode = ID_C;
237238
start.type = code_typet({}, empty_typet());
238239
start.value = make_void_call(f.symbol_expr());

0 commit comments

Comments
 (0)