Prefix temporary variable names with function id

regression/cbmc/Quantifiers-not-exists/test.desc

@@ -3,11 +3,11 @@ main.c
 
 ^\*\* Results:$
 ^\[main.assertion.1\] assertion a\[.*\]\[.*\] > 10: SUCCESS$
-^\[main.assertion.2\] assertion tmp_if_expr\$3: SUCCESS$
-^\[main.assertion.3\] assertion tmp_if_expr\$6: SUCCESS$
-^\[main.assertion.4\] assertion tmp_if_expr\$9: SUCCESS$
-^\[main.assertion.5\] assertion tmp_if_expr\$12: SUCCESS$
-^\[main.assertion.6\] assertion tmp_if_expr\$15: SUCCESS$
+^\[main.assertion.2\] assertion tmp_if_expr\$\d+: SUCCESS$
+^\[main.assertion.3\] assertion tmp_if_expr\$\d+: SUCCESS$
+^\[main.assertion.4\] assertion tmp_if_expr\$\d+: SUCCESS$
+^\[main.assertion.5\] assertion tmp_if_expr\$\d+: SUCCESS$
+^\[main.assertion.6\] assertion tmp_if_expr\$\d+: SUCCESS$
 ^\*\* 0 of 6 failed
 ^VERIFICATION SUCCESSFUL$
 ^EXIT=0$

regression/cbmc/Quantifiers-two-dimension-array/test.desc

@@ -6,7 +6,7 @@ main.c
 ^\[main.assertion.2\] assertion a\[.*\]\[.*\] == 1: SUCCESS$
 ^\[main.assertion.3\] assertion a\[.*\]\[.*\] == 1: SUCCESS$
 ^\[main.assertion.4\] assertion a\[.*\]\[.*\] == 2: SUCCESS$
-^\[main.assertion.5\] assertion tmp_if_expr\$3: SUCCESS$
+^\[main.assertion.5\] assertion tmp_if_expr\$\d+: SUCCESS$
 ^\*\* 0 of 5 failed
 ^VERIFICATION SUCCESSFUL$
 ^EXIT=0$

regression/cbmc/Quantifiers-type/test.desc

@@ -2,8 +2,8 @@ CORE
 main.c
 
 ^\*\* Results:$
-^\[main.assertion.1\] assertion tmp_if_expr\$1: FAILURE$
-^\[main.assertion.2\] assertion tmp_if_expr\$2: SUCCESS$
+^\[main.assertion.1\] assertion tmp_if_expr(\$\d+)?: FAILURE$
+^\[main.assertion.2\] assertion tmp_if_expr\$\d+: SUCCESS$
 ^\*\* 1 of 2 failed
 ^VERIFICATION FAILED$
 ^EXIT=10$

regression/cbmc/pointer-function-parameters-2/test.desc

@@ -3,10 +3,10 @@ main.c
 --function fun --cover branch
 ^\*\* 7 of 7 covered \(100.0%\)$
 ^Test suite:$
-^a=\(\(signed int \*\*\)NULL\), tmp\$\d+=[^,]*, tmp\$\d+=[^,]*$
-^a=&tmp\$\d+!0, tmp\$\d+=\(\(signed int \*\)NULL\), tmp\$\d+=[^,]*$
-^a=&tmp\$\d+!0, tmp\$\d+=&tmp\$\d+!0, tmp\$\d+=(-[0-9]+|[012356789][0-9]*|4[0-9]+)$
-^a=&tmp\$\d+!0, tmp\$\d+=&tmp\$\d+!0, tmp\$\d+=4$
+^a=\(\(signed int \*\*\)NULL\), tmp(\$\d+)?=[^,]*, tmp(\$\d+)?=[^,]*$
+^a=&tmp(\$\d+)?!0, tmp(\$\d+)?=\(\(signed int \*\)NULL\), tmp(\$\d+)?=[^,]*$
+^a=&tmp(\$\d+)?!0, tmp(\$\d+)?=&tmp\$\d+!0, tmp(\$\d+)?=(-[0-9]+|[012356789][0-9]*|4[0-9]+)$
+^a=&tmp(\$\d+)?!0, tmp(\$\d+)?=&tmp(\$\d+)?!0, tmp(\$\d+)?=4$
 ^EXIT=0$
 ^SIGNAL=0$
 --

