From 5aa2c2d99dc91502fad285ea5519805c26c04bff Mon Sep 17 00:00:00 2001 From: Chris Smowton Date: Thu, 19 Apr 2018 17:07:15 +0100 Subject: [PATCH] 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. --- src/java_bytecode/java_entry_point.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/java_bytecode/java_entry_point.cpp b/src/java_bytecode/java_entry_point.cpp index 5c3beafc357..1597868caf2 100644 --- a/src/java_bytecode/java_entry_point.cpp +++ b/src/java_bytecode/java_entry_point.cpp @@ -203,7 +203,7 @@ exprt::operandst java_build_arguments( !assume_init_pointers_not_null && !is_main && !is_this; object_factory_parameterst parameters = object_factory_parameters; - parameters.function_id = function.name; + parameters.function_id = goto_functionst::entry_point(); // generate code to allocate and non-deterministicaly initialize the // argument