Skip to content

Commit 5aa2c2d

Browse files
committed
Attribute main function arguments to __CPROVER_start
These are created to serve as arguments to main() (or whatever --function was passed), but are declared in __CPROVER_start, and so should be named after their declarer like all other locals. This was causing a problem in the security repository, where we relied on local variable names being prefixed by their declaring function name, and the easiest fix was to restore that convention.
1 parent b7ef5af commit 5aa2c2d

File tree

1 file changed

+1
-1
lines changed

1 file changed

+1
-1
lines changed

src/java_bytecode/java_entry_point.cpp

+1-1
Original file line numberDiff line numberDiff line change
@@ -203,7 +203,7 @@ exprt::operandst java_build_arguments(
203203
!assume_init_pointers_not_null && !is_main && !is_this;
204204

205205
object_factory_parameterst parameters = object_factory_parameters;
206-
parameters.function_id = function.name;
206+
parameters.function_id = goto_functionst::entry_point();
207207

208208
// generate code to allocate and non-deterministicaly initialize the
209209
// argument

0 commit comments

Comments
 (0)