regression/cbmc/pointer-function-parameters/test.desc

@@ -3,9 +3,9 @@ main.c
 --function fun --cover branch
 ^\*\* 5 of 5 covered \(100\.0%\)$
 ^Test suite:$
-^a=\(\(signed int \*\)NULL\), tmp\$\d+=[^,]*$
-^a=&tmp\$\d+!0, tmp\$\d+=4$
-^a=&tmp\$\d+!0, tmp\$\d+=([012356789][0-9]*|4[0-9]+)$
+^a=\(\(signed int \*\)NULL\), tmp(\$\d+)?=[^,]*$
+^a=&tmp(\$\d+)?!0, tmp(\$\d+)?=4$
+^a=&tmp(\$\d+)?!0, tmp(\$\d+)?=([012356789][0-9]*|4[0-9]+)$
 ^EXIT=0$
 ^SIGNAL=0$
 --

regression/goto-diff/java-tmp-vars-array/new/Test.java

@@ -0,0 +1,11 @@
+public class Test {
+  public int[] f00(int[] x) {
+    int[] y = new int[x.length];
+    return y;
+  }
+
+  public int[] f01(int[] z) {
+    int[] w = new int[z.length];
+    return w;
+  }
+}

regression/goto-diff/java-tmp-vars-array/old/Test.java

@@ -0,0 +1,11 @@
+public class Test {
+  public int[] f00(int[] x) {
+    int[] y = x;
+    return y;
+  }
+
+  public int[] f01(int[] z) {
+    int[] w = new int[z.length];
+    return w;
+  }
+}

regression/goto-diff/java-tmp-vars-array/test.desc

