Merge pull request #2077 from peterschrammel/stable-tmp-var-names

Prefix temporary variable names with function id

Author: peterschrammel

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.jar

@@ -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/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 = new int[z.length];
+    return w;
+  }
+}

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

@@ -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