@@ -0,0 +1,10 @@
+CORE
+new.jar
+old.jar
+// Enable multi-line checking
+activate-multi-line-match
+EXIT=0
+SIGNAL=0
+new functions:\nmodified functions:\n  Test\.java: java::Test\.f00:\(\[I\)\[I\ndeleted functions:
+--
+^warning: ignoring

regression/goto-diff/java-tmp-vars-inc/new/Test.java

@@ -0,0 +1,11 @@
+public class Test {
+  public int f00(int x) {
+    int y = x++;
+    return y;
+  }
+
+  public int f01(int z) {
+    int w = z++;
+    return w;
+  }
+}

regression/goto-diff/java-tmp-vars-inc/old/Test.java

@@ -0,0 +1,11 @@
+public class Test {
+  public int f00(int x) {
+    int y = x;
+    return y;
+  }
+
+  public int f01(int z) {
+    int w = z++;
+    return w;
+  }
+}

regression/goto-diff/java-tmp-vars-inc/test.desc

@@ -0,0 +1,10 @@
+CORE
+new.jar
+old.jar
+// Enable multi-line checking
+activate-multi-line-match
+EXIT=0
+SIGNAL=0
+new functions:\nmodified functions:\n  Test\.java: java::Test\.f00:\(I\)I\ndeleted functions:
+--
+^warning: ignoring

regression/goto-diff/java-tmp-vars-new/new/Test.java

@@ -0,0 +1,17 @@
+class B {
+  void foo() {}
+}
+
+class A {
+  B b = new B();
+}
+
+public class Test {
+  public A f00(A x) {
+    return org.cprover.CProver.nondetWithoutNull();
+  }
+
+  public A f01(A z) {
+    return org.cprover.CProver.nondetWithoutNull();
+  }
+}

regression/goto-diff/java-tmp-vars-new/old/Test.java

@@ -0,0 +1,17 @@
+class B {
+  void foo() {}
+}
+
+class A {
+  B b = new B();
+}
+
+public class Test {
+  public A f00(A x) {
+    return x;
+  }
+
+  public A f01(A z) {
+    return org.cprover.CProver.nondetWithoutNull();
+  }
+}

regression/goto-diff/java-tmp-vars-new/test.desc

@@ -0,0 +1,10 @@
+CORE
+new.jar
+old.jar
+// Enable multi-line checking
+activate-multi-line-match
+EXIT=0
+SIGNAL=0
+new functions:\nmodified functions:\n  Test\.java: java::Test\.f00:\(LA;\)LA;\ndeleted functions:
+--
+^warning: ignoring

regression/goto-diff/java-tmp-vars-string/new/Test.java

@@ -0,0 +1,11 @@
+public class Test {
+  public String f00(String x) {
+    String y = x + "abc";
+    return y;
+  }
+
+  public String f01(String z) {
+    String w = z + "abc";
+    return w;
+  }
+}

regression/goto-diff/java-tmp-vars-string/old/Test.java

@@ -0,0 +1,11 @@
+public class Test {
+  public String f00(String x) {
+    String y = x;
+    return y;
+  }
+
+  public String f01(String z) {
+    String w = z + "abc";
+    return w;
+  }
+}

regression/goto-diff/java-tmp-vars-string/test.desc

@@ -0,0 +1,10 @@
+CORE
+new.jar
+old.jar
+// Enable multi-line checking
+activate-multi-line-match
+EXIT=0
+SIGNAL=0
+new functions:\nmodified functions:\n  Test\.java: java::Test\.f00:\(Ljava/lang/String;\)Ljava/lang/String;\ndeleted functions:
+--
+^warning: ignoring

src/ansi-c/c_nondet_symbol_factory.cpp

@@ -43,8 +43,8 @@ static const symbolt &c_new_tmp_symbol(
   const bool static_lifetime,
   const std::string &prefix="tmp")
 {
-  symbolt &tmp_symbol=
-    get_fresh_aux_symbol(type, "", prefix, loc, ID_C, symbol_table);
+  symbolt &tmp_symbol = get_fresh_aux_symbol(
+    type, id2string(loc.get_function()), prefix, loc, ID_C, symbol_table);
   tmp_symbol.is_static_lifetime=static_lifetime;
 
   return tmp_symbol;

src/goto-instrument/code_contracts.cpp

@@ -250,7 +250,7 @@ const symbolt &code_contractst::new_tmp_symbol(
 {
   return get_fresh_aux_symbol(
     type,
-    "",
+    id2string(source_location.get_function()),
     "tmp_cc",
     source_location,
     irep_idt(),

src/goto-programs/convert_nondet.cpp

@@ -17,6 +17,7 @@ Author: Reuben Thomas, [email protected]
 #include <java_bytecode/java_object_factory.h> // gen_nondet_init
 
 #include <util/irep_ids.h>
+#include <util/fresh_symbol.h>
 
 #include <memory>
 
@@ -135,11 +136,13 @@ void convert_nondet(
   message_handlert &message_handler,
   const object_factory_parameterst &object_factory_parameters)
 {
+  object_factory_parameterst parameters = object_factory_parameters;
+  parameters.function_id = function.get_function_id();
   convert_nondet(
     function.get_goto_function().body,
     function.get_symbol_table(),
     message_handler,
-    object_factory_parameters);
+    parameters);
 
   function.compute_location_numbers();
 }
@@ -158,6 +161,8 @@ void convert_nondet(
 
     if(symbol.mode==ID_java)
     {
+      object_factory_parameterst parameters = object_factory_parameters;
+      parameters.function_id = f_it.first;
       convert_nondet(
         f_it.second.body,
         symbol_table,

src/goto-programs/goto_convert_class.h

@@ -34,7 +34,6 @@ class goto_convertt:public messaget
     messaget(_message_handler),
     symbol_table(_symbol_table),
     ns(_symbol_table),
-    temporary_counter(0),
     tmp_symbol_prefix("goto_convertt")
   {
   }
@@ -46,7 +45,6 @@ class goto_convertt:public messaget
 protected:
   symbol_table_baset &symbol_table;
   namespacet ns;
-  unsigned temporary_counter;
   std::string tmp_symbol_prefix;
 
   void goto_convert_rec(const codet &code, goto_programt &dest);

src/goto-programs/goto_convert_functions.cpp

@@ -147,8 +147,6 @@ void goto_convert_functionst::convert_function(
 
   // make tmp variables local to function
   tmp_symbol_prefix=id2string(symbol.name)+"::$tmp::";
-  temporary_counter=0;
-  reset_temporary_counter();
 
   f.type=to_code_type(symbol.type);
 

src/goto-programs/goto_convert_side_effect.cpp

@@ -379,14 +379,15 @@ void goto_convertt::remove_function_call(
 
     new_base_name+='_';
     new_base_name+=id2string(symbol.base_name);
-    new_base_name+="$"+std::to_string(++temporary_counter);
+    new_base_name += "$0";
 
     new_symbol.base_name=new_base_name;
     new_symbol.mode=symbol.mode;
   }
 
   new_symbol.name=tmp_symbol_prefix+id2string(new_symbol.base_name);
 
+  // ensure that the name is unique
   new_name(new_symbol);
 
   {
@@ -429,10 +430,11 @@ void goto_convertt::remove_cpp_new(
 
   auxiliary_symbolt new_symbol;
 
-  new_symbol.base_name="new_ptr$"+std::to_string(++temporary_counter);
+  new_symbol.base_name = "new_ptr$0";
   new_symbol.type=expr.type();
   new_symbol.name=tmp_symbol_prefix+id2string(new_symbol.base_name);
 
+  // ensure that the name is unique
   new_name(new_symbol);
 
   code_declt decl;
@@ -480,11 +482,12 @@ void goto_convertt::remove_malloc(
   {
     auxiliary_symbolt new_symbol;
 
-    new_symbol.base_name="malloc_value$"+std::to_string(++temporary_counter);
+    new_symbol.base_name = "malloc_value$0";
     new_symbol.type=expr.type();
     new_symbol.name=tmp_symbol_prefix+id2string(new_symbol.base_name);
     new_symbol.location=expr.source_location();
 
+    // ensure that the name is unique
     new_name(new_symbol);
 
     code_declt decl;

src/goto-programs/remove_function_pointers.cpp

@@ -233,14 +233,13 @@ void remove_function_pointerst::fix_return_type(
        code_type.return_type(), ns))
     return;
 
-  symbolt &tmp_symbol=
-    get_fresh_aux_symbol(
-      code_type.return_type(),
-      "remove_function_pointers",
-      "tmp_return_val",
-      function_call.source_location(),
-      irep_idt(),
-      symbol_table);
+  symbolt &tmp_symbol = get_fresh_aux_symbol(
+    code_type.return_type(),
+    id2string(function_call.source_location().get_function()),
+    "tmp_return_val",
+    function_call.source_location(),
+    irep_idt(),
+    symbol_table);
 
   symbol_exprt tmp_symbol_expr;
   tmp_symbol_expr.type()=tmp_symbol.type;

src/goto-programs/remove_instanceof.cpp

@@ -106,14 +106,13 @@ std::size_t remove_instanceoft::lower_instanceof(
   symbol_typet jlo=to_symbol_type(java_lang_object_type().subtype());
   exprt object_clsid=get_class_identifier_field(check_ptr, jlo, ns);
 
-  symbolt &newsym=
-    get_fresh_aux_symbol(
-      object_clsid.type(),
-      "instanceof_tmp",
-      "instanceof_tmp",
-      source_locationt(),
-      ID_java,
-      symbol_table);
+  symbolt &newsym = get_fresh_aux_symbol(
+    object_clsid.type(),
+    id2string(this_inst->function),
+    "instanceof_tmp",
+    source_locationt(),
+    ID_java,
+    symbol_table);
 
   auto newinst=goto_program.insert_after(this_inst);
   newinst->make_assignment();